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 安装）