如何在 Z3Py 中循环数组

作为逆向工程练习的一部分，我尝试编写一个 Z3 解算器来查找满足以下程序的用户名和密码。这尤其困难，因为每个人参考的 z3py 教程（rise4fun）都已关闭。

#include <iostream>
#include <string>

using namespace std;

int main() {
    string name, pass;
    cout << "Name: ";
    cin >> name;

    cout << "Pass: ";
    cin >> pass;

    int sum = 0;
    for (size_t i = 0; i < name.size(); i++) {
        char c = name[i];
        if (c < 'A') {
            cout << "Lose: char is less than A" << endl;
            return 1;
        }
        if (c > 'Z') {
            sum += c - 32;
        } else {
            sum += c;
        }
    }
    int r1 = 0x5678 ^ sum;

    int r2 = 0;
    for (size_t i = 0; i < pass.size(); i++) {
        char c = pass[i];
        c -= 48;
        r2 *= 10;
        r2 += c;
    }
    r2 ^= 0x1234;

    cout << "r1: " << r1 << endl;
    cout << "r2: " << r2 << endl;
    if (r1 == r2) {
        cout << "Win" << endl;
    } else {
        cout << "Lose: r1 and r2 don't match" << endl;
    }
}

我从二进制文件的汇编中获得了该代码，虽然它可能是错误的，但我想专注于编写求解器。我从第一部分开始，只是计算r1，这就是我所拥有的：

from z3 import *

s = Solver()
sum = Int('sum')
name = Array('name', IntSort(), IntSort())
for c in name:
    s.add(c < 65)
    if c > 90:
        sum += c - 32
    else:
        sum += c
r1 = Xor(sum, 0x5678)
print s.check()
print s.model()

我所断言的是数组中没有小于“A”的字母，因此我希望返回一个数字大于 65 的任何大小的数组。

显然这是完全错误的，主要是因为它无限循环。另外，我不确定我是否正确计算总和，因为我不知道它是否初始化为 0。有人可以帮助弄清楚如何让第一个循环工作吗？

EDIT:我能够得到一个与上面所示的 C++ 代码接近的 z3 脚本：

from z3 import *

s = Solver()
sum = 0
name = Array('name', BitVecSort(32), BitVecSort(32))
i = Int('i')

for i in xrange(0, 1):
    s.add(name[i] >= 65)
    s.add(name[i] < 127)
    if name[i] > 90:
        sum += name[i] - 32
    else:
        sum += name[i]
r1 = sum ^ 0x5678

passwd = Array('passwd', BitVecSort(32), BitVecSort(32))
r2 = 0
for i in xrange(0, 5):
    s.add(passwd[i] < 127)
    s.add(passwd[i] >= 48)
    c = passwd[i] - 48
    r2 *= 10
    r2 += c
r2 ^= 0x1234

s.add(r1 == r2)

print s.check()
print s.model()

这段代码能够给我一个正确的用户名和密码。但是，我硬编码了用户名的长度为 1 和密码的长度为 5。我将如何更改脚本，这样我就不必对长度进行硬编码？每次运行程序时如何生成不同的解决方案？

Z3 中的数组不一定有任何界限。在这种情况下，索引排序是 Int，这意味着无界整数（不是机器整数）。最后，for c in name将永远运行，因为它枚举了name[0], name[1], name[2], ...

看来您实际上在原始程序中存在限制（name.size()），因此枚举到该限制就足够了。否则，您可能需要一个量词，例如 \forall x of Int sort 。 name[x] Z3 Guide)