国赛上逆向有道题目要算 37 元一次方程，肯定不能用手算。解决方法是用 python Z3 库，这个库可以帮助我们解决方程的计算问题。

Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

安装

1
pip install z3-solver

简单使用

1
2
3
4
5
6
from z3 import *

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
# [y = 0, x = 7]

做题约束条件肯定不会这么少，所以需要实例化一个 Solver() 对象，方便我们添加更多的约束条件。

进阶使用

Solver 对象

创建约束求解器：

1
solver = Solver()

设置变量

Int - 整数型

1
2
3
4
# 声明单个变量
x = Int('x')
# 声明多个变量
y,z = Ints('y z')

Real - 实数型

1
2
3
4
# 声明单个变量
x = Real('x')
# 声明多个变量
y,z = Reals('y z')

BitVec - 向量（位与运算）

1
2
3
4
# 声明单个变量
x = BitVec('x')
# 声明多个变量
y,z = BitVecs('y z')

变量设置的类型可能会影响到最后求解的结果。可以先 check 一下看看有没有解，然后再判断是否需要切换变量的类型。

添加约束条件

一行一个约束条件，这里的约束条件就是方程等式：

1
2
3
solver.add(x**2+y**2==74)
solver.add(x**5-y==z)
# [y = -7, x = 5, z = 3132]

判断是否有解

1
2
3
4
if solver.check() == sat:
    print("solver")
else:
    print("no solver")

求解并输出

1
2
ans = solver.model()
print(ans)

额外补充

通常如果是做题的话，解密出来很可能是 flag ，也就是 ascii 码，所以为了进一步确定答案可以给每一个变量都加上额外的一条约束，约束其结果只能在可见 ascii 码范围以内：

1
2
solver.add(x < 127)
solver.add(x >= 32)

练习例题

参考文章