一、符号执行

1. 静态符号执行

定义

符号执行是一种程序分析技术，它通过使用符号代替实际的运行时值来探索程序的所有可能执行路径。这种技术不仅可以帮助生成覆盖率高的测试用例，还能有效地发现潜在的程序错误。

具体地，符号执行采用抽象的符号代替具体值作为程序输入变量，得出每个路径抽象的输出结果和需要满足的约束条件。通过约束求解器，可以反推出指定程序路径时，程序输入应该设置的具体值。

这种传统的符号执行不需要运行程序，所以也称为静态符号执行，它与 fuzz 测试相比各有优劣。举例来说，当我要求如下程序触发 AssertionError 时：

1
2
3
4
5
def f():
    x = int(input())
    y = x * 2
    if y == 12:
        assert False

如果使用 fuzz 测试，由于 x 是随机输入，为了满足y==12，fuzz 需要进行大量的尝试。

如果使用符号执行，要触发 AssertionError 只需要满足约束条件 2*x==12 即可，求解可得x==6，一次分析即可搞定。

原理

符号执行包括三个核心组件：

  • 状态信息存储器
    • σ：程序变量的符号表达式
    • π：路径约束，即走到特定语句所经过的条件组合
    • stmt：指向需要处理的下一条程序语句
  • 语句执行器：执行 stmt 指向的语句，更新 σ 或π的状态
  • 约束求解器：根据路径约束 π 和符号表达式σ，求出可行解

下图演示了符号执行过程中，各组件的变化情况：

缺陷

只需一次分析，即可获得所有路径的可行解，这个理想很美好，但现实很骨感。 静态符号执行在实际应用中，面临两大挑战：

1. 路径爆炸

程序中的分支和循环，都会使得程序路径爆炸式增长，导致分析过程变得不可行：

  • 每增加一次条件判断，程序会产生两个分支，极端情况下，路径数量呈指数增长
  • 无限循环和递归调用，可能导致无穷长的路径
    1
    2
    3
    4
    5
    6
    7
    def func():
        s = 0
        x = int(input())
        while x > 0:
            s += x
            print(f'total sum: {s}')
            x = int(input())

处理路径爆炸问题的思路主要是限制分析的搜索空间，例如设置超时机制、搜索次数，使用启发式搜索等策略。

2. 约束不可解

符号执行中的关键环节在于约束求解器求解约束条件。学过数学的都知道，解不出来的方程可太多了。在程序中会面临更复杂的情况：

  • 程序调用无源码函数

    1
    2
    3
    4
    def func(x, y):
        z = do_something(x)
        if y + z < 0:
            print('error')

  • 不可解的非线程约束条件

为了处理不可解的场景，动态符号执行诞生了，它将具体值与符号值结合，在符号值解不了的场景，用具体值代替，达到化简约束、降低求解难度的目的。

2. 动态符号执行

静态符号执行不需要运行程序，动态符号执行则是要设置输入，启动程序，让程序跑起来。在程序运行过程中，程序的变量在理论上都有两种取值，一种是符号值，一种是具体值。

在实现上，根据两种取值的配合方式，动态符号执行可分为两种路线：

Concolic Testing

在这种测试方法中，每个变量同时保留了符号值和具体值。在求解约束条件时，如果用符号值表达的约束条件解不了，那就将具体值代入对应的符号变量，化简条件再求解。

此外，这种测试方法在一条路径探索结束后，会通过对条件约束进行取反操作，切换到其他的执行路径，再继续进行探索。

Execution-Generated Testing

在这种测试方法中，每个变量值保留符号值和具体值中的一个状态。程序中的任何一个运算，如果所有相关变量都是具体值，那就使用具体执行；如果有任何一个变量是符号值，那就使用符号执行。

缺陷

没有完美的方案，动态符号执行虽然能缓解约束不可解的问题，但是使用具体值简化，也可能导致部分可执行路径无法被探索到。

1
2
3
4
def func(x):
    y = do_something(x)
    if y > 0:
        print('error')

由于 do_something 的源码未知，使用静态符号执行无法求解，动态符号执行会用 x 的具体值来计算 y。假设算出来y==-1，那么if 的判断条件由于矛盾而终止，导致 error 不可达。

为了解决这个问题，需要不断地更换 x 的具体值。从这个角度来看，将 Fuzz 和动态符号执行结合起来，是一件自然而然的事情，于是就有了混合模糊测试技术（Hybrid Fuzzing)。

3. 参考资料

  1. 符号执行入门
  2. Symbolic Execution for Software Testing Three Decades Later
  3. A Survey of Symbolic Execution Techniques
  4. 北京大学 - 软件分析技术 - 第 19 课
  5. Using Klee and Angr

二、混合模糊测试

1. 原理与架构

Fuzz 测试与符号执行互有优劣，在一定程度上是互补关系。

技术 优点 缺点
Fuzz 测试 随机变异，运行速度快 难以深入复杂的执行路径，代码覆盖率有限
符号执行 对程序进行分析和推理，可以突破复杂的路径约束 运行速度慢，资源消耗大

混合模糊测试结合二者的长处，通过 Fuzz 测试随机生成大量输入来测试程序的浅层代码，再结合动态符号执行来探索程序的深层路径，提升整体的代码覆盖率。

混合模糊测试的常见架构设计如下：

在 Fuzz 引擎和符号执行引擎之外，还有一个关键组件 Coordinator，其作用主要为协调 Fuzz 与符号执行的相互配合。

Fuzz 测试与符号执行在执行速度与资源消耗方面都有很大区别，这个差异还会随着 target 而各有不同。如何设计一个好的 Coordinator，让运行时的性能最优，是混合模糊测试需要考虑的一个关键因素。

2. SymCC

SymCC是一款开源的动态符号执行工具，通过在编译时插桩，为每个变量构建符号表达，在运行时，缩短符号推理计算的时间，相比此前的符号执行工具（如 KLEE 和 QSYM）性能有明显提升。

SymCC 由于出色表现，已被 LibAFL 官方集成。SymCC 本身提供了一个 symcc_fuzzing_helper 工具，简单快速的支持混合模糊测试功能，其核心代码为：

这段代码的主要逻辑为：每隔 5 秒检查 AFL 的corpus目录，如果 AFL 有产生新的测试用例，那么就将这个测试用例发给 symcc，symcc 基于这个测试用例开始动态符号执行。

使用 SymCC 进行混合模糊测试的步骤请见参考资料。能顺利跑起来的开源项目不多，SymCC 必须给个好评。

3. 参考资料

  1. Exploratory Review of Hybrid Fuzzing for Automated Vulnerability Detection
  2. Symbolic execution with SymCC: Don’t interpret, compile!
  3. 符号执行 Symcc 与模糊测试 AFL 结合实践