[符号执行-入门1]软件测试中的符号执行

最近在自学符号执行，所以，这篇经典文章(Symbolic Execution for Software Testing: Three Decades Later)[1]做为入门必读。

• 0. 定义
• 1. 经典的符号执行
• 2. 现代符号执行技术
  • 2-1. 混合执行测试(Concolic testing)
  • 2-2. 执行生成测试(Execution-Generated Testing, EGT)
  • 2-3. 动态符号执行中的不精确性(imprecision) vs.完整性(completeness)
• 3. 主要挑战和解决方案
  • 3-1. 路径爆炸(Path Explosion)
  • 3-2. 约束求解(Constraint Solving)
  • 3-3. 内存建模(Memory Modeling)
  • 3-4. 并发控制(Handling Concurrency)
• 4. MISC
• 5. Reference:

0. 定义

符号执行 （Symbolic Execution）是一种程序分析技术，它能够经过分析程序来获得让特定代码区域执行的输入。顾名思义，使用符号执行分析一个程序时，该程序会使用符号值做为输入，而非通常执行程序时使用的具体值。在达到目标代码时，分析器能够获得相应的路径约束，而后经过约束求解器来获得能够触发目标代码的具体值。

软件测试中的符号执行主要目标是[1]：

在给定的探索尽量多的、不一样的程序路径(program path)。对于每一条程序路径，
1) 生成一个具体输入的集合(主要能力)；
2) 检查是否存在各类错误(errors，包含assertion violations, uncaught exceptions, security vulnerabilities, and memory corruption)。

从测试生成的角度，符号执行能够生成高覆盖率的测试用例。
从bug finding的角度，符号执行能够提供一个具体的输入用于触发bug（过去经常用于调试bug）。

1. 经典的符号执行

符号执行的主要思想就是将输入(input)用符号来表征而不是具体值，同时将程序变量表征成符号表达式。所以，程序的输出就会被表征成一个程序输入的函数，即fun(input)。在软件测试中，符号执行被用于生成执行路径(execution path)的输入。
执行路径(execution path)：一个true和false的序列seq={p0,p1,...,pn}。其中，若是是一个条件语句，那么pi=ture则表示这条条件语句取true，不然取false。
执行树(execution tree)：一个程序的全部执行路径则可表征成一棵执行树。
以下图所示：

对应的执行树：

3条不一样的执行路径构成了一棵执行树。三组输入{x=0,y=1},{x=2,y=1},{x=30,y=15}覆盖了全部的执行路径。所以，符号执行的目标就是在给定的时间内，生成一个输入的集合使得全部的（或让尽量多的）执行路径依赖于由符号表征的输入。

符号状态(symbolic state)：符号执行维护一个符号状态，它是一个<变量，符号表达式(symbolic expressions)>的mapping。

符号路径约束(symbolic path constraint)： a quantifier-free first-order formula over symbolic expressions.

符号执行后的结果以下图所示：

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

这个时候，符号路径要么就是一串有限长度的ture后面跟着一个false（跳出循环），要么就是无限长的true。如图所示，

符号执行的主要缺点：若是符号路径约束不可解（不能被solver解决）或者是不能被高效（时间效率）的解，则不能生成input。回到以前的例子（见图 ~\ref{example-program}），若是把函数twice改为(v*v)%50（非线性）：

假设采用的sovler不可解非线性约束，那么，符号执行将失败，即没法生成input。

2. 现代符号执行技术

现代符号执行技术的特色是同时执行精确(Concrete)执行和符号(Symbolic)执行。

2-1. 混合执行测试(Concolic testing)

当给定若干个具体的输入时，Concolic testing动态地执行符号执行。Concolic testing会同时维护两个状态：

1. 精确状态(concrete state): maps all variables to their concrete values.
2. 符号状态(symbolic state): only maps variables that have non-concrete values.

不一样于传统的符号执行技术，因为Concolic testing须要维护程序执行时的整个精确状态，所以它须要一个精确的初始值。举例说明，仍是以前这个例子：

表明工具：

1. DART: Directed Automated Random Testing[2]
2. Concolic testing[3]

2-2. 执行生成测试(Execution-Generated Testing, EGT)

EGT在执行每一个操做以前，检查每一个相关的值是精确的仍是已经符号化了的，而后动态地混合精确执行和符号执行。若是全部的相关值都是一个实际的值（即精确的，concrete），那么，直接执行原始程序（即，操做，operation）。不然（至少一个值是符号化的），这个操做将会被符号执行。举例说明，假设以前那个例子，第17行改为y=10。那么，在调用twice时，传入的参数是concrete的，返回的也是一个concrete value，所以z也是一个concrete value。第七、8行中的z和y+10也会被转换成concrete vaule。而后再进行符号执行。

表明工具：

1. EXE[4]
2. KLEE[5]

因而可知，不管是concolic testing仍是EGT，他们都是动态地mix use concrete and symbolic execution。所以，也被称做“动态符号执行”。

2-3. 动态符号执行中的不精确性(imprecision) vs.完整性(completeness)

不精确性:代码调用了第三方代码库（因为种种缘由没法进行代码插装），假设传入的参数都是concrete value，那么就像EGT中的同样，能够所有看成concrete execution。即便传入的参数中包含符号，动态符号执行仍是能够对符号设一个具体的值。Concolic和EGT有不一样的解决方法，后面再介绍。除了调用外部代码，对于难以处理的操做数（如浮点型）或是一些复杂的函数（solver没法解决或须要耗费大量时间），使用concrete value能够帮助符号执行环节这种impression。
完整性:动态符号执行经过concrete value能够简化约束，从而防止符号执行get stuck。可是这也会带来一个新问题，就是因为这种简化，它可能会致使一些不完整性，即有时候没法对全部的execution path都能生成input。可是，当遇到不支持的操做或外部调用时，这显然优于简单地停止执行。

3. 主要挑战和解决方案

3-1. 路径爆炸(Path Explosion)

描述:
首先，要知道，符号执行implicitly过滤两种路径：

1. 不依赖于符号输入的路径；
2. 对于当前的路径约束，不可解的路径。
   可是，尽管符号执行已经作了这些过滤，路径爆炸依旧是符号执行的最大挑战。

解决方案:

1. 利用启发式搜索搜索最佳路径
   目前，主要的启发式搜索主要focus在对语句和分支达到高覆盖率，同时他们也可被用于优化理想的准则。
   • 方法1：利用控制流图来guideexporation。
   • 方法2：interleave 符号执行和随机测试。
   • 方法3（more recently）：符号执行结合演化搜索(evolutionary search)。其中，fitness function用于drive the exploration of the input space。
2. 利用可靠的(sound)程序分析技术来减少路径爆炸的复杂度
   • 方法1：静态地合并路径，而后再feed solver。尽管这个方法在不少场合都有效，可是他把复杂度转移给了solver，从而致使了下一个challenge，即约束求解的复杂度。
   • 方法2： 在后续的计算中，记录并重用low-level function的分析结果。
   • 方法3 ： 自动化剪枝

3-2. 约束求解(Constraint Solving)

描述:
约束求解是符号执行的技术瓶颈。所以，对于solver的优化（提升solver的求解能力）成了解决这个技术瓶颈的手段。

解决方案:

1. 去除不相关的约束
   通常来讲，程序分支主要依赖于一小部分的程序变量。也就是说，程序分支依赖于一小部分来自于路径条件(path condition)的约束。所以，一种有效的方法就是去掉那些与当前分支的输出不相关的路径条件。例如，现有路径条件：(x+y>10)^(z>0)^(y<12)^(z-x=0)。假设咱们如今想生成知足(x+y>10)^(z>0)^¬(y<12)，其中咱们想创建对¬(y<12)（与y有关）的feasibility。那么，(z>0)和(z-x=0)这两个约束均可以去掉，由于与y不相关。
2. 递增求解
   核心思想就是缓存已经求解过的约束，例如(x+y<10)^(x>5)=>{x=6,y=3}。对于新的约束，首先判断这个新约束的搜索空间是缓存里约束的超集仍是子集。若是是新的约束的搜索空间是缓存的约束的子集，那么，就把缓存中的约束去掉多余的条件后继续求解。若是是超集，那么直接把解代入去验证。

3-3. 内存建模(Memory Modeling)

描述:
程序语句转化成符号约束的精度对符号执行的覆盖率有很大的影响。例如，内存建模是用一个具体的数值去近似一个固定位数的整数变量可能会颇有效，可是另外一方面，它也会致使imprecision，好比丢失一些符号执行的路径，或探索一些无用的解。另外一个例子就是指针，一些工具如DART[3]只能处理精确的指针。

解决方案:
precision和scalability是一个trade-off。须要考虑的因素有：

1. 代码是high level的application code仍是low-level的system code。
2. 不一样的约束求解器的实际效果。

3-4. 并发控制(Handling Concurrency)

描述:
不少现实世界中的程序是并发的，这也意味着他们不少都是不肯定的(non-deteminism)。尽管如此，符号执行已经被有效地运用在测试并发系统，分布式系统。

4. MISC

1. 符号执行的论文，教程，视频，工具

后续，我会记录一些step by step使用部分符号执行工具的blog。

5. Reference:

[1]: Symbolic Execution for Software Testing: Three Decades Later
[2]: DART: Directed Automated Random Testing
[3]: CUTE: A concolic unit testing engine for C
[4]: EXE: Automatically generating inputs of death
[5]: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs