[符号执行-入门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。第7、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