re-z3

---
name: re-z3
description: Z3 约束求解：建模、密钥/flag 推导。触发词：z3、约束求解、solver、SMT
---

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

## 何时使用 / 何时不用

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

## 工具准备

参考 [[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]]）。

1. **从反编译还原约束（比较链 / 数学关系）**：
   - 列出"合法输入必须满足"的**每条**约束：输入来源（用户输入 / 文件名 / 密文）、每次变换（算术 / 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

2. **BitVec / Int 建模**：
   - 位运算为主（XOR / 移位 / 按位与）→ 用 **BitVec**，位宽对齐反编译语义（32 位运算用 `BitVec('x', 32)`，逐字节用 8 位）
   - 纯数学关系（加减乘、比较大小、无位运算）→ 用 **Int** 更快（但溢出语义与 C 不同，见坑 5）
   - 按输入结构建模：字符逐位处理 → 一个 8 位 BitVec 数组或用大 BitVec 切片：
     ```python
     from z3 import *
     s = Solver()
     inp = [BitVec(f'inp_{i}', 8) for i in range(8)]      # 8 字节输入
     ```
   - **位宽不匹配立即出问题**：`BitVec(..., 8)` 与 `BitVec(..., 32)` 直接相加会报 TypeError / 无解——宽度统一，见坑 5

3. **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）

4. **边界（长度 / 字符集）约束**：
   - **先加边界后求解**（无界变量会拖慢求解甚至跑飞，见坑 1）：
     ```python
     for c in inp:
         s.add(c >= 0x20, c <= 0x7e)      # 可打印 ASCII（flag 场景）
     s.add(inp[0] == ord('f'))            # 已知格式头 flag{ 逐位固化
     ```
   - 长度约束：输入长度固定值（`inp[7] == ord('}')`）；校验位 / 分隔符格式按反编译补
   - 已从题目线索 / 格式（`flag{...}`）得知的部分**直接固化为等式**，大幅提速
   - 边界加完先小规模验证：注释掉部分约束跑一次看求解耗时与解的合理性

5. **输出 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]]：求解结果的运行验证沙箱（[[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()` 验证观测值本身与模型是否一致