Z3一把梭：用约束求解搞定一类CTF题

本文转载自知乎，长亭技术专栏原创文章

原文作者：朱文雷

原文链接：https://zhuanlan.zhihu.com/p/30548907?utm_source=tuicool&utm_medium=referral

点击文末阅读原文，即可跳转

Z3 简介

Z3 是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题（可以简单理解为解方程的感觉，虽然这么比喻其实还差距甚远，请勿吐槽），功能强大且易于使用，本文以近期的 CTF 题为实例，向尚未接触过约束求解器的小伙伴们介绍 Z3 在 CTF 解题中的应用。

Z3 约束求解器是针对 Satisfiability modulo theories Problem 的一种通用求解器。所谓 SMT 问题，在 Z3 环境下是指关于算术、位运算、数组等背景理论的一阶逻辑组合决定性问题。虽然 Z3 功能强大，但是从理论上来说，大部分 SMT 问题的时间复杂度都过高，根本不可能在有限时间内解决。所以千万不要把 Z3 想象得过于万能。

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

Z3 本身提供一个类似于 Lisp 的内置语言，但是实际使用中，一般使用 Python Binding 操作会比较方便。

• http://z3prover.github.io/api/html/namespacez3py.html

• https://pypi.python.org/pypi/z3-solver/4.5.1.0

• https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Z3 入门

Z3 内置了多种变量类型，基本能覆盖常见计算机数据结构。包括整数、浮点数、BitVector、数组等。

先来一个简单的例子看一下 Z3 能做什么：

from z3 import *

x = Int('x')
y = Int('y')
solve(x > 2, y 
上面的例子中，定义了两个变量：x 和 y。类型为 Int（注意这里的 Int 可不是 C/C++ 里面包含上下界的 int，Z3 中的 Int 对应的就是数学中的整数，Z3 中的 BitVector 才对应到 C/C++ 中的 int）。
然后就调用了 solve 函数求解三个条件下的满足模型，这三个条件分别是 x 大于 2，y 小于 10，并且 x 加 2 个 y 等于 7。
运行一下结果：
(z3env) $ python example.py 
[y = 0, x = 7]
可以看出，Z3 找到了 y=0，x=7 这组解。细心的小伙伴会发现，x=5,y=1 也符合条件，为什么没有体现？原因在于 Z3 在默认情况下，只寻找满足所有条件的一组解，而不是找出所有解。
好了，经过上面的简单介绍相信大家都对 Z3 有一个基本的认识，下面看看在 CTF 实际应用。

Z3 实战样题一：DEFCAMP 2017 Misc 题 forgot my key
题目如下：
I forgot my flag & key. Help me recover them.
5616f5962674d26741d2810600a6c5647620c4e3d2870177f09716b2379012c342d3b584c5672195d653722443f1c39254360007010381b721c741a532b03504d2849382d375c0d6806251a2946335a67365020100f160f17640c6a05583f49645d3b557856221b2

这题给了一个加密函数，要求还原 flag 和 
key。观察可以发现，加密串每一位都与明文、key、和加密串的前一位相关。但是由于第一位是随机出来的，所以很难从开头递推出来。但是细心观察 
message 的构成又可以发现，后面 32 位是 key 的 md5 串，倒数第 33 位又是已知，因此从这里就可以打开突破口。整理思路如下：

• 第一步：通过倒数第 33 位明文已知，且密文已知，因此可以求得某一位 md5($key) 的值。

• 第二步：根据上一步推出来的值，又可以进一步推另一位 message 的值。如此往复下去，最终应该能找到所有的值。

  
  

思路是有了，然而写起来未必简单，因为人的思维都是正向的，逆向求解特别是还要写出完整求解代码总是麻烦的。

于是我们考虑是否可以使用 Z3 来求解。首先题目肯定保证了答案的唯一性，因此 Z3 求解成功就会得到 flag 无疑。其次，我们根据题目的变换方式，给 Z3 所有的正推关系式，把逆推的逻辑让 Z3 通过约束求解来完成，由于逆推可以一步步进行，因此也不会导致 Z3 复杂度爆炸求解不出来。如此分析应该 Z3 一把梭问题不大。

代码如下：

运行求解：

在我的 Mac 上总共耗时 7s。从这个 solve.py 可以看出，由于使用了 Z3，求解整个题目所需要做的事情基本就是照着原来的逻辑照抄翻译一遍，再添加其他细节（如可见字符范围在32到127之间），然后求解，就大功告成了！

Z3 实战样题二：CSAW 2017 逆向题 realism

前面是一道简单的 misc/crypto 题目，这里再展示 Z3 在一道逆向题的应用。 realism 是一个主要针对 x86 SSE 指令 的逆向题目。题目可以从 https://github.com/youben11/CSAW_2017_quals_rev400 获取。

题目的主要逻辑其实并不长，但是由于应用了 SSE 指令，且同样是一番循环逻辑运算之后，要求运算结果与某个预设值相等，逆向起来有一定复杂度。关键逻辑如下图：