如何在 Z3Py 中循环遍历数组 [英] How to loop over array in Z3Py
问题描述
作为逆向工程练习的一部分，我正在尝试编写一个 Z3 求解器来查找满足以下程序的用户名和密码.这个特别难，因为大家参考的z3py教程(rise4fun)下线了.
As part of a reverse engineering exercise, I'm trying to write a Z3 solver to find a username and password that satisfy the program below. This is especially tough because the z3py tutorial that everyone refers to (rise4fun) is down.
#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，这就是我所拥有的:
I got that code from the assembly of a binary, and while it may be wrong I want to focus on writing the solver. I'm starting with the first part, just calculating r1, and this is what I have:
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 的任意大小的数组.
All I'm asserting is that there are no letters less than 'A' in the array, so I expect to get back an array of any size that has numbers greater than 65.
显然这是完全错误的，主要是因为它无限循环.另外，我不确定我计算的总和是否正确，因为我不知道它是否被初始化为 0.有人可以帮助弄清楚如何让第一个循环工作吗?
Obviously this is completely wrong, mainly because it infinite loops. Also, I'm not sure I'm calculating sum correctly, because I don't know if it's initialized to 0. Could someone help figure out how to get this first loop working?
我能够得到一个接近上面显示的 C++ 代码的 z3 脚本:
I was able to get a z3 script that is close to the C++ code shown above:
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.我将如何更改脚本，这样我就不必对长度进行硬编码?每次运行程序时我将如何生成不同的解决方案?
This code was able to give me a correct username and password. However, I hardcoded the lengths of one for the username and five for the password. How would I change the script so I wouldn't have to hard code the lengths? And how would I generate a different solution each time I run the program?
推荐答案
Z3 中的数组不一定有任何边界.在这种情况下，索引排序是 Int，这意味着无界整数(不是机器整数).因此，for c in name 将永远运行，因为它枚举了 name[0], name[1], name[2], ...
Arrays in Z3 do not necessarily have any bounds. In this case the index-sort is Int, which means unbounded integers (not machine integers). Consequently, for c in name will run forever because it enumerates name[0], name[1], name[2], ...
看来您实际上在原始程序中有一个边界(name.size())，因此枚举到该限制就足够了.否则，您可能需要一个量词，例如 \forall x of Int sort .名称[x] <65. 当然，这带有关于量词的所有警告(参见例如 Z3 指南)
It seems that you actually have a bound in the original program (name.size()), so it would suffice to enumerate up to that limit. Otherwise you might need a quantifier, e.g., \forall x of Int sort . name[x] < 65. This comes with all the warnings about quantifiers, of course (see e.g., the Z3 Guide)
这篇关于如何在 Z3Py 中循环遍历数组的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
