符号执行指南

解决什么问题

在使用 angr 做符号执行时，直接写出的脚本往往运行失败或陷入死循环。常见问题包括：未正确初始化内存状态、缺少对 libc 函数（如 scanf、printf）的 SimProcedure Hook，以及面对循环分支时发生的路径爆炸（Path Explosion）。

核心能力与工作流

本技能提供了一套工程化的分析手册，核心基于 angr、Z3 与 Unicorn Engine 三大组件。

• 工具选型：纯数学方程使用 Z3；含控制流的二进制用 angr；局部代码模拟或脱壳优先选 Unicorn；复杂环境结合两者使用。
• 关键操作：

使用 claripy 构建符号变量并管理约束。
配置 Hook 替换复杂函数，或使用 SimProcedure 简化外部调用。
利用 Concrete + Symbolic 混合模式加速执行，非符号部分由 Unicorn 原生运行。
运用 find/avoid 策略配合 LAZY_SOLVES 或 Veritesting 解决路径爆炸。

适用边界与注意点

• 环境配置：处理复杂二进制时需确认初始内存布局准确，必要时设置 auto_load_libs=False 以避免加载干扰。
• 异常排查：Z3 求解超时（unknown）通常源于非线性约束过复杂，建议拆解问题或设置超时参数。
• 兼容性：SimProcedure 需严格匹配调用约定（如 cdecl 或 fastcall），避免参数类型不匹配导致的错误。