8.1 符号执行原理与上手

8.1 符号执行原理与上手

本节摘要：符号执行的直觉只有一句话：让变量「同时取所有值」。变量不再是具体数字，而是带约束的符号；走到分支处，求解器判定哪条分支在约束下可行，于是「输入空间」被系统性地枚举成「路径空间」。本节先把这个直觉讲透——符号值、路径条件、约束求解三个概念配图落地；再直面它的宿命——路径爆炸，以及工程上的三类缓解外加实践者的第四招「缩小问题」；然后用 angr 把全流程跑通：编译一个自己的 crackme、加载、explore 探索、约束求解解出口令，并排一组常见报错的排查表；最后给 angr 的能力地图（VEX IR、CFG 恢复、去混淆、stripped 支持、GUI 与官方 MCP），并说清什么时候不该用它。样本全程自编译，分析在隔离环境进行。

学习目标

• 用符号值、路径条件、约束求解三个概念复述符号执行原理。
• 解释路径爆炸为什么不可避免，列出三类缓解思路与「缩小问题」。
• 独立完成 angr 加载、探索、求解口令的完整流程。
• 按常见故障排查表定位 explore 空手而归的原因。
• 按「能做与不该做」两端评估 angr 的适用性。

一、直觉：让变量同时取所有值

具体执行时，变量一次只有一个值，跑一遍只验证一条路径。符号执行换成符号值：令输入为符号 x，程序向前走，遇到 if x 大于 5，分支处不选择，而是分岔——左分支携带约束 x 大于 5，右分支携带 x 小于等于 5。走到任何一点，「当前状态」等于（符号取值空间，已累积的路径条件）。约束求解器随时可判定某条路径条件是否有解：无解，这条路径物理上不可达，直接剪掉。

# sym_tree.txt —— 符号执行的分岔与剪枝

                输入 x（符号值）
                     │
              if x > 5 ─────┬──────────────┐
                     │      │              │
              路径条件 x>5  路径条件 x≤5    │
                     ▼      ▼              │
                 分支 A   分支 B       求解器：两界皆有解
                     │      │           继续各自分岔
                     ▼      ▼
                 若 A 要求 x=0 ── 求解器：与 x>5 矛盾 ── 剪枝
​

对逆向工程的含义是颠覆性的：传统爆破是「猜一个值试一次」，符号执行是「让求解器反推出让程序走到目标处的那个值」——第 8.2 节的假设验证，反推的正是「什么输入让校验函数返回成功」。三个概念各记一句话：符号值是「还没定下来的输入」；路径条件是「走到这里必须成立的约束合取」；约束求解是「判定并反解这些约束的引擎」。

二、路径爆炸是宿命

符号执行的原罪叫路径爆炸：分支数随程序长度指数增长，一个循环跑二十圈、每圈两个分支，路径数就是六位数。更糟的是循环次数本身依赖输入时，路径可能无穷。工程缓解分三类，记住思路比记住名词重要：

• 限：探索深度上限、状态数上限、超时兜底——先保证「有限时间内出结果」。
• 并：把同一分支的多个状态合并处理（状态合并类技术），减少状态总数。
• 混：关键变量提前代入具体值（具体化），用「局部具体执行」换「全局可探索」。

实践者的真正解法其实是第四种：别探索整个程序，只探索目标函数。逆向校验逻辑时，从校验函数入口起跑而不是从 main 起跑，规模常常缩小两三个数量级——这个「缩小问题」的习惯，比任何参数调优都值钱。

三、angr 上手：从编译到解出口令

angr 是 Python 生态的符号执行与二进制分析平台（约 9.2k stars，BSD-2 许可证，要求 Python 3.12 以上，2026-10 社区口径）。先造自己的靶子：

// crackme.c —— 自编译练习样本：固定口令逐字节校验（教学用，自行补齐 include）
int check(const char *s) {
    const char *key = "AI4RE_2026";
    for (int i = 0; i < 10; i++)
        if (s[i] != key[i]) return 0;
    return 1;
}

int main(void) {
    char buf[32];
    if (scanf("%31s", buf) != 1) return 1;
    if (check(buf)) printf("Access granted\n");
    else            printf("Denied\n");
    return 0;
}
​

# build_crackme.sh —— 编译并 strip 出练习样本（Windows 下可用 MSYS2 或 WSL）
gcc -O0 -g crackme.c -o crackme
strip crackme      # 练习 stripped 场景
​

然后是 angr 全流程（API 细节以 angr 官方文档为准）：

# solve_crackme.py —— angr 符号执行：求解自编 crackme 的口令
import angr
import claripy

proj = angr.Project("./crackme", auto_load_libs=False)
flag = claripy.BVS("flag", 8 * 16)          # 16 字节符号口令

state = proj.factory.full_init_state(
    stdin=angr.SimFileStream(content=flag, name="stdin"),
    add_options={angr.options.unicorn},      # 引擎加速，可选
)
simgr = proj.factory.simulation_manager(state)
simgr.explore(
    find=lambda s: b"Access granted" in s.posix.dumps(1),
    avoid=lambda s: b"Denied" in s.posix.dumps(1),
)

if simgr.found:
    print("口令:", simgr.found[0].solver.eval(flag, cast_to=bytes))
else:
    print("未找到：检查字符串、长度假设或换用目标函数入口起跑")
​

四步读法：Project 加载二进制并做指令提升；BVS 声明符号输入；full_init_state 构造带符号标准输入的初始状态；explore 用 find 与 avoid 两个谓词驱动探索——找到输出成功串的状态就停，碰到输出失败串的分支就剪。found 非空时，solver.eval 反解出符号值，就是那把钥匙。

常见故障排查（explore 空手而归时按序检查）：

四、能力地图：angr 不只是解题器

把 angr 只当 crackme 解题器是低估。它的能力栈至少四层：

• 表示层：VEX IR 把各架构指令提升为统一中间语言——x86、ARM 在引擎眼里无差别。
• 恢复层：CFG 恢复（proj.analyses.CFG）从 stripped 二进制重建函数边界与调用图，第 7.3 节的二进制图可以由此互相印证。
• 分析层：符号执行之外还有去混淆辅助（识别扁平化控制流的模式）。
• 交互层：angr-management 图形界面；官方还提供 MCP server，把反编译、CFG、交叉引用做成模型可调用的工具（第 8.2 节展开）；其反编译输出支持多语言风味（如按 Go、Rust 习惯渲染），细节以官方文档为准。

五、什么时候不该用

三类场景符号执行不划算：循环次数巨大或数据依赖复杂（AES、压缩、哈希）——约束规模爆炸；重度反调试与自修改代码——状态空间被刻意污染；只需要观察行为而非反推输入——直接动态调试更快（第 8.3 节）。成熟研究者的常态是混合：符号执行定位关键分支与约束，动态调试确认真实行为，两者结论互相背书。所有对未知或第三方样本的运行，一律在隔离环境进行（纪律见《Agent 沙箱与运行时隔离》第 02 章）。

本节要点回顾

• 符号值加路径条件加约束求解：把「猜输入」变成「反推输入」。
• 路径爆炸不可消灭，只能限、并、混，以及最有效的「缩小问题」。
• angr 四步：Project、BVS、full_init_state、explore 加 find 与 avoid；空手而归先查串与绑定。
• 加密与重度混淆场景不硬刚，符号与动态混合是常态。

手工流程跑通了，但每换一个样本就要重读伪代码、重猜成功串与长度——这正是大模型擅长而人嫌烦的环节。下一节把「读代码提假设」交给 LLM，「跑求解器下结论」留给 angr，拼出本章的核心闭环。