符号执行与约束求解：让代码自己“跑”出漏洞
符号执行这东西，我第一次接触是在做固件安全审计的时候。当时有个二进制补丁，逆向分析看得我头大，后来用符号执行工具一跑，直接找到了一个隐藏了五年的缓冲区溢出。嗯，从那天起我就知道，这技术不是花架子。
说白了，符号执行就是让程序在“符号值”上运行，而不是具体的数字。你想想看，传统测试你给个输入，程序走一条路。符号执行不一样，它把所有可能的输入都抽象成符号，程序每遇到一个分支，两条路都走。这样就能覆盖所有执行路径。
符号执行的核心原理
我习惯把符号执行拆成三个部分来理解：
- 符号化输入：把输入变量变成符号，比如 x → α，y → β
- 路径约束收集：每经过一个条件分支，就把条件记录下来
- 约束求解：用求解器检查路径是否可达，生成具体测试用例
举个例子，你看这段代码：
int foo(int x, int y) {
int z = x + y;
if (z > 100) {
// 路径A
return z * 2;
} else {
// 路径B
return z / 2;
}
}传统测试你只能试几个值。符号执行会怎么做？它把 x 记作 α，y 记作 β，z 就是 α+β。走到 if 分支时，路径约束是 α+β > 100；走到 else 分支，约束是 α+β ≤ 100。然后约束求解器一算，就能给出具体的测试数据。
关键点：符号执行不是“猜”输入，而是用数学方式推导出能触发特定路径的输入值。
路径爆炸问题——绕不过去的坎
我在项目中遇到过最头疼的事，就是路径爆炸。一个循环跑100次，每次循环里有个if，那路径数就是2的100次方。这数字有多大？比宇宙中的原子数还多。你不可能全跑完。
为什么会这样？因为符号执行是穷举式的。每个分支点都分裂出两条路径，路径数随分支点指数增长。实际代码里，一个函数几十个分支点太常见了。
怎么解决？我常用的策略有这几个：
| 策略 | 做法 | 代价 |
|---|---|---|
| 路径剪枝 | 设定路径深度上限，超过就放弃 | 可能漏掉深层漏洞 |
| 符号合并 | 把多条路径的约束合并成一个公式 | 精度下降，可能误报 |
| 启发式搜索 | 优先探索“看起来有漏洞”的路径 | 依赖启发函数质量 |
| 混合执行 | 符号执行 + 具体执行交替进行 | 实现复杂 |
我的经验：实际项目中，我一般先用静态分析扫一遍，找出可疑点，然后只对这些点做符号执行。别上来就全量跑，那是给自己找麻烦。
约束求解器——符号执行的“发动机”
符号执行收集了一堆约束，谁来解？约束求解器。我主要用过两个：Z3 和 STP。
Z3——微软出品的全能选手
Z3 是微软研究院开发的，支持位向量、数组、字符串、浮点数……几乎你能想到的类型它都支持。我在做 Linux 内核驱动漏洞挖掘时，用的就是 Z3。它的 API 设计得很干净，C 语言调用起来也不费劲。
// 用 Z3 解一个简单的约束：x + y > 10 且 x < 5
Z3_context ctx = Z3_mk_context(config);
Z3_solver s = Z3_mk_solver(ctx);
Z3_symbol x_sym = Z3_mk_string_symbol(ctx, "x");
Z3_ast x = Z3_mk_const(ctx, x_sym, Z3_mk_int_sort(ctx));
Z3_symbol y_sym = Z3_mk_string_symbol(ctx, "y");
Z3_ast y = Z3_mk_const(ctx, y_sym, Z3_mk_int_sort(ctx));
// x + y > 10
Z3_ast sum = Z3_mk_add(ctx, x, y);
Z3_ast c1 = Z3_mk_gt(ctx, sum, Z3_mk_int(ctx, 10, Z3_mk_int_sort(ctx)));
// x < 5
Z3_ast c2 = Z3_mk_lt(ctx, x, Z3_mk_int(ctx, 5, Z3_mk_int_sort(ctx)));
Z3_solver_assert(ctx, s, c1);
Z3_solver_assert(ctx, s, c2);
Z3_lbool result = Z3_solver_check(ctx, s);
if (result == Z3_L_TRUE) {
Z3_model model = Z3_solver_get_model(ctx, s);
// 从 model 中提取 x 和 y 的值
}STP——轻量级位向量求解器
STP 专注于位向量和数组，速度比 Z3 快不少。如果你只处理整数运算和内存操作，STP 是更好的选择。我记得有一次跑一个网络协议解析器的符号执行，Z3 要 30 秒，STP 只要 8 秒。
不过 STP 的 API 比较简陋，文档也少。我建议新手先从 Z3 入手，等熟悉了约束求解的套路，再考虑 STP。
| 特性 | Z3 | STP |
|---|---|---|
| 支持类型 | 位向量、数组、字符串、浮点数、实数 | 位向量、数组 |
| 性能 | 通用，复杂约束较慢 | 位向量运算极快 |
| API 易用性 | 优秀，多语言绑定 | 一般，C 接口为主 |
| 社区活跃度 | 高，文档丰富 | 低，靠邮件列表 |
在漏洞挖掘中的应用
符号执行在漏洞挖掘里，主要干三件事：
- 生成测试用例：自动构造能触发特定路径的输入
- 验证漏洞可达性：静态分析报了个警告，符号执行能告诉你“这个漏洞到底能不能触发”
- 绕过保护机制：比如绕过 ASLR，符号执行可以计算出精确的偏移量
我曾经用符号执行挖过一个 HTTP 解析器的漏洞。静态分析报了个空指针解引用，但我不确定是不是误报。用符号执行一跑，约束求解器给出了一个具体的 HTTP 请求包——发过去，服务端直接崩溃。嗯，确认了，不是误报。
注意：符号执行不是银弹。遇到复杂的外部调用（比如系统调用、硬件交互），符号执行就抓瞎了。这时候需要结合具体执行，也就是混合执行（Concolic Testing）。
知识体系总览
下面这张图，是我自己总结的符号执行知识体系。你看一眼，心里就有谱了：
这张图把符号执行的三个核心环节串起来了。你从左往右看：先把输入符号化，然后一路走一路收集约束，最后交给求解器算出具体值。路径爆炸是最大的拦路虎，但也不是没办法对付。
我的建议：学符号执行，别一上来就啃理论。找个现成的工具（比如 KLEE、Angr），拿个简单的 C 程序跑一跑。看到工具自动生成测试用例的那一刻，你就明白这东西有多强了。
好了，符号执行的核心内容就这些。记住一句话：符号执行不是魔法，它只是用数学的方式，让代码自己“说”出它的漏洞。