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

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

安装

pip install z3-solver

简单使用

from z3 import *

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

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

进阶使用

Solver 对象

创建约束求解器:

solver = Solver()

设置变量

Int - 整数型

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

Real - 实数型

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

BitVec - 向量(位与运算)

# 声明单个变量
x = BitVec('x')
# 声明多个变量
y,z = BitVecs('y z')
变量设置的类型可能会影响到最后求解的结果。可以先 check 一下看看有没有解,然后再判断是否需要切换变量的类型。

添加约束条件

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

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

判断是否有解

if solver.check() == sat:
    print("solver")
else:
    print("no solver")

求解并输出

ans = solver.model()
print(ans)

额外补充

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

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

练习例题

参考文章

Last modification:September 6th, 2020 at 11:41 am