KLEE — 用符号执行自动给复杂系统程序生成高覆盖测试

是什么

KLEE 是一个自动给 C 程序找测试输入的工具。日常类比：像你检查迷宫，不是随便丢几颗石子看会滚到哪里，而是在每个岔路口都贴一张便签：“要走左边，输入必须满足什么条件；要走右边，输入又必须满足什么条件”。

普通运行只拿一个具体输入，比如 argv[1] = "abc"。KLEE 把输入先看成”可以是任何值”的符号变量，程序每遇到 if 就把条件记下来，最后让约束求解器给出一组真实输入，让原程序沿着同一路径再跑一遍。

这篇 OSDI 2008 论文的关键不是”符号执行第一次出现”，而是证明它能跑在真实系统程序上：GNU Coreutils、BusyBox、MINIX、HiStar 这类和文件、参数、系统调用强相关的代码。

为什么重要

不理解 KLEE，下面这些事都没法解释：

• 为什么测试可以从”人想案例”变成”机器枚举路径并吐出输入”
• 为什么约束求解器能把 x > 0 && x < 10 && x != 5 变成一个具体测试值
• 为什么 GNU Coreutils 这种老牌工具套件还有深层 bug 能被自动挖出来
• 为什么安全研究里符号执行常和 fuzzing、静态分析并列成三大武器

核心要点

KLEE 的工作可以拆成 三步：

1. 符号执行：把输入当未知数跑程序。类比：做数学题时先写 x，不急着填数字。程序执行到分支时，KLEE 不只选一边，而是为两边各保存一份状态和路径条件。

2. 约束求解器：把路径条件变成真实输入。类比：你写下”这把钥匙要比 3 大、比 8 小、不能等于 6”，求解器告诉你”拿 4 就行”。KLEE 当年主要借助 STP 处理位级约束，所以能精确到 C 程序里的整数溢出和按位运算。

3. 搜索策略：在爆炸的路径里挑有价值的先跑。类比：逛大楼时不可能一秒走完所有房间，先去没去过的楼层和门最多的走廊。KLEE 用覆盖导向的启发式、状态压缩和求解缓存，把指数级路径爆炸压到工程上可跑。

实践案例

案例 1：一个 if 怎么生成两个测试

int check(char c) {
  if (c == 'K') return 1;
  return 0;
}

逐部分解释：

• 普通测试如果只传 'A'，只能覆盖 return 0
• KLEE 把 c 当符号值，看到 c == 'K' 就分出两条路
• 求解器给第一条路生成 c = 'K'，给第二条路生成任意非 K 的字符
• 于是机器自动得到两个测试，覆盖两个分支

案例 2：约束求解器不是猜，是解方程

int gate(unsigned x) {
  if ((x & 7) == 3 && x < 20) return 42;
  return 0;
}

逐部分解释：

• (x & 7) == 3 不是普通大小比较，而是位运算约束
• x < 20 再加一道范围限制
• STP 这类求解器能直接处理位向量，给出 x = 3、x = 11、x = 19 这样的可行值
• 这就是 KLEE 比随机测试强的地方：它不靠撞运气，而是把条件翻成数学问题

案例 3：KLEE 测一个迷你程序的大致形状

#include <klee/klee.h>

int main() {
  char input[4];
  klee_make_symbolic(input, sizeof(input), "input");
  if (input[0] == '-' && input[1] == 'x')
    klee_assert(input[2] != 0);
  return 0;
}

逐部分解释：

• klee_make_symbolic 把 4 个字节声明成”都可以变”
• 分支要求前两个字节分别是 - 和 x
• 断言要求第三个字节不能是 0；KLEE 会问求解器：“有没有输入能让它等于 0？”
• 如果有，KLEE 生成一个可复现的测试文件，普通编译后的程序也能跑出同样错误

踩过的坑

1. 把高覆盖当成完全正确：覆盖率只说明”走过很多代码”，没写断言或没有可观察崩溃时，逻辑错误仍可能安静通过。
2. 忘了路径爆炸：每个符号分支都可能复制状态，循环和解析器最容易把路径数量放大到不可控。
3. 环境模型写得太理想：文件系统、命令行参数、系统调用如果被简化过头，生成的测试可能漏掉真实运行里的边界情况。
4. 求解器卡住就以为程序没 bug：复杂位运算、大数组和浮点会让求解变慢；超时只说明工具没探索到，不说明代码安全。

适用 vs 不适用场景

适用：

• C/C++ 系统工具、解析器、命令行程序这类输入边界多的代码
• 想自动生成回归测试，并且希望测试能在原始二进制上复现
• 安全审计里的崩溃、越界访问、断言失败、差分测试
• 需要证明某条已探索路径上不存在断言反例的局部性质

不适用：

• 大量并发、网络时序、非确定性行为主导的系统
• 强依赖浮点、GPU、内联汇编或未建模外部库的程序
• 只关心性能瓶颈而不是功能路径覆盖的场景
• 想一次性证明整个程序完全正确；那是验证工具和规格语言的任务

历史小故事（可跳过）

• 1970s：King 提出 symbolic execution，核心想法已经出现，但机器和求解器都太弱。
• 2005 年前后：DART、EXE、CUTE 等工具把符号执行重新带回系统测试和安全研究。
• 2008 年：Cadar、Dunbar、Engler 在 OSDI 发表 KLEE，展示真实 Unix 工具上的高覆盖和 bug 发现能力。
• 2010s：KLEE 成为研究基线，后续 SAGE、angr、S2E、Mayhem 等工具继续扩展二进制分析和混合执行。
• 今天：符号执行常和 fuzzing 组合使用：fuzzer 负责高速乱撞，KLEE 负责解开难分支。

一个常被混淆的点：高覆盖不等于完全正确

KLEE 最亮眼的实验是覆盖率：Coreutils 总体行覆盖达到 80% 以上，单工具平均超过 90%，还超过了维护多年的手写测试套件。

但覆盖率不是正确性证明。一个程序即使每一行都跑过，如果没有断言、没有 oracle、没有和另一份实现对比，很多”结果不符合需求”的 bug 仍然不会自动显形。

论文里最聪明的延伸是 cross-check：把 BusyBox 和 GNU Coreutils 中号称等价的工具喂同样输入，看输出是否一致。这样 KLEE 不只找崩溃，还能找功能差异。

学到什么

1. 测试输入可以被”求”出来：符号执行把程序路径变成约束，求解器把约束变成真实输入。
2. 工程化比理论更难：KLEE 的贡献在状态管理、约束缓存、搜索策略、环境模型，而不只是教科书里的符号执行。
3. 系统程序的边界就是 bug 富矿：参数、文件、权限、系统调用失败，正是手写测试最容易漏的地方。
4. 安全价值来自可复现：KLEE 生成的是具体测试，开发者可以用普通工具复现、调试、加入回归套件。

延伸阅读

• 论文 PDF：KLEE OSDI 2008（原文 16 页，实验部分很值得看）
• USENIX 页面：KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs（会议归档页）
• 工具文档：KLEE Documentation（安装、教程、API）
• llvm —— KLEE 把 C 程序编到 LLVM bitcode 后解释执行
• davis-putnam-1960 —— 约束求解器背后的 SAT/SMT 思想源头之一

关联

• llvm —— KLEE 的输入是 LLVM bitcode，靠统一 IR 避开多语言前端差异
• davis-putnam-1960 —— 约束求解最终要判断一组逻辑条件能否同时成立
• dpll-1962 —— 现代 SAT 求解器的回溯搜索骨架
• chaff-2001 —— 工业 SAT 求解性能跃迁，让自动分析工具更实用
• z3-2008 —— 和 STP 同时代的 SMT 求解器，支撑大量验证工具
• boogie-2005 —— 同样把程序问题翻译成逻辑约束，再交给求解器

反向链接

• aflgo-2017 —— AFLGo — 让灰盒 fuzzing 朝目标代码前进
• bohme-aflfast-2016 —— AFLFast — 把 fuzzing 的力气花在更少人走的路径上
• driller-2016 —— Driller 2016 — 用符号执行给 fuzzing 打穿深分支
• fairfuzz-2018 —— FairFuzz 2018 — 保护关键字节，让 fuzzing 往深处走
• making-smart-contracts-smarter —— Making Smart Contracts Smarter — Oyente 用符号执行给智能合约找漏洞