符号执行基础理论：符号变量与具体值、路径约束与求解器、执行树与状态空间
好，咱们进入正题。符号执行这东西，说白了就是让程序「带着问号跑」。你想想看，平时我们调试程序，都是给具体的输入值，比如传个整数 5，或者字符串 "admin"。但符号执行不一样——它给程序一个符号变量，比如 α，然后看程序怎么处理这个未知数。
我个人习惯把符号执行比作「侦探破案」。具体执行是看结果，符号执行是看过程。嗯，咱们一个一个来拆解。
符号变量与具体值
先搞清楚最基础的概念：符号变量和具体值有什么区别？
具体值，就是实实在在的数字、字符串。比如 int x = 10;，这个 x 就是具体值。你给它加 1，结果一定是 11。
符号变量呢？它是个「占位符」。比如 int x = α;，这个 α 代表「任意可能的整数」。你给它加 1，结果就是 α+1——还是一个符号表达式。
我在项目中遇到过一种情况：用具体值测试时，某个漏洞死活复现不出来。后来换成符号执行，才发现那个漏洞需要输入满足一个非常复杂的条件——比如 a > 100 && b < 50 && a + b == 200。用具体值去猜？累死你。符号变量直接帮你把条件列出来，交给求解器去算。
核心区别一句话：
- 具体值：已知的、确定的数值。程序跑一遍，结果唯一。
- 符号变量：未知的、抽象的符号。程序跑一遍，结果是一堆表达式。
举个简单的代码例子：
int foo(int x) { // x 是具体值还是符号变量？
int y = x * 2;
if (y > 100) {
return 1;
} else {
return 0;
}
}如果 x 是具体值，比如 x=60，那 y=120，走 true 分支，返回 1。如果 x 是符号变量 α，那 y=2α，路径条件就是 2α > 100 或 2α <= 100。求解器会告诉你：α > 50 时走 true，α <= 50 时走 false。
我的小技巧：刚开始学符号执行时，可以把符号变量想象成「代数里的 x」。你解方程时不会把 x 换成具体数字，对吧？符号执行也一样——保持变量为符号，直到最后让求解器去算。
路径约束与求解器
好，现在程序带着符号变量跑起来了。每遇到一个分支，就会产生一个「路径约束」。路径约束就是程序走到当前这条路径必须满足的条件集合。
我曾经踩过一个坑：以为路径约束就是简单的 if 条件。其实不是。路径约束是累积的。你想想看，程序经过多个 if 之后，路径约束是所有分支条件的「与」组合。
比如这段代码：
void check(int a, int b) {
if (a > 0) {
// 路径约束1: a > 0
if (b < 10) {
// 路径约束2: a > 0 && b < 10
if (a + b == 50) {
// 路径约束3: a > 0 && b < 10 && a + b == 50
crash(); // 目标路径
}
}
}
}要触发 crash()，必须同时满足三个条件。这就是路径约束的威力——它把多个条件串联起来，形成一个逻辑公式。
那求解器是干嘛的？说白了，求解器就是「解方程的工具」。你把路径约束扔给它，它告诉你：有没有解？如果有，具体值是什么？
| 求解器类型 | 能解什么 | 常见工具 |
|---|---|---|
| SMT 求解器 | 整数、实数、位向量、数组、字符串 | Z3, CVC4, Yices |
| SAT 求解器 | 布尔逻辑公式 | MiniSat, Glucose |
| 约束求解器 | 特定领域的约束（如路径条件） | STP, Boolector |
注意：求解器不是万能的。遇到非线性运算（比如乘法、除法、三角函数），求解器可能算不出来，或者算得很慢。我遇到过最头疼的情况是：路径约束里有个 a * b == 100，Z3 直接超时。后来改成位向量表示才搞定。
嗯，这里要注意：路径约束和求解器是符号执行的「心脏」。没有求解器，符号变量就只是一堆没用的符号。没有路径约束，求解器也不知道该解什么方程。
执行树与状态空间
最后聊聊执行树和状态空间。这两个概念其实是一体两面。
执行树：程序所有可能执行路径的树形表示。每个节点代表一个程序状态（比如当前执行到哪一行、变量值是什么），每条边代表一次执行步骤（比如赋值、分支）。
状态空间：所有可能程序状态的集合。说白了，就是执行树里所有节点的集合。
为什么要把这两个概念拎出来？因为符号执行本质上就是在「遍历执行树」或「探索状态空间」。
我刚开始做符号执行时，以为就是把所有路径都跑一遍。后来发现——天呐，路径数量是指数级增长的！每多一个 if，路径数就翻倍。10 个 if 就是 1024 条路径，20 个 if 就是 100 万条。这还只是理论值，实际程序里循环、递归更可怕。
举个例子：
void example(int n) {
int x = 0;
for (int i = 0; i < n; i++) {
if (x % 2 == 0) {
x = x + 1;
} else {
x = x * 2;
}
}
}这个循环每迭代一次，就有两个分支。如果 n=10，路径数就是 2^10 = 1024。如果 n=20，就是 100 多万条。符号执行要处理这么多路径？不现实。
所以实际中怎么搞？
- 路径剪枝：如果某条路径的约束已经无解（比如
a > 0 && a < 0），直接扔掉，不往下探索。 - 状态合并：把多个相似的状态合并成一个。比如两个状态只有变量值不同，但路径约束一样，可以合并。
- 启发式搜索：不遍历所有路径，而是优先探索「看起来有戏」的路径（比如离目标代码近的路径）。
我个人习惯用「深度优先 + 路径剪枝」的组合。先沿着一条路径走到黑，如果发现约束无解，就回溯。这样内存占用小，适合找特定漏洞。
但要注意：深度优先可能漏掉某些路径。如果你在做「全覆盖测试」，那最好用广度优先或随机搜索。
避坑指南：我曾经在一个 CTF 题目里用符号执行找漏洞，结果跑了 3 个小时没出结果。后来发现是循环次数太大，状态空间爆炸了。解决办法是「循环展开」——把循环手动展开成有限次，或者设置最大迭代次数。嗯，从那以后我写符号执行脚本时，都会先估算一下状态空间的大小。
总结一下今天的内容：
- 符号变量 vs 具体值：符号变量是「未知数」，具体值是「已知数」。符号执行用符号变量代替输入，让程序跑出表达式。
- 路径约束与求解器：路径约束是程序走到某条路径必须满足的条件。求解器负责解这些条件，给出具体输入值。
- 执行树与状态空间：执行树是所有路径的树形表示，状态空间是所有状态的集合。实际中要避免状态爆炸，用剪枝、合并、启发式搜索来优化。
下节课咱们会讲「符号执行引擎的架构」，到时候我会拿一个真实的开源工具来拆解。你想想看，一个符号执行引擎到底是怎么把代码变成约束，再交给求解器的？嗯，到时候见分晓。