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

Z3 简介

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

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

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

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

Z3 入门

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

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

from z3 import *

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

上面的例子中,定义了两个变量: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

function my_encrypt($flag, $key) {
  $key = md5($key);
  $message = $flag . "|" . $key;

  $encrypted = chr(rand(0, 126));
  for($i=0;$i<strlen($message);$i++) {
    $encrypted .= chr((ord($message[$i]) + ord($key[$i % strlen($key)]) + ord($encrypted[$i])) % 126);
  }
  $hexstr = unpack('h*', $encrypted);
  return array_shift($hexstr);
}

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

  • 第一步:通过倒数第 33 位明文已知,且密文已知,因此可以求得某一位 md5($key) 的值。
  • 第二步:根据上一步推出来的值,又可以进一步推另一位 message 的值。如此往复下去,最终应该能找到所有的值。

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

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

代码如下:

#!/usr/bin/env python3

from z3 import *
import binascii

s = '5616f5962674d26741d2810600a6c5647620c4e3d2870177f09716b2379012c342d3b584c5672195d653722443f1c39254360007010381b721c741a532b03504d2849382d375c0d6806251a2946335a67365020100f160f17640c6a05583f49645d3b557856221b2'

encrypted = []
for i in range(0, len(s), 2):
    encrypted.append(binascii.unhexlify(s[i+1] + s[i])[0])

print('message len:', len(encrypted)-1)
print(encrypted)
# 声明变量,encrypted 是已知,因此 IntVal 即可
encrypted = [IntVal(i) for i in encrypted]
message = [Int('flag%d' % i) for i in range(len(encrypted)-1)]
# 创建一个求解器,求解全靠它
solver = Solver()

ml = len(encrypted) - 1

# 添加明文字符的约束条件
for i in range(ml):
    if i == ml - 33:
        solver.add(message[i] == ord('|'))
    else:
        # 肯定是可见字符,因此限定范围如下
        solver.add(message[i] < 127)
        solver.add(message[i] >= 32)
# 添加明文和密文对照关系的约束条件
for i in range(ml):
    solver.add(encrypted[i+1] == (message[i] + message[ml-32+i%32] + encrypted[i]) % 126)

if solver.check() == sat:
    m = solver.model()
    s = []
    for i in range(ml):
        s.append(m[message[i]].as_long())
    print(bytes(s))
else:
    print('unsat') 

运行求解:

(z3env) $ time python solve.py 
message len: 103
b'DCTF{0d940de38493d96dc6255cbb2c2ac7a2db1a7792c74859e95215caa6b57c69b2}|6941f4cac9b7784fdd77e11b51cd0d64'

real	0m7.277s
user	0m7.260s
sys	0m0.010s 

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

z3 实战样题二:CSAW 2017 逆向题 realism

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

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

image

把逻辑整理成伪代码如下:

xmm5 = results[0]

for i in range(8, 0, -1):
    xmm2 = andps(flag, bytes(masks[i:i+8]))
    xmm5 = psadbw(xmm5, xmm2)
    assert xmm5 == results[9-i] 

同样的,如果要根据结果逆推,首先需要理解清楚每一个指令的精确含义,然后需要做大量的逆推工作。因此考虑是否可以用 Z3 从正向思维来解决这类问题。

这里的难点在于要准确模拟 andps 和 psadbw 两个指令的行为。此外,需要选择正确的 BitVector 大小。因为 8 位会导致 psadbw 加法溢出得到错误的值,因此这里统一使用 16 位。

程序如下: gist.github.com/zTrix/0

运行我们的程序:

(z3env) $ time python3 solve.py 
b'flag{4r3alz_m0d3_y0}'

real	0m0.788s
user	0m0.790s
sys	0m0.000s 

仅需 0.8s 即可解出结果。

总结

合理使用 Z3 可以在许多场景下根据约束自动帮助我们求解,只需要根据正向思路使用 Z3 表达原有逻辑即可,大大减少我们分析和逆推的时间。当然,Z3 的功能远不止这些,这里只是介绍了最简单的入门应用,有兴趣的小伙伴可以通过阅读文档资料进一步了解。

参考资料

(长亭技术专栏原创文章,转载请注明来源)


为您推荐了相关的技术文章:

  1. 符号执行:利用Angr进行简单CTF逆向分析
  2. Automatic Exploit Generation:漏洞利用自动化
  3. 符号执行入门
  4. Z3Py在CTF逆向中的运用
  5. 从一道Crypto题目认识z3 - 安全客,安全资讯平台

原文链接: zhuanlan.zhihu.com