z3介绍

Z3 是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题，功能强大且易于使用，常用于解决CTF当中的密码题或逆向题，Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

z3安装

由于os下安装失败了，所以我在我的虚拟机ubuntu16.04下安装
千万不要用pip install z3或者pip install z3-solver来安装，会发现使用不了
用源码安装就很舒服

#创建一个用于z3的虚拟python环境
virtualenv z3 #没有安装的可以用pip直接安装

#进入到我们的z3环境
cd z3 

#启动虚拟python环境
source ~/z3/bin/active

#下载z3源码(这里我嫌git clone太慢了直接去github下载)
去https://github.com/Z3Prover/z3下载源码然后解压

#编译z3
cd z3
python scripts/mk_make.py --python

cd build
make
make install
#然后就安装成功了

#这里再强烈安利bpython，感觉比ipython还棒，可以更好的了解z3库的函数
pip install bpython

z3的使用

(z3) ☁  exp  bpython
bpython version 0.17.1 on top of Python 2.7.12 /usr/bin/python
>>> from z3 import *
>>> 
>>> x = Int('x')  #定义一个整数型x变量
>>> y = Int('y') #定义一个整数型y变量
>>> solve(x > 2, y < 10, x + 2*y == 7)  #求满足x > 2, y < 10, x + 2*y == 7的解
[y = 0, x = 7]  #默认只返回一组解

又或者可以写成下面这样

(z3) ☁  exp  bpython
bpython version 0.17.1 on top of Python 2.7.12 /usr/bin/python
>>> from z3 import *
>>> 
>>> x = Int('x') #定义一个整数型x变量
>>> y = Int('y') #定义一个整数型y变量
>>> solver = Solver() #生成一个约束求解器
>>> solver.add(x > 2) #添加约束条件 x > 2
>>> solver.add(y < 10) #添加约束条件 y < 10
>>> solver.add(x + 2*y == 7) ##添加约束条件 x + 2*y == 7
>>> solver.check() #检查是否有解，如果有,返回sat; 如果不满足,返回unsat
sat
>>> solver.model() #输出结果
[y = 0, x = 7]

除了整数型变量我们还可以用Real设置实数型变量,用BitVec设置多少位的变量

z3 in CTF

这里我们拿angr的一道例题简单练练手
crackme

题目逻辑很简单，就是输入一个key，然后通过4个校验就输出correct,否则wrong

直接上脚本：

from z3 import *
v4 = Int('v4')
solver = Solver()

v5 = v4 % 100 / 10
solver.add(v4 % 10 + v5 + v4 / 1000 + v4 % 1000 / 100 == 23)
solver.add(v5 / (v4 % 10) == 2 )
solver.add(v4 % 1000 / 100 - v5 == -1)
solver.add(v4 / 1000 % v5 == 3)
#solver.add(v4 % 10 != 0)

#遍历全部输出结果，Or函数表示或的意思，就是条件只需要满足其中的一个就行
while solver.check() == sat : 
	print solver.model()
	print '---------------\n'
	solver.add(Or(solver.model()[v4] != v4))


(z3) ☁  exp  python crackme.py
sat
[v4 = 9563]

#几乎秒出结果(z3真好用)

☁  Symbolic-Execution  ./crackme     
please input the key:9563
correct!

以后做到其他逆向题的时候再深入研究

参考文章：