Z3方程求解器位掩码操作

Question

在对一个程序进行逆向工程之后，我发现了这些限制。在

我必须找到两个无符号的数字：

x + y = 0xC0ED91BD

以及

^{pr2}$

在原始程序中，数字的乘法是使用imul指令执行的。在

当只检查Z的低32位时，Z应该小于60。在

Z & 0x00000000ffffffff < 60

但是，当我添加第二个等式作为约束时，z3给出了一个错误。在

我的代码是：

#! /usr/bin/python

from z3 import *
import sys

s = Solver()
result = int(sys.argv[1], 16)

x = Int('x')
y = Int('y')

s.add(x + y == result)
s.add(x > 0, y > 0)
s.add((x * y) & 0x00000000ffffffff < 60)

while s.check() == sat:
    print s.model()
    s.add(Or(x != s.model()[x], y != s.model()[y]))

更新：

以下是基于推荐解决方案的代码：

#! /usr/bin/python

from z3 import *
import sys

s = Solver()
x = BitVec('x', 32)
y = BitVec('y', 32)

result = BitVecVal(int(sys.argv[1], 16), 32)

s.add(x + y == result)
s.add(x > 0, y > 0)
s.add(x * y < 10)

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

二进制文件是64位的。在

但是，乘法运算是使用32位整数执行的，如下所示：

mov     edx, [rbp+var_14]
mov     eax, [rbp+var_10]
imul    eax, edx

因此，如果eax=0x425a95e5和edx=0x7e92fbd8

然后在使用imul指令进行乘法后，eax将存储：0x00000038。在

同时，EFLAGS寄存器中的进位标志位和溢出标志位都将在其之后设置。在

Answer 1

这里的问题是您已经声明了x和{}是任意宽度的整数，而不是固定长度的位向量。只需更改声明以匹配基础位大小。假设你想用32位运算，你会说：

x = BitVec('x', 32)
y = BitVec('y', 32)

相反。您还应该类似地声明result：

^{pr2}$

一旦你做了这些改变，你的程序应该可以正常工作。在

注意，在这种情况下，使用0x00000000ffffffff进行掩蔽是不必要的；因为数字已经是32位宽了。只有当x和y较大时，才需要保留它；比如64位。在

通过以上更改，当我运行程序并用0xC0ED91BD调用它时，我得到以下输出：

[y = 2123561944, x = 1113232869]
[y = 1440310864, x = 1796483949]
[y = 1171875408, x = 2064919405]
... many other lines ..

这可能看起来很混乱，因为数字似乎比你想象的要大。但请记住，位向量上的算术是按2^n进行的，其中n是位大小，因此结果实际上是正确的：

>>> 2123561944 + 1113232869 % 2**32 == 0xC0ED91BD
True
>>> 2123561944 * 1113232869 % 2**32 < 60
True

等等