Z3 约束求解器

安装
Z3 理论基础
使用 Z3
Z3 在 CTF 中的运用
参考资料

Z3 是一个由微软开发的 Satisfiability Modulo Theories（SMT）求解器。可以用来检查满足一个或多个理论的公式的可满足性，也就是说,它可以自动化地通过内置理论对一阶逻辑多种排列进行可满足性校验。目前其支持的理论有：

equality over free 函数和谓词符号
实数和整形运算(有限支持非线性运算)
位向量
阵列
元组/记录/枚举类型和代数（递归）数据类型
...

因其强大的功能，Z3 已经被用于许多领域中，在安全领域，主要见于符号执行、Fuzzing、二进制逆向、密码学等。另外 Z3 提供了多种语言的接口，这里我们使用 Python。

安装

在 Linux 环境下，执行下面的命令：

$ git clone https://github.com/Z3Prover/z3.git
$ cd z3

$ python scripts/mk_make.py --python
$ cd build
$ make
$ sudo make install

另外还可以使用 pip 来安装 Python 接口，这是二进制分析框架 angr 里内置的修改版：

$ sudo pip install z3-solver

Z3 理论基础

Op	Mnmonics	Description
0	true	恒真
1	flase	恒假
2	=	相等
3	distinct	不同
4	ite	if-then-else
5	and	n元合取
6	or	n元析取
7	iff	implication
8	xor	异或
9	not	否定
10	implies	Bi-implications

使用 Z3

先来看一个简单的例子：

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

首先定义了两个变量 x 和 y，类型是 Z3 内置的整数类型 Int，solve() 函数会创造一个 solver，然后对括号中的约束条件进行求解，注意在 Z3 默认情况下只会找到满足条件的一组解。

>>> simplify(x + y + 2*x + 3)
3 + 3*x + y
>>> simplify(x < y + x + 2)
Not(y <= -2)
>>> simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
And(x >= 2, 2*x**2 + y**2 >= 3)
>>>
>>> simplify((x + 1)*(y + 1))
(1 + x)*(1 + y)
>>> simplify((x + 1)*(y + 1), som=True)
1 + x + y + x*y

simplify() 函数用于对表达式进行化简，同时可以设置一些选项来满足不同的要求。更多选项使用 help_simplify() 获得。

同时，Z3 提供了一些函数可以解析表达式：

>>> n = x + y >= 3
>>> "num args: ", n.num_args()
('num args: ', 2)
>>> "children: ", n.children()
('children: ', [x + y, 3])
>>> "1st child:", n.arg(0)
('1st child:', x + y)
>>> "2nd child:", n.arg(1)
('2nd child:', 3)
>>> "operator: ", n.decl()
('operator: ', >=)
>>> "op name:  ", n.decl().name()
('op name:  ', '>=')

set_param() 函数用于对 Z3 的全局变量进行配置，如运算精度，输出格式等等：

>>> x = Real('x')
>>> y = Real('y')
>>> solve(x**2 + y**2 == 3, x**3 == 2)
[x = 1.2599210498?, y = -1.1885280594?]
>>>
>>> set_param(precision=30)
>>> solve(x**2 + y**2 == 3, x**3 == 2)
[x = 1.259921049894873164767210607278?,
 y = -1.188528059421316533710369365015?]

逻辑运算有 And、Or、Not、Implies、If，另外 == 表示 Bi-implications。

>>> p = Bool('p')
>>> q = Bool('q')
>>> r = Bool('r')
>>> solve(Implies(p, q), r == Not(q), Or(Not(p), r))
[q = False, p = False, r = True]
>>>
>>> x = Real('x')
>>> solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
[x = -1.4142135623?, p = False]

Z3 提供了多种 Solver，即 Solver 类，其中实现了很多 SMT 2.0 的命令，如 push, pop, check 等等。

>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()    # 创造一个通用 solver
>>> type(s)         # Solver 类
<class 'z3.z3.Solver'>
>>> s
[]
>>> s.add(x > 10, y == x + 2)   # 添加约束到 solver 中
>>> s
[x > 10, y == x + 2]
>>> s.check()       # 检查 solver 中的约束是否满足
sat                 # satisfiable/满足
>>> s.push()        # 创建一个回溯点，即将当前栈的大小保存下来
>>> s.add(y < 11)
>>> s
[x > 10, y == x + 2, y < 11]
>>> s.check()
unsat               # unsatisfiable/不满足
>>> s.pop(num=1)    # 回溯 num 个点
>>> s
[x > 10, y == x + 2]
>>> s.check()
sat
>>> for c in s.assertions():    # assertions() 返回一个包含所有约束的AstVector
...     print(c)
... 
x > 10
y == x + 2
>>> s.statistics()  # statistics() 返回最后一个 check() 的统计信息
(:max-memory   6.26
 :memory       4.37
 :mk-bool-var  1
 :num-allocs   331960806
 :rlimit-count 7016)
>>> m = s.model()   # model() 返回最后一个 check() 的 model
>>> type(m)         # ModelRef 类
<class 'z3.z3.ModelRef'>
>>> m
[x = 11, y = 13]
>>> for d in m.decls():         # decls() 返回 model 包含了所有符号的列表
...     print("%s = %s" % (d.name(), m[d]))
... 
x = 11
y = 13

5.3 KiB Raw Blame History Unescape Escape

Z3 约束求解器

安装

Z3 理论基础

使用 Z3

Z3 在 CTF 中的运用

参考资料

5.3 KiB

Raw Blame History