Satisfiability Modulo Theories (SMT) - Z3

Tip

学习和实践 AWS 黑客技术：HackTricks Training AWS Red Team Expert (ARTE)
学习和实践 GCP 黑客技术：HackTricks Training GCP Red Team Expert (GRTE) 学习和实践 Azure 黑客技术：HackTricks Training Azure Red Team Expert (AzRTE)

支持 HackTricks

• 查看 订阅计划!
• 加入 💬 Discord 群组 或 Telegram 群组 或 在 Twitter 🐦 上关注我们 @hacktricks_live.
• 通过向 HackTricks 和 HackTricks Cloud GitHub 仓库提交 PR 来分享黑客技巧。

很基本地，这个工具可以帮助我们为需要满足某些条件的变量寻找取值，手工计算会非常繁琐。因此，你可以向 Z3 指定变量需要满足的条件，它会找到一些值（如果可能的话）。

部分文本和示例摘自 https://ericpony.github.io/z3py-tutorial/guide-examples.htm

基本操作

布尔/与/或/非

#pip3 install z3-solver
from z3 import *
s = Solver() #The solver will be given the conditions

x = Bool("x") #Declare the symbos x, y and z
y = Bool("y")
z = Bool("z")

# (x or y or !z) and y
s.add(And(Or(x,y,Not(z)),y))
s.check() #If response is "sat" then the model is satifable, if "unsat" something is wrong
print(s.model()) #Print valid values to satisfy the model

Ints/Simplify/Reals

from z3 import *

x = Int('x')
y = Int('y')
#Simplify a "complex" ecuation
print(simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
#And(x >= 2, 2*x**2 + y**2 >= 3)

#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
#so you can get the decimals you need from the solution
r1 = Real('r1')
r2 = Real('r2')
#Solve the ecuation
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
#Solve the ecuation with 30 decimals
set_option(precision=30)
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))

打印模型

from z3 import *

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
s.check()

m = s.model()
print ("x = %s" % m[x])
for d in m.decls():
print("%s = %s" % (d.name(), m[d]))

机器算术

现代 CPU 和主流编程语言使用基于 定长位向量 的算术运算。机器算术在 Z3Py 中以 Bit-Vectors 的形式提供。

from z3 import *

x = BitVec('x', 16) #Bit vector variable "x" of length 16 bit
y = BitVec('y', 16)

e = BitVecVal(10, 16) #Bit vector with value 10 of length 16bits
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print(simplify(a == b)) #This is True!
a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
print(simplify(a == b)) #This is False

有符号/无符号数

Z3 提供了针对有符号/无符号情形的特殊算术运算。对于位向量是否被视为有符号或无符号，运算结果会不同。在 Z3Py 中，运算符 <, <=, >, >=, /, % 和 >> 对应于 有符号 版本。相应的 无符号 运算符是 ULT, ULE, UGT, UGE, UDiv, URem 和 LShR.

from z3 import *

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)
solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)
solve(x < 0)

# using unsigned version of <
solve(ULT(x, 0))

在 reversing 中常用的 Bit-vector 辅助

当你 lifting checks from assembly or decompiler output 时，通常最好将每个输入字节建模为 BitVec(..., 8)，然后像目标代码那样精确重建字（word）。这样可以避免将数学整数与机器算术混用所导致的错误。

from z3 import *

b0, b1, b2, b3 = BitVecs('b0 b1 b2 b3', 8)
eax = Concat(b3, b2, b1, b0)        # little-endian bytes -> 32-bit register value
low_byte = Extract(7, 0, eax)        # AL
high_word = Extract(31, 16, eax)     # upper 16 bits
signed_b0 = SignExt(24, b0)          # movsx eax, byte ptr [...]
unsigned_b0 = ZeroExt(24, b0)        # movzx eax, byte ptr [...]
rot = RotateLeft(eax, 13)            # rol eax, 13
logical = LShR(eax, 3)               # shr eax, 3
arith = eax >> 3                     # sar eax, 3 (signed shift)

将代码翻译为约束时的一些常见陷阱：

• >> 对位向量表示 算术 右移。对于逻辑的 shr 指令，使用 LShR。
• 当原始比较/除法是 无符号 时，使用 UDiv、URem、ULT、ULE、UGT 和 UGE。
• 保持位宽明确。如果二进制截断到 8 或 16 位，请使用 Extract 或用 Concat 重建该值，而不要默默地将所有内容提升为 Python 整数。

函数

解释型函数，例如算术，其中 函数 + 有一个 固定的标准解释（它把两个数相加）。未解释函数 和常量是 最大程度灵活的；它们允许 任何解释，只要该解释与关于该函数或常量的 约束 一致。

from z3 import *

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
s.check()
m = s.model()
print("f(f(x)) =", m.evaluate(f(f(x))))
print("f(x)    =", m.evaluate(f(x)))

print(m.evaluate(f(2)))
s.add(f(x) == 4) #Find the value that generates 4 as response
s.check()
print(m.model())

示例

数独求解器

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
(0,0,0,5,1,0,0,0,7),
(0,8,9,0,0,0,0,4,0),
(0,0,0,0,0,0,2,0,8),
(0,6,0,2,0,1,0,5,0),
(1,0,2,0,0,0,0,0,0),
(0,7,0,0,0,0,5,2,0),
(9,0,0,0,6,5,0,0,0),
(0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print "failed to solve"

Reversing workflows

如果你需要对二进制进行符号执行并自动收集约束，请查看 angr 的说明：

Angr

如果你已经在查看反编译的校验并且只需求解它们，直接使用 Z3 通常更快且更易控制。

Lifting byte-based checks from a crackme

在 crackmes 和 packed loaders 中，一个非常常见的模式是针对候选密码的一长串字节方程。将字节建模为 8 位向量，限制字符集，并且只有在原始代码扩大它们时才放宽。

</details>

这种风格很适合真实世界的逆向，因为它与现代 writeups 的实际做法一致：恢复算术/按位关系，将每个比较转换为约束，然后一次性求解整个系统。

#### 使用 `push()` / `pop()` 的增量求解

在逆向过程中，你经常想在不重建整个求解器的情况下测试多个假设。`push()` 会创建一个检查点，`pop()` 会丢弃在该检查点之后添加的约束。当你不确定某个分支是带符号还是无符号、某个寄存器是零扩展还是符号扩展，或当你在尝试从反汇编中提取的多个候选常量时，这非常有用。
```python
from z3 import *

x = BitVec('x', 32)
s = Solver()
s.add((x & 0xff) == 0x41)

s.push()
s.add(UGT(x, 0x1000))
print(s.check())
s.pop()

s.push()
s.add(x == 0x41)
print(s.check())
print(s.model())
s.pop()

from z3 import *

xs = [BitVec(f'x{i}', 8) for i in range(4)]
s = Solver()
for x in xs:
s.add(And(x >= 0x30, x <= 0x39))
s.add(xs[0] + xs[1] == xs[2] + 1)
s.add(xs[3] == xs[0] ^ 3)

while s.check() == sat:
m = s.model()
print(''.join(chr(m[x].as_long()) for x in xs))
s.add(Or([x != m.eval(x, model_completion=True) for x in xs]))

from z3 import *

t = Then('simplify', 'solve-eqs', 'bit-blast', 'sat')
s = t.solver()