符号执行分析套件

要解决的具体问题

符号执行是 CTF 与二进制漏洞分析中的常用手段，但直接让模型编写 angr 脚本往往得到不可用的代码：状态初始化错误导致脚本启动即崩溃，缺少 libc 函数钩子让求解器陷入无意义的路径探索，路径爆炸让执行迟迟无法收敛。本技能把这些易错点固化为可复用的模式。

具体痛点：

• 脚本不稳定：基础模型生成的 angr 脚本常因状态初始化错误、缺少 libc 函数钩子而直接崩溃。
• 约束不会解：符号值与具体值混用，导致 Z3 求解失败或得到错误答案。
• 执行被卡住：路径爆炸后探索空间失控，脚本长时间无法结束。

技能如何工作

核心流程分四步：

1. 选工具：纯逻辑约束交给 Z3；需要寄存器与内存状态、路径探索时用 angr；二进制加壳或无法直接加载时先用 Unicorn Engine 仿真脱壳。
2. 初始化状态：加载二进制、建立初始状态，按模板完成符号化输入（stdin、argv 或符号文件）。
3. 挂接钩子：对 scanf、printf、malloc、strcmp 等 libc 函数套用钩子模板或 SimProcedure 替换，避免无关调用拖慢探索。
4. 求解与收敛：探索结束后把路径约束交给 Z3 求解，得到满足条件的输入。

配套的 ANGR_COOKBOOK.md 收录 15+ 个开箱即用的脚本模式，覆盖常见 CTF 场景，并给出路径爆炸管理的优化技巧。遇到反调试检查可路由到 anti-debugging-techniques，做去混淆时路由到 code-obfuscation-deobfuscation，分析自定义 VM 挑战时路由到 vm-and-bytecode-reverse。

适用边界与注意点

• 路径爆炸在复杂程序上仍可能失控，钩子与剪枝只缓解不消除。
• SimProcedure 替换改变了函数语义，对结果有强依赖的场景需人工复核。
• 仿真脱壳只覆盖轻量壳，强混淆或带反仿真的壳需要额外手段。
• 自定义 VM 挑战需先识别字节码语义，angr 无法自动推导 VM 指令。