论文阅读--"Symbolic Execution for Software Testing"

该论文以较为通俗的语言和简单的例子阐述了符号执行的基本原理，并介绍了符号执行技术的发展历程和面临挑战。通过本文，可以基本的了解符号执行
论文地址：https://dl.acm.org/doi/fullHtml/10.1145/2408776.2408795

软件测试环境中，符号执行的一个关键目标是在一定的时间内探索尽可能多的不同程序路径，并为每一条路径：

（1）生成一组具体的输入值来执行该路径

（2）检查是否存在各种错误，包括断言违规、未捕获的异常、安全漏洞、内存损坏等

符号执行关键思想

关键思想

符号执行关键思想：使用符号值，而不是具体的数据值作为输入，并将程序变量的值表示为符号表达式，而不是符号输入值。那么，程序的输出值为符号输入值的一种函数 function(symbolic_input_values)。

程序表达方式

具体而言，符号执行为程序每个执行路径生产测试用例。而程序的执行路径可以分为true和false的序列，在序列的第i个位置为true则表示第i个条件判断语句执行then分支，若为false则执行else分支。

每个程序的执行路径都可以用执行树来表达，后面会通过例子理解。

符号执行的目标就是生成一组输入，在一定的时间内遍历尽可能多的路径。

符号执行思路与过程

符号执行拥有两个变量：

符号状态 σ ：表示变量到符号表达式的映射集合
符号路径约束 PC ：是符号表达式的无量词的一阶式

在符号开始之前，符号状态 σ 为空集，PC 初始化为 True

当一条路径执行结束时，使用约束求解器求解PC，可以生成具体的输入值。（对于该输入值，如果程序以其作为输入，程序将执行与符号执行完全相同的路径并以相同的方式终止）

那么符号状态 σ和符号路径约束 PC是怎么变化的呢？

例子

int twice(int v) {
    return 2 * v;
}

void testme(int x, int y) {
    z = twice(y);
    if (z == x) {
        if (x > y + 10)
            ERROR;
    }
}

int main() {
    x = sym_input();
    y = sym_input();
    testme(x, y);
    return 0;
}

可以看到void testme(int x, int y)函数存在三条执行路径；上图表示这对应的执行树。

当符号执行开始执行时：

符号状态 σ = 空集
符号路径约束 PC = True

当符号执行遇到一个输入语句时，形式为var = sym_input()，符号执行将为符号状态σ添加映射： $var \rightarrow s$

其中 $s$ 是一个新的未约束的符号值。

例如，对于上面的例子，在执行第16、17行：

...
 x = sym_input();
 y = sym_input();
...

后，符号状态 $\sigma=\{x \rightarrow x_0,y \rightarrow y_0\}$ ，其中$x_0，y_0$是新的未约束的符号值。

当符号执行遇到一个赋值语句时，形式为v = e，符号执行将为符号状态σ添加映射： $v \rightarrow \sigma(e)$ ，其中$σ(e)$就是在当前符号化状态计算e得到的符号表达式。

例如，对于上面的例子，在执行第6行：

int twice(int v) {
    return 2 * v;
}
    z = twice(y);

后，符号状态 $\sigma=\{x \rightarrow x_0,y \rightarrow y_0\, z \rightarrow 2y_0\}$

当符号执行遇到一个条件语句if(e) S1 else S2，PC会有两种更新：
1. 首先更新PC（表示then分支）为： $PC = PC \Lambda \sigma(e)$
2. 之后建立一个路径约束(else语句)PC‘： $PC^{'} = PC \Lambda \lnot\sigma(e)$
- 如果PC可以满足对符号值的某些分配，给一些实际值，那么符号执行继续沿着then这条分支执行下去，且符号状态为σ和符号路径约束为PC；
- 同样，如果PC’可满足，PC‘则使用符号状态σ和符号路径约束PC’创建另一个符号执行的实例，并沿着“else”分支继续执行；
- 与直接执行程序所不同的是，符号执行的两个分支都可以执行，从而产生两条路径；如果没有满足的分支PC，符号执行将终止

例如，对于上面的例子：

z = twice(y);
if (z == x) {
    if (x > y + 10)
        ERROR;

在第7行，会创建两个路径约束实例，路径约束分别为：

$x_0 = 2y_0$ 和 $x_0\neq2y_0$

在第7行，会创建两个路径约束实例，路径约束分别为：

$(x_0 = 2y_0)\Lambda(x_0>y_0+10)$ 和 $(x_0 = 2y_0)\Lambda(x_0 \leq y_0+10)$

当符号执行遇到exit语句或错误（程序崩溃、违反断言等），将终止符号执行的当前实例，利用约束求解器对当前符号路径约束PC得到一个可满足的值，该值就构成了测试用例输入。即：如果程序执行这些可满足的实际值，就会采用与符号执行完全相同的路径，并以相同的方式结束。
当符号执行遇到循环和递归时，符号执行可能会导致无限多条路径，如下图：

这段代码就有无数条执行路径，每条路径的可能性有两种：①任意数量的True加上一个False结尾；②无穷多数量的True。

对于这种情况：

符号路径约束 $PC =(\wedge_ {i\in [1,n]}N_{i} >0) \wedge (N_{n+1}\leq 10)$ 其中每个$N_{i}$都是一个新的符号值

执行结尾符号状态 $\sigma =\{N \rightarrow N_{n+1} , sum \rightarrow \sum Ni\}$

在实践中，需要对搜索进行限制（时间超时、路径数、循环迭代次数、搜索深度等）

静态符号执行的缺点

关键缺点：当符号执行得到的约束不能被约束求解器求解时，就无法生产输入

假如上面的代码例子产生变化：

① twice函数发生了改变：

int twice (int v) {
	return (v∗v) % 50;
}

则符号执行到twice函数时，会产生两个路径约束：

$x_0 \neq (y_0y_0)mod50$ $x_0 = (y_0y_0)mod50$

② 假设twice函数不可用（例如没有函数源码），则会产生两个路径约束：

$x_0 \neq twice(y_0)$ $x_0=twice(y_0)$

其中， $twice$ 是一个未解释的函数

在这两种情况下，约束求解器无法解决任何这些约束，符号执行将无法为修改后的程序生成任何输入。

为了缓解这个问题，研究者提出了混合符号执行 concolic execution（实际执行+符号执行）的方法，这是一种动态的符号执行，可以为修改后的程序生产一些输入。

混合符号执行（Concolic Execution）

混合符号执行Concolic Execution（实际执行+符号执行），是一种动态符号执行。在执行符号执行的同时，程序也在一些具体的输入值上执行。

Concolic Execution维护一个具体状态和一个符号状态。

具体状态将所有变量映射到它们的具体值
符号状态仅映射具有非具体值的变量

与经典的符号执行不同，混合符号执行在过程中需要获取程序的具体状态，因此它需要初始的具体值作为输入。

执行过程

Concolic Executio的初试输入可以给定或随机生成，在执行过程中收集条件语句中对输入的符号约束，然后使用约束求解器推断先前输入的变体（取反等），以便将程序的下一次执行引导到另一条执行路径。

系统地或启发式地重复该过程，直到探索完所有执行路径，满足用户定义的覆盖标准，或时间预算到期。

例子

int twice(int v) {
    return 2 * v;
}

void testme(int x, int y) {
    z = twice(y);
    if (z == x) {
        if (x > y + 10)
            ERROR;
    }
}

int main() {
    x = sym_input();
    y = sym_input();
    testme(x, y);
    return 0;
}

还是以上面的程序为例：

首先，Concolic Execution先产生一些随机输入，例如{x = 22, y = 7}
之后，同时具体地和符号化地执行程序。当实际执行到第7行的else分支时，符号执行会在该执行路径生成路径约 $x_0\neq2y_0$
之后，Concolic Execution会将路径约束的连接词取反，得到 $x_0= 2y_0$ ，并求解，可得到一种测试用例输入：{x = 2, y = 1}
通过这个新的测试用例输入，Concolic Execution会得到并进入新的路径，并同时开启新的实际执行与符号执行。在本例中，就会进入到第7行的then分支和第8行的else分支，此时就会产生新的路径约束： $(x_0=2y_0) \Lambda (x_0 \leq y_0+10)$ ，对于此约束进行约束求解，生成新的测试输入，可以让程序继续执行之前没有执行过的路径；而再对该约束取反，得到： $(x_0=2y_0) \Lambda (x_0 > y_0+10)$ ，就可以探索到新的路径，例如：{x = 30, y = 15}，使用这个测试输入，程序会触发第9行的ERROR。
通过这三次执行程序，Concolic Execution已经覆盖了程序的所有路径，并停止生产测试用例输入

注意，这里使用“深度优先”的搜索策略来探索所有的执行路径；我们也可以使用其他策略来探索不同顺序的路径。

执行生成测试(EGT)

本文作者通过EXE和Klee 这两篇工作，实现和扩展了EGT方法（Execution-Generated Testing）

EGT方法区分了程序的具体状态和符号状态，通过在每次操作之前动态检查所涉及的值是否是实际的，将具体执行和符号执行混合在一起。

如果是实际值，那么就按照程序本身执行；相反，如果至少有一个值是符号化的，则通过更新当前路径的路径条件以符号方式执行。

例子

还是以上面的程序为例，在第17行处，如果把y**=**sym input() 改为 y = 10，那么第6行z **=**twice (y); 函数将使用具体值 “20”来调用函数twice(20)，完成实际执行。

之后，第7行if (z == x)将变为if (20 == x)

约束 $x=20$ ，程序走then分支

约束 $x \neq 20$ ，程序走else分支

注意，在then分支，程序走到第8行为if (x > 20)，由于x = 20，则无法往下继续走。

总之，混合符号执行Concolic Execution与执行生成测试EGT，主要的贡献都是结合了实际执行与符号执行，缓解了传统符号执行的缺点。它们都是动态符号执行的范畴。

动态符号执行的缺点

动态符号执行的优点是：可以使用具体值，来降低与外部代码交互或约束求解超时所导致的不精确性，这缓解了传统符号执行遇到的问题。但是这个过程遇到的问题是，会丢失一些执行路径，从而牺牲了完整性。

先回顾一下Concolic Execution是怎样解决静态符号执行的缺点的：例如，在上面的代码例子中，将twice函数进行改变：返回值改为(v*v)%50 ，而且程序执行的初试随机值为{x = 22, y = 7}，则针对该随机输入，生成的路径约束为 $x_{0}\ne (y_{0} y_{0}) mod 50$ 假设约束求解器不能解决非线性约束，则Concolic Execution将无法为替代执行路径生成输入。当函数twice的源代码不可用时（是某个第三方库函数或系统调用），会出现类似情况，此时，路径约束为 $x_0 \neq twice(y_0)$ ，其中 $twice$ 是一个未解释的函数。以上是前文静态符号执行的缺点，混合符号执行Concolic Execution会通过使用实际值替换符号值的方式解决这个问题。例如，将 $y0$ 使用实际值 “7” 替换。那么上面的路径约束就简化为： $x_0 \neq 49$ ，求解该约束，可以得到一个探索新路径的输入：{x = 49, y = 7}。以此解决了传统符号执行（静态符号执行）的缺点。

但是，这个例子中，无法生成路径true, false的输入，即在代码：

void testme(int x, int y) {
    z = twice(y);
    if (z == x) {
        if (x > y + 10)
            ERROR;
    }
}

中，符合if (z == x)，但又不符合if (x > y + 10)，进不去ERROR

即：无法生成对于约束 $x_{0}= (y_{0} y_{0}) mod 50\wedge (x_{0}\leq y_{0}+10)$ 的测试输入，因为 $y_0$ 的值已经被实际化为“7”了。因此会造成路径的丢失，失去了路径完整性。

但是相比与传统符号执行遇到不受支持的操作或外部调用问题时直接终止执行，混合符号执行Concolic Execution的方法还是更可取。

符号执行的挑战

一、路径爆炸

符号执行的关键挑战之一就是路径爆炸问题。除了较小的程序外，所有程序中都有大量的程序路径，这通常是代码中静态分支数量的指数级。限制符号执行时间及循环迭代次数都可以缓解这一问题，主要的方法包括：

启发式技术-优先探索最有希望的路径启发式技术是用于确定路径探索优先顺序的关键机制。
- 使用CFG来探索，尽量选择与未覆盖指令最接近的路径
- 基于随机探索，将符号探索与随机测试相结合
使用合理的程序分析技术降低路径探索的复杂性
- 使用 selelct 表达式进行静态融合，然后将其直接传递给约束求解器
- 通过缓存和重用底层函数的计算结果，减小分析的复杂性

以上这些方法都是当时其他文献的工作，这里没有深入研究。

二、约束求解

两种优化方法：

不相关的约束消除：通常一个程序分支只依赖于一小部分的程序变量，因此一种有效的优化是从当前路径条件中移除与识别当前分支不相关的约束
增量求解：在符号执行期间生成的约束集的一个重要特征是，它们以来自程序源代码的一组固定的静态分支来表示。所以，多个路径可能会产生相似的约束集，所以可以使用相似的解决方案。通过重用以前相似请求得到的结果，可以提升约束求解的速度（CUTE、KLEE使用）

三、内存建模

程序语句转换为符号约束的精确性对符号执行的覆盖率有很大的影响。内存建模可以引申为其他方面的挑战，主要是符号执行如何模拟具体的系统环境。

精确度和可伸缩性之间的权衡应该根据要分析的代码(例如，低级系统代码与高级应用程序代码)以及不同约束求解理论之间的确切性能差异来确定。而在动态符号执行中，可以通过自定义符号公式中具体值的使用来调整可伸缩性和精度。

四、处理并发性

动态符号执行已经被有效地用于测试并发程序，包括具有复杂数据输入的应用程序、分布式系统等。