python - 将 Python Z3 与 QWORD 结合使用

Question

我是 z3py 的新手。

我正在对代码进行逆向工程，其中 XMM 寄存器中存储有两个 QWORD。

并且对其执行不同的操作。

假设我必须找到 2 个 qword，p1 和 p2，给出以下等式:

x = p1 + p2
y = p1 ^ p2

if x == r1 and y == r2:
    print p1, p2

注意:P1 和 P2 是 QWORD，实际上代表 8 个字符的 ASCII 字符串。因此，P1 是一个 8 字节的数组，其中每个字节对应于可打印字符的 ASCII 值。

我编写了以下代码:

#! /usr/bin/python

from z3 import *

s = Solver()

a = BitVec('a', 64)
b = BitVec('b', 64)

s.add(a + b == result1)
s.add(a ^ b == result2)

if s.check():
    print(s.model())

问题:

我认为在我的例子中不应该使用 BitVec 来表示 QWORD，因为我知道 QWORD 的每个字节对应于一个可打印的 ASCII 字符。那么，我应该如何表示我的输入？

Answer 1

最好改用 4 个 8 位值的 Python 数组:

#! /usr/bin/python

from z3 import *

s = Solver()

A = [BitVec('a%s' % i, 8) for i in range(4)]
B = [BitVec('b%s' % i, 8) for i in range(4)]

s.add(A[0] <= 128)
s.add(A[0] + B[0] == 12)
s.add(A[1] + B[1] == 5)
s.add(A[2] ^ B[2] == 9)
s.add(A[3] >= 20)

if s.check() == sat:
    print(s.model())

打印:

[a2 = 0,
 b2 = 9,
 a3 = 20,
 b1 = 0,
 a1 = 5,
 b0 = 140,
 a0 = 128]

这样您就可以通过以自然的方式使用数组元素来添加任意约束。