angr 符号执行（符号化输入 / 自动求解）

何时使用 / 何时不用

• 用：CTF 逆向题——输入在长循环 / 深比较链里逐字节校验（校验通过地址已知或可定位），人工逆推繁琐易错
• 用：已知"输入必须到达某地址 / 避开某地址"，想把路径条件交给求解器（find / avoid 模式）
• 用：输入来源复杂（argv / 文件 / 标准输入），需要按通道符号化后求解
• 不用：简单 XOR / 明文比较（一屏伪代码内）——人工更快（[[re-binary-core]]）
• 不用：校验含不可符号化内容（环境相关值、随机数、未符号化输入）——会无解或误解（见坑 3）
• 不用：需要精确约束集合而非一条路径时——纯约束求解用 [[re-z3]] 更轻（见坑 2）
• 注意：符号执行是把双刃剑——先人工定位关键校验函数缩小符号化范围（见坑 2）；运行验证走沙箱（[[re-analyze/platform-tips]] 最高原则）

工具准备

参考 [[re-analyze/platform-tips]] 最高原则——用求解结果运行目标验证时默认沙箱；angr 本身是进程内仿真器，不接触真实系统调用，求解过程无需沙箱。

angr（pip 安装）