4

作为逆向工程练习的一部分，我正在尝试编写 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。有人可以帮助弄清楚如何让第一个循环工作吗？

编辑：我能够得到一个接近上面显示的 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。我将如何更改脚本，这样我就不必对长度进行硬编码？每次运行程序时如何生成不同的解决方案？

4

2 回答 2

3

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

看来您实际上在原始程序（name.size()）中有一个界限，因此枚举到该限制就足够了。否则，您可能需要一个量词，例如 Int sort 的 \forall x 。name[x] < 65。当然，这带有关于量词的所有警告（例如，参见Z3 指南）

于 2014-05-19T17:09:43.820 回答
2

假设要确定长度。这是我认为你可以做的：

length = Int('length')
x = Int('x')
s.add(ForAll(x,Implies(And(x>=0,x<length),And(passwd[x] < 127,passwd[x] >=48))))
于 2015-06-22T20:43:56.277 回答