Z3 约束求解（建模 / 密钥与 flag 推导）

何时使用 / 何时不用

用：从反编译还原出一组"合法输入必须满足"的比较链 / 数学等式（如序列号 = f(用户名)、flag 逐字节满足某关系），直接逆推繁琐时交给求解器
用：CTF 逆向题 / 加密题的密钥 / flag 推导（校验逻辑是纯确定性计算，无系统调用依赖）
用：已有人工展开的循环体（逐位 XOR / 移位 / 加减）约束，想验证约束集是否完备（见坑 4）
不用：输入在长循环里逐字节校验、循环未展开——先 re-angr 符号执行或先人工展开（本技能要求约束先还原成表达式，见坑 2）
不用：约束含哈希 / 非对称验签等不可逆运算——Z3 对 SHA / RSA 验签无能为力（见坑 3）
不用：需要整条路径条件而非约束集合——re-angr 更合适
注意：建模必须逐行对照反编译伪代码（re-ghidra / re-ida / re-radare2 产物）；求解出的结果跑原程序验证（沙箱，re-analyze/platform-tips 最高原则）

工具准备

参考 re-analyze/platform-tips 最高原则——求解本身不执行目标，但用求解结果运行目标验证时默认沙箱。

z3-solver（pip 安装）

pip install z3-solver（Linux / macOS / Windows 均提供预编译 wheel；纯 Python 绑定 + 原生库，安装简单）
若与系统包管理器混装冲突（系统 z3 版本旧）：先 pip install --upgrade z3-solver，或独立 venv 内安装
验证: python3 -c "import z3; print(z3.get_version_string())"
无网络环境：离线 wheel（pip download z3-solver 后拷入）或系统包 apt install z3（注意系统 z3 的 python 绑定与 pip 版 API 差异，推荐 pip 版）

python3

Linux: apt install python3（多数自带）；macOS: brew install python；Windows: 官方安装包 / choco install python
验证: python3 --version

反编译产物（约束还原的原料）

re-ghidra / re-ida / re-radare2 对校验函数的反编译伪代码——比较链、每次算术 / XOR / 查表变换、最终比对方式（strcmp / 校验位 / 逐位比较）；导出函数级伪代码，作为逐行建模的对照（见坑 4）
验证: 伪代码能完整覆盖"合法输入必须满足"的每一条约束

操作步骤

按顺序执行，每步记录结果（约束清单 / 建模脚本 / 求解输出 / 验证结果，证据路径见 re-triage）。

从反编译还原约束（比较链 / 数学关系）：
- 列出"合法输入必须满足"的每条约束：输入来源（用户输入 / 文件名 / 密文）、每次变换（算术 / XOR / 移位 / 查表）、最终比对方式（if (a == b) / 校验位相等 / 逐字节 strcmp）
- 逐条转成数学表达式，写成清单（伪代码行 → 约束式，一一对应，见坑 4）：
  - if (x * 3 + 5 != 0x100) fail → x*3 + 5 == 0x100
  - 循环已展开：for (i=0;i<8;i++) out[i]=in[i]^key[i]; if(strcmp(out, s)) fail → 8 条 in[i]^key[i] == s[i]
- 不要跳过任何一行——跳过的行就是漏掉的约束（见坑 4）；遇到不可逆段（哈希）先标记，见坑 3
BitVec / Int 建模：
- 位运算为主（XOR / 移位 / 按位与）→ 用 BitVec，位宽对齐反编译语义（32 位运算用 BitVec('x', 32)，逐字节用 8 位）
- 纯数学关系（加减乘、比较大小、无位运算）→ 用 Int 更快（但溢出语义与 C 不同，见坑 5）
- 按输入结构建模：字符逐位处理 → 一个 8 位 BitVec 数组或用大 BitVec 切片：
```
from z3 import *
s = Solver()
inp = [BitVec(f'inp_{i}', 8) for i in range(8)]      # 8 字节输入
```
- 位宽不匹配立即出问题：BitVec(..., 8) 与 BitVec(..., 32) 直接相加会报 TypeError / 无解——宽度统一，见坑 5
solver.check / model：
- 约束全部 s.add(...) 后：r = s.check() —— sat / unsat / unknown
- sat → m = s.model() 取解；unsat → 约束集有矛盾（见坑 4 / 坑 5）；unknown → 非线性 / 复杂表达式（见坑 3）
- 逐字节提取：''.join(chr(m[inp[i]].as_long()) for i in range(8))（BitVec 取值用 as_long()）
- 求解不是一次性的：先加边界约束再 check（见步骤 4），unsat 时用 s.assertions() 逐条注释排查（见坑 4）
边界（长度 / 字符集）约束：
- 先加边界后求解（无界变量会拖慢求解甚至跑飞，见坑 1）：
```
for c in inp:
    s.add(c >= 0x20, c <= 0x7e)      # 可打印 ASCII（flag 场景）
s.add(inp[0] == ord('f'))            # 已知格式头 flag{ 逐位固化
```
- 长度约束：输入长度固定值（inp[7] == ord('}')）；校验位 / 分隔符格式按反编译补
- 已从题目线索 / 格式（flag{...}）得知的部分直接固化为等式，大幅提速
- 边界加完先小规模验证：注释掉部分约束跑一次看求解耗时与解的合理性
输出 flag / 密钥：
- 组装输出：字节数组按序拼成字符串 / 十六进制，写进 flag.txt（或密钥二进制），同时打印 repr 检查（可打印性）
- 多解处理：while s.check() == sat: 取解 → s.add(Or(逐位 != 当前解)) 枚举多解，与题目预期比对（见坑 4）
- 验证：沙箱内（re-sandbox）把求解输出原样喂给目标程序（stdin / 参数 / 文件），必须校验通过 / 打印 flag；再与 re-angr / 人工还原结果交叉对照

跨域联合

re-ctf：本技能是 re-ctf 网关工作流第 3 步的约束求解路径（"满足一组等式即 flag / 密钥"）
re-binary-core：反编译工作台（re-ghidra / re-ida / re-radare2）——约束还原的原料；re-triage 初勘确认架构与位数（位宽建模依据）
re-angr：姊妹技能——长循环逐字节校验用 angr 符号执行；已展开 / 无循环的约束集合用本技能更轻更快；angr 求解慢时对约束子集转 z3
re-keygen / re-license：注册机场景——序列号 = f(用户名 / 机器码) 的等式集合建模求解（re-keygen 工具准备将 z3 列为可选方案；re-cracking 网关将其作为不可逆算法之外的硬推手段）
re-crypto-id / re-crypto-decrypt：自定义加密的密钥 / 明文推导（等式可逆部分建模；纯哈希部分见坑 3）
re-sandbox：求解结果的运行验证沙箱（re-analyze/platform-tips 最高原则）
re-patching：约束不可解（含不可逆段）时转补丁绕过验证

常见坑与陷阱

无界变量 → 求解慢 / 跑飞：现象——s.check() 几十分钟不返回，或内存暴涨；原因——符号变量没加取值范围约束，求解器遍历巨大空间（尤其乘除 / 移位组合）；对策——先加边界再求解（步骤 4：长度 / 字符集 / 位宽上限），已知格式位（flag{ 头）直接固化；仍慢就收紧边界逐段验证
位宽不匹配 → 无解 / 报错：现象——unsat 但人工看约束明明可满足，或 TypeError: unsupported operand；原因——不同位宽 BitVec 混算（8 位与 32 位相加、移位宽度不一致）、C 的隐式整数提升没建模（char 运算提升到 int 再截断）；对策——逐条对照伪代码确认运算宽度（32 位乘法结果只取低 32 位 = 加 Extract(31,0)）；先还原最小的完整语义再放宽（见坑 5）
非线性运算支持差 → 换思路：现象——check() 返回 unknown，或含乘法 / 异或组合时求解极慢；原因——非线性多项式（乘除、部分按位运算组合）对 SMT 求解器是难点；对策——能人工化简的先化简（XOR 对称性、常数折叠、用模逆 pow(a,-1,m) 消除法）；仍 unknown → 换 re-angr 符号执行整条路径，或逐位爆破（约束拆成单字节求解）；哈希 / 验签段直接放弃建模（不可逆），转 re-patching / 诚实报告
约束遗漏 → 错解：现象——求解出"满足"的输入跑程序却被拒；原因——反编译伪代码某行没转成约束（长度检查、字符集白名单、边界 if 分支、额外校验位），或求解器只给出一个解而题目要求特定解；对策——逐行对照伪代码核对约束清单（步骤 1 的一一对应表），把漏掉的 if / 校验补进 s.add；多解时枚举所有解逐一跑目标验证（步骤 5）；unsat 排查时逐条注释约束定位矛盾
溢出 / 有符号语义没建模：现象——求解结果数值与程序实际计算对不上（偶对偶错）；原因——C 的 32 位有符号溢出（int 乘法回绕）、移位方向（>> 算术 / 逻辑）、字节序（大端目标）没对齐；对策——确定目标架构与位数（re-triage），有符号运算用 BitVec(..., 32) + 符号扩展模拟，或改用 Int 加范围约束模拟回绕（s.add(a == (b * c) % 2**32)）；字节序按目标（多数 CTF 题小端）
长循环硬建模给 z3（该用 angr 的题）：现象——把长循环逐字节校验手工展开成约束，展开有误导致 unsat，或展开后求解极慢；原因——循环不变量提取 / 展开方式出错，且展开规模大；对策——长循环 / 深比较链先 re-angr 符号执行（自动处理循环与路径），z3 只接手"无循环、纯等式集合"（直接从 Ghidra 反编译提取的比较链）；两路结果交叉验证
PRNG 状态还原类问题可能返回错误模型：现象——check() 返回 sat 且模型数值合理，但代回原程序（如 xorshift128+ 生成器）输出对不上，或干脆无解；原因——某些位向量问题（PRNG 内部状态还原）对 SMT 求解器是已知难点（Z3 4.12.x 从两次输出还原 xorshift128+ 双 64 位状态有已知失败案例）；对策——结果必须交叉验证：把模型代回目标程序重放（re-sandbox）、枚举多解、或与 re-angr/暴力破解（密钥空间小时）对照；sat 不保证正确
硬编码"观测值"当常量断言 → 假 unsat：现象——unsat 但人工核对约束明明可满足；原因——把实验观测的中间值直接断言成等式（如 RNG(seed).next(26) == 57508594，而计算实际得 14325532），等式永假；对策——先不加中间观测值的断言，只断言输入-输出关系让 Z3 反推未知；确需固定中间值时先用 m.eval() 验证观测值本身与模型是否一致

11 KiB Raw Blame History Unescape Escape

Z3 约束求解（建模 / 密钥与 flag 推导）

何时使用 / 何时不用

工具准备

z3-solver（pip 安装）

python3

反编译产物（约束还原的原料）

操作步骤

跨域联合

常见坑与陷阱

11 KiB

Raw Blame History