Symbolic Execution 发现了我 94% 测试覆盖率都遗漏的整数溢出

你的测试套件有 94% 的覆盖率，零失败。一个 symbolic execution 引擎在三秒内就在你的代码中找到了一个崩溃。

测试没有坏。覆盖率指标没有说谎。问题在于测试只验证特定点上的行为。Symbolic execution 验证的是整个输入区域上的行为。无论你写多少示例，如果 bug 藏在两个示例之间的缝隙里，测试就抓不住。

Symbolic Execution 到底做了什么

Symbolic execution 是一种程序分析技术，它在 symbolic 变量而非具体值上运行你的代码。普通测试把 x = 5 传给一个函数，symbolic execution 引擎则传入 x = α，其中 α 代表每一个可能的整数。

当代码运行时，引擎追踪约束。当它遇到一个像 if (x > 0) 的分支时，它不选择方向。它分叉执行。一条路径携带约束 α > 0，另一条携带 α ≤ 0。两条路径独立继续。

当一条路径到达断言、内存访问或潜在的崩溃点时，引擎向 SMT solver 提出一个简单的问题：“是否存在一个 α 的值，能满足这条路径上的所有约束，同时违反这条安全属性？” 如果 solver 回答有，它就会返回一个具体的反例。现在你拥有了一个能触发你从未写过的测试才能发现的 bug 的特定输入。

你的单元测试抓不住的 Bug

考虑一个在复制前验证数组边界的函数：

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

你的测试套件看起来是合理的：

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

全绿。但 offset 和 count 是 size_t，无符号整数。在 64 位系统上，如果两个值都很大，offset + count 可能会回绕成一个小数字。如果 offset = 0xFFFFFFFFFFFFFFFF 且 count = 1，那么 end = 0，并不大于 src_len。边界检查通过了。memcpy 从无效地址读取。

没有哪个合理的开发者会写一个 offset = 2^64 - 1 的测试用例。输入空间大到无法理解。Symbolic execution 不需要你猜出那个坏输入。它探索发生回绕的路径，并要求 solver 找出满足约束 end ≤ src_len 同时 offset + count 溢出的值。Solver 在几毫秒内就返回了反例。

引擎如何探索路径

核心机制是约束收集和路径分叉。你代码中的每一条条件语句都成为一个分支点。引擎维护一个路径约束，这是一个布尔公式，代表执行到达当前点必须满足的所有条件。

在每个分支处，引擎查询 solver：

当前路径约束加上 true 分支条件是否可满足？
当前路径约束加上 false 分支条件是否可满足？

如果两者都可满足，引擎就分叉。它将两条路径都加入探索队列。Symbolic execution 正是通过这种方式为有限程序实现穷尽路径覆盖的。

当一条路径到达崩溃、越界访问或断言失败时，引擎要求 solver 在当前路径约束下给出一个 symbolic 输入的满足赋值。这个赋值就是你触发 bug 的输入。

你可以直接用 Z3——那个驱动许多 symbolic execution 引擎的 SMT solver——来观察约束求解的步骤：

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

Solver 返回满足溢出约束的具体值。这就是 symbolic execution 的数学核心。引擎自动对你程序中的每个分支执行这一过程。

让它无法取代你测试套件的权衡

Symbolic execution 不是免费的。有三个成本限制了它的实用范围。

路径爆炸。 每条 if 语句都会让路径数量翻倍。一个包含 20 个独立分支的函数有超过一百万条路径。大多数引擎在超时或路径预算耗尽后放弃。循环让情况更糟。一个对无界范围进行 symbolic 迭代的循环会产生无限多条路径。引擎通常将循环展开固定次数然后继续。

外部状态和系统调用。 Symbolic execution 在纯函数上效果最好。当你的代码读取文件、发起网络请求或查询数据库时，引擎不知道会返回什么值。有些工具启发式地建模常见库调用。另一些要求你编写 mock models。这既繁琐又容易出错。

Solver 超时。 真实代码的约束公式很复杂。数组、bitvectors、浮点运算和非线性数学都可能把 SMT solver 推向指数级时间。一条在具体执行中只需微秒的路径，在 symbolic 执行中可能需要数分钟来求解。引擎会丢弃这些路径并将它们报告为未解决。

由于这些限制，symbolic execution 是测试的补充，而不是替代。它发现深层的边角案例。你的测试验证常见案例和集成行为。

在真实代码上尝试它的三种方式

你不需要博士学位就能运行 symbolic execution。现代工具隐藏了大部分复杂性。

针对 C/C++：KLEE。 KLEE 是构建在 LLVM 上的经典开源 symbolic execution 引擎。你用 clang -emit-llvm 将代码编译为 LLVM bitcode，然后在结果上运行 klee。KLEE 在 GNU coreutils、SQLite 和其他广泛使用的 C codebases 中发现过严重 bug。

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEE 为每个发现的 bug 输出 .ktest 文件。你可以用一个小运行时来回放它们，查看确切的输入。

针对 Python 和二进制文件：angr。 angr 是一个用于 symbolic execution、二进制分析和逆向工程的 Python 框架。它在编译后的二进制文件上工作，所以你不需要源代码。你编写一个 Python 脚本来设置 symbolic 寄存器和内存，然后让 angr 探索。

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr 比 KLEE 慢，但能处理真实世界的二进制文件及其混乱的调用约定和库依赖。

针对 Rust：Kani。 Kani 是一个构建在 CBMC 上的 Rust 专用验证器。你用 #[kani::proof] 注解一个函数，然后运行 cargo kani。它在底层使用 symbolic execution 来检查算术溢出、越界访问和断言失败。

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

如果你已经在 Rust 生态系统中，Kani 是最容易上手的入口。它与 cargo 集成，并以熟悉的格式提供错误追踪。

常见问题

Symbolic execution 会取代 fuzzing 吗？

不会。Fuzzing 生成随机输入并观察崩溃。Symbolic execution 对路径进行推理，找出满足特定约束的输入。Fuzzing 能扩展到大型程序和长时间运行。Symbolic execution 在更小的区域内发现更深层的 bug。这两种技术配合得很好。像 Driller 和 QSYM 这样的工具将它们结合起来，用 fuzzing 做覆盖率，用 symbolic execution 攻克难以到达的分支。

Symbolic execution 能证明我的代码没有 bug 吗？

只能针对没有无界循环和没有外部依赖的有限程序。对于大多数生产代码，symbolic execution 可以在路径深度限制内证明某些 bug 类别的不存在。它不能证明完全正确性。

运行需要多长时间？

小函数需要几分钟到几小时。Symbolic execution 不是 CI 速度之王。在关键的安全函数、解析器和边界检查代码上运行它。不要试图对你的整个 web 框架做 symbolic execution。

从一个函数开始

你不需要对你的整个 codebase 做 symbolic execution。选一个 bug 会造成伤害的函数。一个解析器。一个授权检查。一个缓冲区拷贝。

写一个 KLEE harness、一个 angr 脚本或一个 Kani proof。运行它。看着它找出一个你永远不会写测试用例的输入。修复 bug。睡个好觉。

目标不是取代你的测试。目标是别再假装 94% 的覆盖率意味着 94% 的安全。Symbolic execution 发现缝隙。你的测试永远做不到。