0%

符号执行测试|概述

Posted on Edited on In Views: Valine:

Reference: Symbolic Execution for Software Testing: Three Decades Later

简介

定义

符号执行是一种可生成高覆盖测试用例、在复杂程序中寻找深层错误的有效技术；是一种流行的程序分析技术。

使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

目标及优势

在给定时间里，探索尽量多的、不同的程序路径（program path）。

  1. 生成一个具体输入的集合；（符号执行的主要优势之一）
  2. 检查是否存在错误：断言违规、未捕获的异常、安全漏洞和内存损坏。

其中，生成具体输入集合的优势所在：

  • 测试用例角度：允许创建高覆盖率的测试套件；
  • 查找bug角度：针对bug提供触发此bug的输入，用于验证和debug。

另外，在给定程序路径中寻找错误时，符号执行比传统的动态执行技术更强大，传统动态执行技术的表现则要看那些触发错误的具体输入的可用性。

最后，与某些其他程序分析技术不同，符号执行既可以找出“缓冲区溢出”这样的一般性错误，也可以引出更高级的程序属性，例如“复杂的程序断言”。

传统符号执行

符号执行的核心思想

  • 输入：用符号值(symbolic values)来表征而不是具体值(concrete data values)；
  • 程序变量：根据输入符号值表征成符号表达式(symbolic expressions)；
  • 输出：根据程序计算出的函数表达式:

$$
function(input)
$$

执行路径与执行树

在软件测试中，符号执行用于生成执行路径的输出；符号执行可以同时探索程序在不同输入下可能采用的多种路径。

  • （一条）执行路径 (execution path) ：由true/false组成的一个序列，
    $$
    seq={p1,p2,p3,…}
    $$
    如果$ p_i=true $，则说明在此路径中第$i$个条件语句取$true$值，走$then$分支。

  • **执行树 **(execution tree) ：一个程序的所有执行路径用树形结构表示。

举例:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
int twice(int v){
    return 2*v;
}
void testme(int x,int y){
    z=twice(y);
    if(z==x){ //condition statement 1
        if(x>y+10){ //condition statement 2
            ERROR; 
        }
    }
}
int main(){
    x=sym.input();
    y=sym_input();
    testme(x,y);
    return ();
}

这段程序由两个条件语句分流成三条分支，设计如下三个输入：
$$
{x=0,y=1},{x=2,y=1},{x=30,y=15}
$$
可覆盖到三条执行路径，即：
$$
{ true,true },{ true,false },{ false,* }
$$

三条执行路径形成一个执行树，

graph TD
    A[2*y equals x] -->|true| B[x greater than y+10]
    A -->|false| C(x=0,y=1)
    B -->|true| D(x=30,y=15)
    B -->|false| E(x=2,y=1)

符号状态和符号路径约束

  • 符号状态 $\sigma$ (symbolic state) :符号执行维护一个符号状态，将变量映射成符号表达式。

  • 符号路径约束 $PC$ (symbolic path constraint) ：一个无修饰的、一阶逻辑的符号表达式公式。（a quantifier-free first-order formula over symbolic expression）

    参看：补充概念解释

分析普通程序

符号执行开始时，$\sigma$被初始化为空映射集合$\sigma =\phi，$PC$被初始化为$true$，$\sigma$和PC会在符号执行过程中不断更新。

每当程序给一个变量获取新值，就将$var\rightarrow s$加入$\sigma ={…}$中，s是一个新的符号值；每当程序给一个变量赋新值，就更新$\sigma$中该变量所映射的符号值。

每当经过一个条件语句$e$，$PC$会被更新为$PC\wedge \sigma(e)$，并走”then”分支；同时生成一个新的$PC’$并初始化为$PC\wedge \neg{\sigma(e)}$，并走”else”分支。

每当经过一个$PC$/ $PC’$允许的赋值语句，$PC$/ $PC’$会保持不变继续走，各自维护和更新自己的$\sigma$；

在沿着一条执行路径的符号执行结束时，PC使用约束求解器 (constraint solver) 来生成具体的输入值。如果程序在这些具体的输入值上执行，它将采取与符号执行完全相同的路径，并以相同的方式终止。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
int twice(int v){
    return 2*v;
}
void testme(int x,int y){
    z=twice(y);
    /*sigma={x->x0,y->y0,z->2y0}*/ //z获取到符号值
    if(z==x){
        if(x>y+10){//PC: (x0=2y0) and (x0>y0+10)
            ERROR; 
            /*
            sigma={
            	x->x0,
            	y->y0,
            	x=2y0,
            	x0 > y0+10
            }
            */
        }//PC': else:(x0=2y0) and (x0<=y0+10)
    }
}
int main(){
    /*
    start: sigma={},PC=true
    */
    x=sym.input();
    y=sym_input();
    /*sigma={x->x0,y->y0}*/ //x0,y0是两个初始化的无约束的符号值。
    testme(x,y);
    return ();
}

分析循环程序

当代码中包含循环和递归时，如果终止条件是符号的话，那么符号执行会产生无限数量的执行路径。

1
2
3
4
5
6
7
8
void testme_inf(){
    int sum=0;
    int N=sym_input();
    while(N>0){
        sum = sum+N;
        N=sym_input();
    }
}

此种情况可能有无数条执行路径，执行路径要么有无限长的true；要么有无数个true后以一个false跳出循环并结束，则此条路径的$PC$和符号状态$\sigma$如下：
$$
PC = \big( \bigwedge_{i\in[1,n]}{N_i > 0} \big)\wedge(N_{n+1}\leq0)
$$

$$
\sigma= {N \to N_{n+1},sum \to \sum_{i \in [1,n]}{N_i}}
$$

传统符号执行的缺点

如果符号路径约束$PC$不可解或不能被高效地解决，则不能为程序生成input。

补充概念解释

  • 一阶逻辑 first-order logic ：逻辑函数的参数可以是变量，但不能是函数。这种语言的语法(Syntax)由字母系统(Alphabet)和构造法则(formation rules)组成。

  • 无修饰公式 quantifier-free formulas ：由谓词符号、等式和逻辑运算符号组成的公式。比如：$p(x)$。

  • 构造法则 formation rules ：

    • 术语 terms ：包括变量、函数。
    • 公式 formulas：包括修饰符(quantifier)、谓词符号、等式、逻辑运算符号。

参考：可满足性模块理论(SMT)基础

现代符号执行

现代符号执行技术的特点是同时执行具体执行和符号执行。以下技术可以统称为”动态符号执行“。

混合执行测试(concolic testing)

当给定若干个具体的输入时，混合执行测试动态地执行符号执行。

混合执行测试维护两个状态：

  1. 具体状态（concrete state）：映射{所有变量$\rightarrow$具体值}
  2. 符号状态（symbolic state）：只映射有非具体值的变量。

混合执行测试需要一个具体的初始值，因而使用一些既定的、随机的输入来执行程序。执行过程中，从程序中的各条件语句收集符号约束，之后用约束求解器推断之前输入值的变化，以此来控制程序的下一段可选择路径的执行。

混合测试使用一些既定的、随机的输入来执行程序，从程序中的各条件语句收集符号约束，之后用约束求解器推断之前输入值的变化，以此来控制程序的下一段可选择路径的执行。

这个过程是系统地或启发性地重复的，直到所有的执行路径都被探索，用户定义的覆盖率标准被满足，或者时间预算过期。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
int twice(int v){
    return 2*v;
}
void testme(int x,int y){
    z=twice(y);
    if(z==x){/*PC=(2*y0=x0) //x=2,y=1
        S3:{x=2,y=1} takes this path, 
        different from prev(S2)
        */
        if(x>y+10){/*PC=(2*y0==x0)^(x0>y0+10) //x=30,7=15
        	S5:{x=30,7=50} takes this path, 
        	different from prev(S4)
        	*/
            ERROR; 
        }else/*PC=(2*y0=x0)^(x0<=y0+10) //x=2,y=1
            S4:solve (2*y0=x0)^(x0>y0+10),
            and generate new input:{x=30,7=15}
            */ 
        }
    }else{/*PC=(2*y0!=x0) //x=22.y=7
    	S2:solve (2*y0=x0) 
    	and generate new input:{x=2,y=1}
    	*/
    }
}
int main(){
    x=sym.input();
    y=sym_input();
    /*S1:generate random input:{x=22,y=7}*/
    testme(x,y);
    return ();
}

第一条执行路径：input={x=22,y=7}，$S1\rightarrow S2$，生成{x=2,y=1}；

第二条执行路径：input={x=2,y=1}，$S3\rightarrow S4$，生成{x=30,y=15}；

第三条执行路径：input={x=30,y=15}，$S5$，结束。

执行生成测试EGT(execution-generated testing)

EGT混合具体执行和符号执行。

EGT在执行每个操作之前，动态地检查每个相关值是否是具体的，如果是具体的，就正常按照源代码执行；如果至少有一个变量是符号化的，就符号化地执行——为当前程序路径更新PC。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
int twice(int v){
    return 2*v;
}
void testme(int x,int y){
    z=twice(y);//z=20, 按照源代码执行
    if(z==x){//=> if(20==x)
        //add x=20
        if(x>y+10){//=>if(x>20)
            //infeasible
            ERROR; 
        }else
            //x=20
        }
    }else{
    	//add x!=20
    }
}
int main(){
    x=sym.input();
    y=10;//instead of y=sym_input()
    testme(x,y);
    return ();
}

动态符号执行的不精准性vs.完整性

使用具体值缓解不精确性，以牺牲完整性为代价

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

与外部代码交互的角度：如果传递给调库、系统调用的参数是具体的，则可以像在源代码中简单地具体执行该调用。即使某些操作数是符号化的，动态符号执行也可以使用符号操作数的具体值之一，例如在EGT中寻找满足当前路径约束的具体值来完成。

约束求解超时的角度：符号执行中一些不精确性会蔓延，例如未处理的操作或一些导致约束求解器超时的复杂函数。具体值的使用允许动态符号执行从该不精确中恢复，以丢失某些执行路径为代价，从而牺牲了完整性。

讨论上述导致约束求解器超时的复杂函数的问题：假定约束求解器无法解决非线性的约束，而程序中恰好有一个处理函数在做非线性的运算，那么混合测试就无法针对一条待选的执行路径有效地生成新的输入值。为了解决这种情况，混合测试以具体值替换一些符号值，使得生成的约束是简化的（simplified），而且可以被现有的约束求解器解决。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//int twice（int v）{}
int squareMod50(int v){//non-linear funtion
    return (v*v)%50;
}
void testme(int x,int y){
    z=squareMod50(y); //替换y0为7，sigma={x->x0,y->7}
    //z=49
    if(z==x){//simplified as (x0==49)
        if(x>y+10){//混合测试生成input{x=49,y=7}
            ERROR; 
        }else
        }
    }else{
    	//simplified as (x0!=49)
    }
}
int main(){
    x=sym.input();
    y=sym_input();
    /*sigma={x->x0,y->y0}*/
    testme(x,y);
    return ();
}

传统符号执行就没有办法做这样的简化工作(simplication)，因为符号执行过程中不允许用具体值。

当符号执行在一条执行路径卡住时，动态符号执行可以利用具体值为执行路径生成测试输入值以简化约束。但是达成简化可能会牺牲完整性——可能就不会为个别执行路径生成测试输入。

主要挑战和解决方案

讨论符号执行面对的主要挑战以及几个应对的解决方案。

路径爆炸(Path Explosion)

符号执行的一大挑战：程序无论大小，总有大量的执行路径，其数量基本上是程序分支数的指数级别的量。所以，如果给给定一段时间，符号执行会先尽量遍历关键路径。

首先，符号执行会隐式地过滤两种路径：

  1. 不依赖符号输入值的路径；
  2. 对于当前路径约束不可解的路径。

另外，路径爆炸是符号执行所面临的最大挑战之一。解决路径爆炸的两个关键方法是：

  1. 启发式地优先探索最有前途的路径。
  2. 使用可靠的程序分析技术来降低路径探索的复杂性。

启发式技术(heuristic techniques)

符号执行工具排列路径探索优先级的主要机制：搜索的启发式。多数的启发式会关注实现对于语句和分支的高覆盖，也可以用于满足我们需要的标准。

方法1：利用**静态的控制流图(CFG)**来将爆炸引导向最近的一条路径。

方法2：基于随机探索的启发式。程序从头开始，在每个符号化分支两个分叉中随机选择一个去探索。

方法3：将随机测试和符号探索交错起来的方法。这种方法结合了随机测试快速到达深度执行状态的能力，以及符号执行彻底探索给定邻域中状态的能力。

方法4：符号执行与进化搜索相结合，在进化搜索中使用适应度函数来驱动对输入空间的探索。Austin工具将基于搜索的软件测试与动态符号执行相结合，前者使用合适的适应度函数来驱动测试输入空间的演化搜索，后者利用这两个方面的优点。

基于搜索的软件测试的有效性取决于其适应度函数的质量。

利用动态和静态分析的具体状态信息或符号信息来改进适应度函数，从而更好地生成测试。

程序彻底分析技术(sound program analysis techniques):

利用程序分析和软件验证的各种思想，以合理的方式减少路径探索的复杂性。

可以用来减少探索路径数量的一种简单方法是使用$select$表达式将它们静态合并，然后将这些$select$表达式直接传递给约束求解器。这种方法可以解决很多情况的问题，但是它也将复杂性传递给了约束求解器——新的挑战：约束求解的复杂度。

组合技术通过在后续计算中缓存和重用低层函数的分析来改进符号执行。关键思想是计算每个待测函数的函数概要(根据函数输入和输出的前置和后置条件进行描述)，然后在更高级别的函数中重用这些概要。延迟测试生成是一种类似于静态软件验证中的反例导向细化范例的方法。该技术首先使用动态符号执行，通过用无约束的输入替换每个调用的函数，探索被测函数的抽象。

避免重复探索代码相同部分的相关方法：在探索过程中自动修剪冗余路径——具有相同符号约束的相同程序点的路径可以丢弃。类似的技术工作原理是将输入分割成互不干扰的块，然后分别进行研究。

约束求解(Constraint Solving)

约束求解在符号执行中占主导地位，也是符号执行的技术瓶颈。符号执行在某些程序中无法扩展的一个关键原因是，它们的代码所生成的查询会破坏求解程序。

实现约束求解器优化成了解决这个技术瓶颈的手段。

消除不相关的约束(Irrelevant constraint elimination)

符号执行中的绝大多数查询都是为了确定某个分支的可行性而发出的。一个重要的发现是，通常一个程序分支只依赖于少量的程序变量，因此依赖于路径条件的少量约束。

因此，一种有效的优化是从路径条件中移除那些与决定当前分支的结果无关的约束。

例如，让当前执行的路径条件为
$$
{(x+y>10)}\wedge{(z>0)}\wedge{(y<12)}\wedge{(z-x=0)}
$$
并且我们希望针对如下的新条件生成输入
$$
{(x+y>10)}\wedge{(z>0)}\wedge{\neg{(y<12)}}
$$
其中，$\neg (y<12)$是是我们试图建立其可行性的否定分支条件。此时，删除条件$(z-x=0)$是安全的，因为约束不会影响到 $y<12$ 的分支。

这个简化约束集的解将为x和y提供新的值，我们使用当前执行的z值来生成新的输入。更正式地说，该算法通过查看否定约束所依赖的所有约束之间是否共享任何变量来计算它们的传递闭包。

递增求解(Incremental solving)

在符号执行过程中产生的约束集的一个重要特征是，它们以程序源代码中一组固定的静态分支来表示。因此，许多路径都有类似的约束集，因此允许有类似的约束;可以利用这一事实，通过重用以前类似查询的结果来提高约束求解的速度。

在KLEE中，所有查询结果都存储在一个缓存中，该缓存将约束集映射为具体的变量赋值，或者在约束集不可满足时映射一个特殊的无解决方案标志)。

内存建模(Memory Modeling)

将程序语句转换为符号约束的精度对符号执行实现的覆盖率以及约束解决的可伸缩性有很大的影响。例如,使用一个内存模型近似固定宽度的整数变量与实际数学整数可能更有效,但另一方面可能导致不精确的分析代码取决于角落算术溢出等情况下,这可能导致符号执行遗漏路径或探索不可行。

并发控制(Handling Concurrency)

大型的实际程序通常是并发的。由于这些程序固有的非确定性，测试非常困难。尽管存在这些挑战，动态符号执行已被有效地用于测试并发程序，包括具有复杂输入数据的应用、分布式系统和GPGPU prog中的复杂数据应用程序。

总结

符号执行已经成为一种有效的程序测试技术，它提供了一种自动生成输入的方法，可以触发从低级程序崩溃到高级语义属性等各种软件错误;生成测试套件，实现高覆盖率的程序;并提供每个路径的正确性保证。

补充资料

Awesome Symbolic Execution