简介
Z3是一个微软出品的开源约束求解器,能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题(可以简单理解为解方程的感觉,虽然这么比喻其实还差距甚远,请勿吐槽),功能强大且易于使用。
Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大,也被用于很多其他领域。CTF 领域来说,能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外,著名的二进制分析框架 angr 也内置了一个修改版的 Z3。
安装
这里我用的是angr里面的z3,安装教程。
测试
python
1 | from z3 import * |
上面的例子中,定义了两个变量:x 和 y。类型为 Int(注意这里的 Int 可不是 C/C++ 里面包含上下界的 int,Z3 中的 Int 对应的就是数学中的整数,Z3 中的 BitVector 才对应到 C/C++ 中的 int)。
然后就调用了 solve 函数求解三个条件下的满足模型,这三个条件分别是 x 大于 2,y 小于 10,并且 x 加 2 个 y 等于 7。
运行一下结果:
bash
1 | (angr) angr@36aeab92fea7:~/z3$ python test.py |
ctf实例
某比赛中的逆向题
首先我们利用IDA去打开该文件,定位到关键点,发现关键函数如下:
c
1 | signed __int64 sub_400766() |
可以看得出来这个题目的目的就是找出满足方程的flag。我们可以很方便的把方程式列出来,但是求解对于一些数学不是很好的人来说简直就是噩梦,这时候Z3求解器就可以很方便的给我们帮助。我们按照题目的意思一步一步利用Z3求解器来求解:
python
1 | from z3 import * |
第八届极客大挑战的REConvolution
我们打开文件,也是比较直观的看到约束条件,我试着逆向了这个过程,花费了挺多的时间才得到答案,但是如果我们使用Z3Py来求解的话就会非常的快。
函数关键部分如下:
c
1 | int __cdecl main(int argc, const char **argv, const char **envp) |
我们利用Z3Py来进行变量的声明和约束的增加并进行求解
python
1 | #! /usr/bin/env python2 |
执行脚本如下:
bash
1 | (angr) angr@36aeab92fea7:~/z3$ python exp2.py |