Symbolic Execution for Software Testing(翻译)

注：该翻译纯属自嗨

0.介绍

符号执行在近几年获得了大量关注，它作为一种很有效率的技术用于产生高覆盖率的测试组件和找出复杂软件应用的深层错误。在符号执行背后的关键理念在三十多年前就被提出了，由于约束可满足性的显著发展，以及结合了具体符号执行的更具扩展性的动态方法，它到最近才开始变得实用起来。在这篇文章中，我们概述了现代符号执行技术在路径探索，条件约束和内存模型几个方面的挑战，并讨论几个主要在作者工作中得出的解决方案。需要注意的是，我们并非全面考察在该领域的现有工作，而是去说明一些关键性的挑战，并通过作者在工作中所遇一些实例，来提出解决方案。有关符号执行的详细概述，请参考该领域中以前发表的文献。

在软件测试环境中，符号执行的关键目的是在给定的一段时间内，尽可能发现不同的程序执行路径。每一条路径生成一系列输入来执行该路径，并检查各种各样的错误，包括断言违反，未捕获的异常，安全漏洞和内存崩溃。得到具体输入值的能力是符号执行最主要的优势之一：从测试生成的观点来看，它允许生成高覆盖率的测试组件；从寻找bug的观点来看，它提供给开发者触发bug的具体输入值，这些输入值可以单独用于debug，它们由符号执行工具生成。

此外，在给定程序路径上寻找错误方面，符号执行比传统的动态执行技术更强大，比如一些流行工具Valgrind或Purify的应用，它们依赖于有效的具体输入来触发错误。最后，与其他一些程序分析技术不同，符号执行技术不仅仅限制于找出一般的错误，如缓冲区溢出，还可以推断出更高级的程序属性，比如复杂的程序断言。

1.经典符号执行概述

在符号执行的背后是关键理念是使用符号性质的值，而不是作为输入的具体数据值，并将程序变量的值表示为符号表达式。因此，程序计算出的输出值就表示为符号输入值的函数。在软件测试中，符号执行用于为程序的每条执行路径生成测试输入。一条执行路径就是true和false的集合，其中，序列中第i个位置的true表示沿该路径执行的第i个条件语句使用then分支。程序的所有执行路径可以表示为一棵树，名为执行树。

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;
}

举个例子，在上方代码中，函数testme()有三条执行路径，如下图。

当输入取{x = 0,y = 1},{x = 2,y = 1} and {x = 30,y = 15}时，这些路径可以成为实例执行。

其目的是生成这样一组输入，使所有执行路径都依赖于符号输入，或尽可能的在给定的时间预算中，通过运行程序找到来精确的找到这些输入。

符号执行维护一个符号状态σ，它将变量映射为一个符号表达式。以及一个符号化路径约束PC，它是一个符号表达是上的无量词一阶公式。在符号执行的起始阶段，σ被初始化为空映射，PC则被初始化为true，在符号执行期间，σ和PC都会进行更新。顺着程序的一条执行路径符号执行到结尾时，使用约束求解器求解PC来生成具体的输入值。如果程序使用这些输入值进行执行，那么它会精确地执行在相同路径上并以相同的方式结束。

举例来说，上方代码以σ为空映射，且PC为true初始化然后执行。在每一个读取语句var = sym_imput()接收程序的一个输入，符号执行添加一个映射var->s到σ中，这里s是个无约束条件的新符号值。比如，符号执行main()函数的前两行，会得到结果σ={x->x0, y->y0}，这里x0和y0是两个刚初始化无条件约束的符号值。对每一个赋值操作v=e，符号执行都会更新σ，将v映射到σ(e)，通过e在当前符号状态下的值得到符号表达式。比如，在执行到第6行后，σ={x->x0, y->y0, z->2y0}。

在每一个条件语句if(e) S1 else S2，PC会被更新为PC∧σ(e)(then分支)，一个新的条件约束PC'就会被创建，它初始化为PC∧¬σ(e)(else分支)。如果对符号值进行一些适当的赋值能使PC有效，即PC是可满足的，则符号执行沿着then分支继续执行下去，并维持现有的PC和σ。同样的，若PC'是可满足的，则另一个符号执行被创建，它维持现有的PC'和σ，沿else分支执行。需要注意的是，与具体的执行不同，两个分支都可以被执行，结果会有两条执行路径。如果某个PC或PC'是不可满足的，则符号执行沿着相应路径终止。比如，在上述代码第7行后，有两个符号执行实例被创建，它们的路径约束分别是 x0=2y0 和 x0!=2y0；类似的，在第8行后，两个符号执行实例被创建，它们的路径约束分别是(x0=2y0)∧(x0>y0+10)和(x0=2y0)∧(x0<=y0+10)。

如果一个符号执行实例碰到了exit或error时，当前符号执行实例就会被终止，并利用一个现成的约束求解器来生成一个可满足当前路径约束的赋值。这个可满足赋值形成了测试输入，也就是说，若程序使用这些具体的输入值来执行，那就一定会沿着相应的路径来执行，并以相同方式终止。举例来说，在上述代码中，我们得到了符号执行的3个实例，它们的测试输入分别是{x=0, y=1}，{x=2, y=1}和{x=30, y=15}。

若代码中包含循环或递归结构，且它们的终止条件是符号化的，则可能导致有无穷多条路径。

void testme_inf(){
    int sum = 0;
    int N = sym_input();
    while (N > 0){
        sum = sum + N;
        N = sym_input();
    }
}

比如在上方代码中就有无数条执行路径，每条执行路径是任意数量的trues然后跟着一个false，或就是无数的trues。n个true后跟一个false的路径的符号路径约束为

每一个Ni都是一个符号值，且执行到最后的符号状态为{N->Nn+1, sum->∑i∈[1,n] Ni}。在实践过程中，需要对路径搜索设置一个限制，例如timeout，限制路径数量，循环迭代次数或探测深度。

经典的符号执行有一个关键的缺点，若符合执行路径的符号路径约束无法使用约束求解器进行有效的求解，则无法生成输入。举例来说，符号执行在最上方那段代码中有两种变体，其中一个变体，我们将twice函数修改为以下代码

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

另一种变体，我们假设twice函数的代码未知。让我们假设我们的约束求解器不能求解非线性运算。在第一种变体中，在执行完第一条条件语句后，符号执行会产生路径约束x0!=(y0y0) mod 50和x0=(y0y0) mod 50。在第二中变体中，符号执行会产生路径约束x0!=twice(y0)和x0=twice(y0)，这里twice是未有解释的函数。由于余数求解器无法求解这些约束条件，符号执行将无法为修改后的程序生成任何输入。我们接下来会描述两种现代符号执行技术，它们缓解这个问题并至少为修改后的程序生成一些输入。

2.现代符号执行技术

现代符号执行技术的关键要素之一是将具体执行和符号执行混合的能力。我们提出以下两种扩展方式，然后讨论它们提供的关键优势。

向导性随机测试(Concolic Testing)：有向自动随机测试，或动态符号执行的向导性随机测试，同时程序在具体的输入值上运行。Concolic testing维护了一个具体化状态和一个符号化状态：该具体化状态映射所有变量到它们的具体值；该符号化状态仅映射没有具体值的变量。和经典符号执行不同，由于concolic执行维护全部程序执行的具体化状态，它需要给输入初始化具体的值。Concolic testing通过给定的或随机的输入值开始执行，并将执行中的符号约束混合到输入值中，然后使用约束求解器来推断先前输入的变化，以便引导程序接下来的执行该走向哪一个执行路径。这个过程系统的或启发式的重复，直到所有执行路径探索完毕，或者达到用户规定的覆盖率，或者时间预算耗尽。

举个例子，依旧是这段代码

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执行会生成一些随机的输入值，比如{x=22, y=7}，然后符号化和具体化地一起来执行程序。在第7行代码中，这个具体的执行会走向else分支，然后符号执行会生成x!=2y0的路径约束。Concolic testing否定路径约束中的连接，并求解x0=2y0得到测试输入{x=2, y=1}；这个新的输入会强制让程序执行不同的执行路径。Concolic testing利用这个新的输入重复具体执行和符号执行。这次执行的路径与之前不同，它在第7行执行then分支，并在第8行执行else分支。例如之前的执行，concolic testing也会沿着具体执行来进行符号执行，并生成路径约束(x0=2y0)∧(x0<=y0+10)。Concolic testing会生成一个新的测试输入来使程序强制执行沿着之前为执行过的路径。它通过否定连接(x0<=y0+10)并求解约束(x0=2y0)∧(x0>y0+10)得到测试输入{x=30, y=15}。在这个输入下程序收到ERROR语句。在这第三次程序执行后，concolic testing报告所有被探索的执行路径，并终止测试输入的生成。注意在这个例子中，concolic testing使用深度优先搜索的方式来发现所有执行路径。然而，也可以用其他策略来探测不同顺序的路径，这在之后会讨论到。

Execution-Generated Testing(EGT):

EGT方法通过区分程序的具体状态和符号状态来工作，使用EXE和KLEE工具来实现和扩展。为此，EGT通过在每次运算之前动态检查所涉及的值是否都是具体的，从而混合具体的和符号执行。这样的话，执行的运行就和原始程序相同。另外，如果至少有一个值是符号值，则进行的是符号化运算。它利用当前路径的路径条件进行更新。依旧用如下代码举例：

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;
}

如果在15行执行y=10，则第6行的twice函数会使用具体值20作为参数被调用，就像会在原本会程序中被调用那样(要注意twice函数可以对输入的值进行任意复杂的操作，但这并不会给符号执行带来什么压力，因为这个调用会被具体的执行)。之后，第7行的分支变为if (20 == x)，并且符号执行会遵循then(添加约束x == 20)分支和else分支(添加约束x != 20)。注意在then路径，第8行条件会变为if (x > 20)，并且因此then这条分支是不可执行的，因为x在第7行已经被限制为20了，与x>20矛盾。

Concolic testing和EGT是两种现代符号执行技术，它们的主要优势在于能将具体执行与符号执行相结合。为了简单起见，在本文其他地方我们将这些技术统称为动态符号执行技术。

动态符号执行的不精确性和完整性：

将具体执行与符号执行混合的一个关键优点是，与外部代码交互或约束求解超时所造成的不精确性可以通过使用具体值来缓解。

举例来说，大多数实际应用都会与外部进行交互，例如通过调用一些不是符号执行的库，或使用系统调用。如果这些调用的所有参数都是具体的，这个调用就会简单地具体执行，就像原本的程序那样。然而，即使一些操作对象是符号化的，动态符号执行可以使用这个操作对象可能的具体的来执行：在EGT中，这是通过求解当前路径约束的可满足赋值来完成的。而concolic testing可以立即使用当前concolic在运行时取得输入的具体值。

除了外部代码外，不精确性在符号执行中也蔓延到了其他地方，比如无法处理的运算(如浮点运算)或者造成约束求解器超时的复杂的函数，使用具体值允许动态符号执行恢复这种不精确性，虽然这会使得一些执行路径缺失，即牺牲了其完整性。

为了进一步说明，我们描述在twice函数返回非线性值(v*v)%50的运行版本中，concolic testing的行为。我们假设concolic testing开始于一个随机输入{x=22, y=7}，它由符号路径约束(x0 != (y0y0) mod 50)生成。如果我们假设约束求解器无法求解非线性约束，则concolic testing无法为一条可选执行路径生成输入，如果源代码中twice函数使用了外部代码(如调用外部函数库，使用系统调用)，也会出现类似的情况。在这种情况下路径约束会变为x0!=twice(y0)，这里twice是一个粗略的函数。concolic testing处理这种情况是通过将一些符号值替换为具体值，以此得到的简化后的约束可以被现有的约束求解器求解。举个例子，上述例子中，concolic testing将y0替换为具体值7，这样就能简化路径约束为x0!=49。通过求解x0=49这个路径约束，concolic testing生成输入{x=49, y=7}来探索之前未被探测的路径。要注意经典符号执行没这么容易简化执行，这是因为在整个符号执行中，具体状态都是不可取的。

动态符号执行能够使用具体值来简化约束，这有助于它为卡住的执行路径生成测试输入，但这里有一个问题，由于简化了路径约束，使得它丧失了完整性，即可能无法对一些执行路径生成输入。例如，在我们的例子中，动态符号执行无法仅为路径true和false生成输入(而是以具体值替代)。但是，当遇到不支持的操作或外部调用时，这显然优于简单地终止执行的替代方案。

关键性挑战和一些解决方案

路径激增

符号执行的关键挑战之一是，除了非常小的程序外，其余都具有数量庞大的程序路径，这通常是代码中静态分支的指数级别。所以，给定一个固定的时间预算，首先探索最相关的路径十分重要。

首先，要知道符号执行暗中过滤了所有不依赖于输入的所有分支，并且给定当前路径约束是不可行的。尽管有这种过滤，路径激增任是符号执行面临的最大挑战。有两种关键方法用于解决这个问题：启发式优先的考虑最有希望的路径探索和利用完善的程序分析技术来降低路径探索复杂度，我们将依次讨论这两种方法。

启发式技术

符号执行工具进行启发式路径探索使用的关键机制是使用启发式搜索。大部分启发式方法都致力于实现高度陈述和分支覆盖，但它们也存在其他的优化标准。

一种十分有效的方法是使用静态控制流图(CFG)从未覆盖的指令开始，去引导探索最近的路径(即CFG静态测量)。一种类似的方法是偏向之前访问过的，运行时间最少的语句。

再比如，基于随机探索的启发式技术也被证明是成功的。它的关键理念是从程序一开始，在每一个可选的符号化分支上随机选择要探索分支。

另一种成功的方法是将符号探测与随机测试交错执行。这种方法结合了随机测试迅速到达深度的执行状态的能力和符号执行可以彻底执行探索给定邻域内的状态的能力。

...