Z3约束求解器在CTF逆向中的应用教程

1. Z3简介

Z3是由微软公司开发的一个优秀的SMT（可满足性模理论）求解器，能够检查逻辑表达式的可满足性。主要应用领域包括：

• 软件/硬件验证和测试
• 约束求解
• 混合系统分析
• 安全性研究
• 生物学研究（计算机分析）
• 几何问题

在CTF逆向中，Z3可以简单理解为一个"解方程的计算器"，特别适用于当我们逆向到最后需要求flag或具体数值解时。

2. 安装Z3

2.1 Pycharm安装步骤

1. File → Settings → Project Interpreter
2. 点击+号
3. 搜索框中搜索"z3"
4. 下载z3和z3-solver

2.2 Linux下安装步骤

git clone https://github.com/Z3Prover/z3.git
cd z3
python scripts/mk_make.py
cd build
make
make install

3. Z3语法基础

3.1 主要数据类型

• Int：整型
• Bool：布尔型
• Array：数组
• BitVec('a',8)：char型（数字不一定是8，如C语言中的int型可以用BitVec('a',32)表示）

3.2 常用API

• Solver()：创建一个通用求解器
• add()：添加约束条件
• check()：检测解的情况（有解返回sat，无解返回unsat）
• model()：在存在解时，获取解的交集

4. 基础使用示例

4.1 简单方程求解

求解方程组：

x + y = 5
2x + 3y = 14

from z3 import *

# 1. 设未知数
x = Int('x')
y = Int('y')

# 2. 列方程
s = Solver()
s.add(x + y == 5)
s.add(2 * x + 3 * y == 14)

# 3. 解方程判断是否有解
if s.check() == sat:
    result = s.model()
    # 4. 输出方程的解
    print(result)
else:
    print('无解')

4.2 复杂逻辑问题求解

公务员考试题目示例（年龄计算问题）：

from z3 import *

a = Int('a')  # 2014年小李的年龄
b = Int('b')  # 小李弟弟的年龄
c = Int('c')  # 小王的年龄
d = Int('d')  # 小王哥哥的年龄

s = Solver()

# 添加约束条件
s.add(a == b + 4)  # 小李比他弟弟大4岁
s.add(c == d - 2)  # 小王比他哥哥小2岁
s.add(a + d == 40)  # 2014年小李和小王哥哥的年龄和是40
s.add(b + c == 36)  # 2015年小李弟弟和小王的年龄和是36

if s.check() == sat:
    print(s.model())

5. CTF逆向实战应用

5.1 题目分析

以Reversing.kr网站中的一道题目为例：

• 要求：当Serial为'76876-77776'时，求Name的值
• 提示：Name是4个字节，最后一个字节为'p'

5.2 解题步骤

1. 信息收集：

   • 程序为MFC编写，无壳
   • 输入错误的Name会显示"Wrong"

2. 关键函数定位：

   • 使用OD下GetWindowTextW断点
   • 通过栈回溯找到关键函数（偏移1740）

3. 逆向分析：

   • Name由4个字节组成，最后一个为'p'，其余3个为a-z
   • 存在10个判断方程，对应Serial的验证

4. 约束条件提取：

((name[0]&1)+5+(((name[1]>>2) & 1 )+1)) == ord('7')-0x30
((((name[0]>>3) & 1)+5)+(((name[1]>>3)&1)+1)) == ord('6')-0x30
(((name[0]>>1) & 1)+5+(((name[1]>>4) & 1 )+1)) == ord('8')-0x30
(((name[0]>>2) & 1)+5+(((name[1]) & 1 )+1)) == ord('7')-0x30
(((name[0]>>4) & 1)+5+(((name[1]>>1) & 1 )+1)) == ord('6')-0x30
(((name[2]) & 1)+5+(((name[3]>>2) & 1 )+1)) == ord('7')-0x30
(((name[2]>>3) & 1)+5+(((name[3]>>3) & 1 )+1)) == ord('7')-0x30
(((name[2]>>1) & 1)+5+(((name[3]>>4) & 1 )+1)) == ord('7')-0x30
(((name[2]>>2) & 1)+5+(((name[3]) & 1 )+1)) == ord('7')-0x30
(((name[2]>>4) & 1)+5+(((name[3]>>1) & 1 )+1)) == ord('6')-0x30

5. Z3求解脚本：

from z3 import *

name = [BitVec('u%d'%i,8) for i in range(0,4)]
solver = Solver()

# 添加10个约束条件
solver.add(((name[0]&1)+5+(((name[1]>>2) & 1 )+1))==ord('7')-0x30)
solver.add(((((name[0]>>3) & 1)+5)+(((name[1]>>3)&1)+1))==ord('6')-0x30)
solver.add((((name[0]>>1) & 1)+5+(((name[1]>>4) & 1 )+1))==ord('8')-0x30)
solver.add((((name[0]>>2) & 1)+5+(((name[1]) & 1 )+1))==ord('7')-0x30)
solver.add((((name[0]>>4) & 1)+5+(((name[1]>>1) & 1 )+1))==ord('6')-0x30)
solver.add((((name[2]) & 1)+5+(((name[3]>>2) & 1 )+1))==ord('7')-0x30)
solver.add((((name[2]>>3) & 1)+5+(((name[3]>>3) & 1 )+1))==ord('7')-0x30)
solver.add((((name[2]>>1) & 1)+5+(((name[3]>>4) & 1 )+1))==ord('7')-0x30)
solver.add((((name[2]>>2) & 1)+5+(((name[3]) & 1 )+1))==ord('7')-0x30)
solver.add((((name[2]>>4) & 1)+5+(((name[3]>>1) & 1 )+1))==ord('6')-0x30)

# 添加额外约束
solver.add(name[3] == ord('p'))
for i in range(0,4):
    solver.add(name[i] >= ord('a'))
    solver.add(name[i] <= ord('z'))

# 求解并输出结果
solver.check()
result = solver.model()
flag = ''
for i in range(0,4):
    flag += chr(result[name[i]].as_long().real)
print(flag)  # 输出结果为"bump"

6. 总结

Z3在CTF逆向中的应用要点：

1. 逆向分析提取关键约束条件
2. 将约束条件转化为Z3可识别的表达式
3. 合理设置变量类型和范围
4. 添加所有已知约束条件
5. 求解并验证结果

通过本教程，您应该已经掌握了Z3求解器在CTF逆向中的基本应用方法。在实际解题过程中，关键在于准确提取和分析程序中的约束条件，并将其正确转化为Z3可以处理的表达式。