CTF 逆向约束求解实战：在 ctf-wiki 中用 Z3 SMT 求解器破解复杂算法题

• 文档
• 网络安全
• 教程

Z3 是由微软开发的可满足性模理论求解器（SMT Solver），能在给定的一组逻辑约束中快速找到一个可行解。在 CTF 逆向题中，当程序将输入经过复杂变换后再用一组等式做校验时，手工逆推往往费时且易错，此时用 Z3 建模约束即可一键求解出合法输入。本文以 ctf-wiki 中的 z3.md 为主线，从安装、变量建模、约束添加与求解讲起，并以 GWCTF 2019 的xxor题目完整演示"逆向分析 → Z3 求解 → 逆运算还原 flag"的实战流程。

Z3 求解器架构示意图

Z3 是什么：SMT 求解器简介

Z3 是微软研究院开发的可满足性模理论求解器（Satisfiability Modulo Theory solver，即SMT solver）。它用于检查一组逻辑表达式的可满足性（satisfiable），并且能够在这组约束中找出其中一个可行解——注意它并不会枚举出全部可行解。

从架构上看，Z3 对外提供 C++、Python、.NET、Java、OCaml 等多种语言接口，这些高层接口最终都会落到底层 C API 与 SMT-LIB 输入之上；内部则由 Tactics（策略）层负责预处理（Preprocessing）、分块求解（Cube & Conquer）以及Then、Or、Probe等策略组合，再交由 SAT、SMT、NLSat、Fixedpoint、QSAT 等底层求解器完成实际求解。这也是上文架构图中输入 → 策略调度 → 求解器求解的整体流程。

在 CTF 逆向题中，我们经常会遇到形如"输入经过若干轮加密变换后必须满足一组等式"的约束条件，此时使用z3辅助求解是最高效的方案。在 ctf-wiki 的导航结构中，该主题被编排在 mkdocs.yml 的"逆向分析 → 工具 → 约束求解"目录下，与 angr、unicorn 等符号执行工具一起构成逆向辅助工具链。

安装 z3-solver

Z3 提供了多种语言的接口，在 CTF 场景中通常使用 Python 版本，直接通过 pip 安装即可。注意这里应当安装的是z3-solver而非z3（z3是一个无关的同名包）：

$ pip3 install z3-solver

ctf-wiki 在搭建 CTF 环境时也将z3-solver作为逆向/Pwn 基础工具预装，例如在 environment.md 的 Dockerfile 中可以看到它与 pwntools、angr、capstone、keystone-engine 等一同被pip install进容器环境，说明该库是 CTF 逆向工作流中的标配组件。

基本用法

本节仅介绍 z3 最核心的建模与求解用法。一阶命题逻辑公式由项（变量或常量）与扩展布尔结构组成，z3 的 Python API 恰好一一对应了这套概念。

变量表示

在z3中可以通过如下方式创建变量实例：

• 整型（integer，长度不限）

>>> import z3 >>> x = z3.Int(name = 'x') # x is an integer

• 实数类型（real number，长度不限）

>>> y = z3.Real(name = 'y') # y is a real number

• 位向量（bit vector，长度需在创建时指定）——逆向题中模拟 C 语言的int/uint32_t等定长类型时最常用

>>> z = z3.BitVec(name = 'z', bv = 32) # z is a 32-bit vector

• 布尔类型（bool）

>>> p = z3.Bool(name = 'p')

整型与实数类型变量之间可以互相转换，例如在混合算术表达式中把整数提升为实数参与除法运算，或把实数截断为整数：

>>> z3.ToReal(x) ToReal(x) >>> z3.ToInt(y) ToInt(y)

常量表示

除了 Python 原有的常量数据类型外，也可以使用z3自带的常量类型参与运算，从而保证运算对象与变量同属 z3 的表达式体系：

>>> z3.IntVal(val = 114514) # integer 114514 >>> z3.RealVal(val = 1919810) # real number 1919810 >>> z3.BitVecVal(val = 1145141919810, bv = 32) # bit vector，自动截断 2680619074 >>> z3.BitVecVal(val = 1145141919810, bv = 64) # bit vector 1145141919810

注意上面位向量常量的行为：当数值超出指定位宽时会被自动截断（1145141919810放入 32 位向量后变成2680619074），这与 C 语言中整数溢出的语义一致，因此逆向建模时务必按目标变量的真实类型选择位宽。

求解器

在使用z3进行约束求解之前，需要先获得一个求解器（Solver）类实例。它本质上就是一组约束的集合，后续所有约束都会被添加进该集合，并在调用check()时统一交给求解引擎处理：

>>> s = z3.Solver()

添加约束

通过求解器的add()方法为指定求解器添加约束条件，约束条件可以直接用z3变量组成的式子进行表示：

>>> s.add(x * 5 == 10) >>> s.add(y * 1/2 == x)

对于布尔类型的式子，可以使用z3内置的And()、Or()、Not()、Implies()等方法进行布尔逻辑运算：

>>> s.add(z3.Implies(p, q)) >>> s.add(r == z3.Not(q)) >>> s.add(z3.Or(z3.Not(p), r))

And/Or可接受多个参数，Implies(a, b)表示"若 a 则 b"，它们共同构成了逻辑约束（如条件分支、状态机判断）的建模基础。

约束求解

当约束添加完毕，使用check()方法检查约束是否可满足（satisfiable），即 z3 是否能够找到一组解：

• z3.sat：约束可以被满足
• z3.unsat：约束无法被满足

>>> s.check() sat

若约束可满足，则可以通过model()方法获取一组解，解以"变量 → 取值"的映射形式给出：

>>> s.model() [q = True, p = False, x = 2, y = 4, r = False]

对于约束数量比较少的情况，也可以不创建求解器，直接通过solve()方法求解，它等价于"建一个临时 Solver、add 全部约束、check 并打印 model"的快捷方式：

>>> z3.solve(z3.Implies(p, q), r == z3.Not(q), z3.Or(z3.Not(p), r)) [q = True, p = False, r = False]

例题：GWCTF 2019 - xxor

下面通过 GWCTF 2019 的xxor题目完整走一遍"逆向 → 建模 → 求解 → 还原"的流程。该题的主逻辑是：读入 6 个整数 → 前三个整数经过 3 轮类 TEA 变换 → 对变换结果做一组等式校验。手工逆推这组混合了移位、加法、异或的等式非常繁琐，而用 Z3 可以在毫秒级直接求出变换后的中间值，再逆着加密逻辑还原出原始输入。

逆向分析

首先将程序拖入 IDA，main()函数整体逻辑比较简单：首先读入 6 个整型到栈上，接下来对前三个整型调用三次sub_400686()函数进行处理并将结果存到v7中，最后调用sub_400770()进行检查：

__int64 __fastcall main(int a1, char **a2, char **a3) { int i; // [rsp+8h] [rbp-68h] int j; // [rsp+Ch] [rbp-64h] __int64 v6[6]; // [rsp+10h] [rbp-60h] BYREF __int64 v7[6]; // [rsp+40h] [rbp-30h] BYREF v7[5] = __readfsqword(0x28u); puts("Let us play a game?"); puts("you have six chances to input"); puts("Come on!"); v6[0] = 0LL; v6[1] = 0LL; v6[2] = 0LL; v6[3] = 0LL; v6[4] = 0LL; for ( i = 0; i <= 5; ++i ) { printf("%s", "input: "); a2 = (char **)((char *)v6 + 4 * i); __isoc99_scanf("%d", a2); } v7[0] = 0LL; v7[1] = 0LL; v7[2] = 0LL; v7[3] = 0LL; v7[4] = 0LL; for ( j = 0; j <= 2; ++j ) { dword_601078 = v6[j]; dword_60107C = HIDWORD(v6[j]); a2 = (char **)&unk_601060; sub_400686(&dword_601078, &unk_601060); LODWORD(v7[j]) = dword_601078; HIDWORD(v7[j]) = dword_60107C; } if ( (unsigned int)sub_400770(v7, a2) != 1 ) { puts("NO NO NO~ "); exit(0); } puts("Congratulation!\n"); puts("You seccess half\n"); puts("Do not forget to change input to hex and combine~\n"); puts("ByeBye"); return 0LL; }

sub_400686()有点类似于魔改的 TEA 加密：以输入为初始状态(v3, v4)，每轮让v5累加一个常数，并用移位、加法、异或混合运算更新v3、v4，共迭代0x40（64）轮：

__int64 __fastcall sub_400686(unsigned int *a1, _DWORD *a2) { __int64 result; // rax unsigned int v3; // [rsp+1Ch] [rbp-24h] unsigned int v4; // [rsp+20h] [rbp-20h] int v5; // [rsp+24h] [rbp-1Ch] unsigned int i; // [rsp+28h] [rbp-18h] v3 = *a1; v4 = a1[1]; v5 = 0; for ( i = 0; i <= 0x3F; ++i ) { v5 += 1166789954; v3 += (v4 + v5 + 11) ^ ((v4 << 6) + *a2) ^ ((v4 >> 9) + a2[1]) ^ 0x20; v4 += (v3 + v5 + 20) ^ ((v3 << 6) + a2[2]) ^ ((v3 >> 9) + a2[3]) ^ 0x10; } *a1 = v3; result = v4; a1[1] = v4; return result; }

这里的参数a1为输入，而a2则为四个 int32 常量（这也是 TEA 算法中"密钥"的角色），位于数据段：

.data:0000000000601060 dword_601060 dd 2 ; DATA XREF: main+FE↑o .data:0000000000601064 dd 2 .data:0000000000601068 dd 3 .data:000000000060106C dd 4

而sub_400770()会对处理过后的输入进行检查，检查条件是一个由加减法组成的等式系统：

__int64 __fastcall sub_400770(_DWORD *a1) { __int64 result; // rax if ( a1[2] - a1[3] == 2225223423LL && a1[3] + a1[4] == 4201428739LL && a1[2] - a1[4] == 1121399208LL && *a1 == -548868226 && a1[5] == -2064448480 && a1[1] == 550153460 ) { puts("good!"); result = 1LL; } else { puts("Wrong!"); result = 0LL; } return result; }

用 Z3 求解约束

这一组"变换后必须满足"的等式非常适合交给 Z3。我们定义 6 个整型变量x[0]~x[5]表示sub_400686()运算后的中间结果，然后把sub_400770()中的全部校验等式（注意将负数换算为对应的 32 位无符号十六进制等价形式，如-548868226 == 0xDF48EF7E）逐一add进求解器：

import z3 x = [0] * 6 for i in range(6): x[i] = z3.Int('x[' + str(i) + ']') s = z3.Solver() s.add(x[0] == 0xDF48EF7E) s.add(x[5] == 0x84F30420) s.add(x[1] == 0x20CAACF4) s.add(x[2]-x[3] == 0x84A236FF) s.add(x[3]+x[4] == 0xFA6CB703) s.add(x[2]-x[4] == 0x42D731A8) if s.check() == z3.sat: print(s.model()) else: raise Exception("NO SOLUTION!")

运行求解脚本，得到中间结果（其中x[0]、x[1]、x[5]由常量约束直接确定，x[2]~x[4]由三元一次方程组解出）：

$ python3 solve.py [x[2] = 3774025685, x[3] = 1548802262, x[4] = 2652626477, x[1] = 550153460, x[5] = 2230518816, x[0] = 3746099070]

值得说明的是，这里s.check() == z3.sat的判断是必要的一步——只有当求解器确认约束可满足时，model()返回的解才是有效的；若返回unsat则说明约束本身自相矛盾（例如建模时等式符号写错、位宽选择错误等）。

逆运算还原输入

拿到中间结果后，还需要逆着sub_400686()的逻辑写出解密程序还原原始输入。TEA 这类 Feistel 结构的加密是可逆的：加密时v5从 0 开始每轮累加0x458BCD42（即十进制的 1166789954），解密时则从加密结束时的sum开始，每轮先逆推v4、再逆推v3，最后让sum回退一个0x458BCD42：

#include <stdio.h> #include <stdint.h> void decrypt(uint32_t sum, uint32_t *v, uint32_t *k) { uint32_t v0, v1; v0 = v[0]; v1 = v[1]; for (int i = 0; i < 0x40; i++) { v1 -= (v0 + sum + 20) ^ ((v0 << 6) + k[2]) ^ ((v0 >> 9) + k[3]) ^ 0x10; v0 -= (v1 + sum + 11) ^ ((v1 << 6) + k[0]) ^ ((v1 >> 9) + k[1]) ^ 0x20; sum -= 0x458BCD42; } v[0] = v0; v[1] = v1; } int main(int argc, char **argv, char **envp) { uint32_t data[] = { 3746099070, 550153460, 3774025685, 1548802262, 2652626477, 2230518816 }; uint32_t sum = 0; uint32_t k[] = { 2, 2, 3, 4 }; for (int i = 0; i < 0x40; i++) { sum += 0x458BCD42; } for (int i = 0; i < 3; i++) { decrypt(sum, &data[i * 2], k); printf("%4x%4x", data[i * 2], data[i * 2 + 1]); } puts(""); return 0; }

运行解密程序，得到一段十六进制字符串：

$ ./solve 666c61677b72655f69735f6772656174217d

还原 flag

把十六进制字符串两两一组转成 ASCII 字符，就是最终的 flag：

s = '666c61677b72655f69735f6772656174217d' while len(s) != 0: print(chr(int(s[:2], 16)), end = '') s = s[2:] print('') # flag{re_is_great!}

完整流程可以概括为三步：IDA 逆向提取校验约束 → Z3 求中间值 → 逆算法还原输入。其中 Z3 承担的是最枯燥的等式求解环节，让解题者把精力集中在算法识别（这里是类 TEA 结构）与逆向还原上。

小结

• Z3 是一个 SMT 求解器，能在约束集合中找到一个可行解；CTF 逆向中它主要用于处理"变换后必须满足一组等式"的校验型题目。
• 建模的核心是选对类型：定长数据（int32、uint64等）用BitVec并指定位宽，纯数学整数用Int，含小数的场景用Real，布尔逻辑用Bool配合And/Or/Not/Implies。
• 求解的固定套路是：Solver()创建求解器 →add()逐条添加约束 →check()判断sat/unsat→model()取解；简单场景可直接用solve()一步到位。
• 拿到中间值后，通常还需按加密算法的可逆结构写解密程序，把 Z3 的结果进一步还原为真正的输入，正如例题xxor中 TEA 解密与十六进制转字符的收尾工作。

更多高级用法（如Optimize优化目标、策略组合、数组/量词等理论）可查阅 Z3 官方 API 文档，本文覆盖的基础建模与求解套路已足以应对绝大多数 CTF 逆向中的约束求解需求。

• 文档
• 网络安全
• 教程