一、符号执行概念

• 从测试的角度来看，它可以模拟出各个路径的输入值，从而创建高覆盖率的测试套件。
• 从缺陷查找的角度来看，它为开发人员提供了触发缺陷的具体输入，利用该输入，程序可用于缺陷的确认与调试。符号执行不仅限于查找诸如缓冲区溢出之类的问题，而且可以通过根据缺陷发现的条件，生成复杂的断言，来判断缺陷发生的可能性。

• 经典符号执行并不真实地执行，而是基于解析程序，通过符号值模拟执行；有代价小、效率高的优点，但是执行效率比较低、误报高。
• 动态符号执行结合使用了具体执行与符号执行，综合了具体执行和经典符号执行的优点，并出现了 混合执行  和  执行生成测试 两种符号执行技术；
• 选择性符号执行可以对程序员感兴趣的部分进行符号执行，其它部分用真实值执行，代表工具 S2E 。

二、经典符号执行

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

• 执行路径（execution path）：一个true和false的序列seq={p0,p1...,pn}。其中，如果是一个条件语句，那么pi=true则表示条件语句的取值为:true，否则取false；
• 执行树（execution tree）：一个程序的所有执行路径则可表征成一颗执行树。

• 符号状态（symbolic state）：符号执行维护一个 符号状态 σ，将变量映射到符号表达式；
• 符号路径约束（symbolic path constraint）： 符号路径约束PC，它是符号表达式上无量词的一阶公式；
• 在执行开始时，将符号状态σ初始化为一个空映射，将符号路径约束PC初始化为true；
• 在符号执行过程中，符号状态σ 和 符号路径约束PC都会更新；
• 在沿着程序执行路径的符号执行结束时， 使用约束求解器对符号路径约束PC进行求解，以生成具体的输入值。如果程序在这些具体的输入值上执行，它将采用与符号执行完全相同的路径并以相同的方式终止。

• 初始化：初始化符号状态σ为空，符号路径约束PC为true；
• 在 每个赋值v=e处，符号执行都通过将v映射到 σ(e)来更新σ ，该映射是通过对当前符号状态求值，而获得的符号表达式。 例如：

        a) main()函数的前两行（第14-15行）的符号执行导致σ= {x -> x0，y -> y0}，其中x0，y0是两个初始不受约束的符号值;

        b)  在执行第6行之后，σ = {x -> 0，y -> y0，z -> 2y0}。

• 对于每个条件语句：if（e） then S1 else S2。

        a) 在第7行之后，分别创建了两个符号执行实例，分别具有路径约束x0 = 2y0和x0 ≠ 2y0；

        b）在第8行之后，分别创建两个具有路径约束的符号执行实例（x0 = 2y0）∧（x0 > y0 + 10）和（x0 = 2y0）∧（x0 ≤ y0 + 10）；

        c）“then”分支： PC被更新为PC ∧ σ(e)；

        d）“else”分支： 生成一个新的PC', PC'被初始化为：PC∧¬ σ(e)；   ∧¬表示false

        e）如果分支的状态σ的PC可满足，则符号执行沿着分支继续，否则路径终止。

           例如：

1. 如果一个符号执行实例碰到了exit或error时，当前符号执行实例就会被终止，并利用一个现成的约束求解器来生成一个可满足当前路径约束的赋值。 例如： 三条路径按照约束求解后，分别得到我们期望的三组输入：{x=0, y=1}，{x=2, y=1}和{x=30, y=15}。
2. 若代码中包含循环或递归结构，且它们的终止条件是符号化的，则可能导致有无穷多条路径。在实践过程中，需要对路径搜索设置一个限制，例如timeout，限制路径数量，循环迭代次数或探测深度。

三、现代符号执行技术

3.1、混合执行测试

与经典的符号执行不同，由于混合执行在整个执行过程中，需要维护程序的具体状态，因此其输入需要初始具体值。 

混合执行测试从一个给定的输入或随机输入开始执行程序，沿着执行的条件语句在输入上收集符号约束，然后使用约束求解推断先前输入的变化，以便引导程序接下来的执行该走向哪一个执行路径。重复此过程，直到探索了所有执行路径，或者满足用户定义的覆盖标准、时间设置到期为止。

  

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

• 具体状态：映射所有有具体值的变量；
• 符号状态：仅映射没有具体值的变量。

对于样例代码，执行过程如下：

• 混合执行会生成一些随机的输入值，比如{x=22, y=7}，然后符号化和具体化地一起来执行程序。
• 依据{x=22, y=7}，程序在第7行，这个具体的执行会走向else分支；符号执行沿着执行路径会生成x ≠ 2y0的路径约束；
• 混合测试将路径约束中的连接（x ≠ 2y0）取反，生成一个新的约束x0=2y0，并求解得到测试输入{x=2, y=1}。这个新的输入会强制让程序执行then路径。
• 依据{x=2, y=1}，程序在第8行执行else分支。混合测试会沿着具体执行来进行符号执行，并生成路径约束（x0 = 2y0）∧（x0 ≤ y0 + 10）；
• 混合测试将路径约束中的连接（（x0 ≤ y0 + 10））取反，会生成一个新约束（x0 = 2y0）∧（x0 > y0 + 10）的测试，求解得到测试输入{x=30, y=15}。在这个输入下程序走到ERROR语句。
• 混合测试报告所有被探索的执行路径，并终止测试输入的生成。

比较混合执行测试和传统的符号执行，不难发现由于具体值的引入，简化了约束求解的难度。

3.2、执行生成测试

3.3、选择性符号执行

受路径爆炸与约束求解问题的制约，符号执行不适用于程序规模较大或逻辑复杂的情况。选择性符号执行可以解决这类问题。

选择性符号执行也是具体执行与符号执行混合的一种分析技术，依据特定的分析，决定符号执行与具体执行的切换使用。在选择性符号执行中，用户可以制定一个完整系统中的任意感兴趣额的部分进行符号执行分析，可以是应用程序、库文件、系统内核和设备驱动程序。选择性符号执行在符号执行和具体执行间无缝地来回转换，并透明地转换符号状态和具体状态。选择性符号执行极大地提高了符号执行在实际应用中对大型软件分析测试的可用性，且不再需要对这些环境进行模拟建模。

选择性符号执行的核心是符号执行和具体执行的交互处理,即在具体执行转入符号执行区域及符号执行转入具体执行时的处理。

四、挑战与解决方案

4.1、路径爆炸(Path Explosion)

因为在符号执行的分析过程中，在每个分支节点，符号执行都会衍生出两个符号执行实例，程序分支路径的数量与程序分支的数量呈指数级增长关系。

以下图的代码为例，代码中共有３个分支判断语句和１个循环语句，３个分支判断语句，根据x,y,z值的不同，将会产生８条不同的程序路径；而对于循环来说，当a取最大值时，该循环将会产生231条路径。

 

符号执行在过程处理中默认已经过滤了以下两种路径：

• 不依赖于符号输入的路径
• 对于当前的路径约束，不可解的路径。

但是，尽管符号执行已经做了这些过滤，路径爆炸依旧是符号执行的最大挑战。路径爆炸不是符号执行特有的挑战，是整个程序分析都需要考虑的最大的问题。

   

解决路径爆炸的方案，可以从以下两个角度来考虑：

• 减少路径总数（优先的考虑最有希望的路径， 路径合并，剪枝）；
• 相似的路径不再分析（函数摘要，缓存）；

依据这个思路业界提出了两种解决方案：

• 启发式（Heuristic)： 大多数启发式方法侧重于实现较高的语句和分支覆盖率。

        a）特别有效的方法是使用静态控制流图（CFG）来指导探索，向最接近的路径或优先选择先前执行次数最少的语句；

        b）在每个可行的符号分支，随机选择要探索的一侧； 或者将符号检验与随机检验进行交错进行；

        c）采用先验知识，探索以往容易出错的函数；目前也有研究通过AI的方式得到这些推荐的分析路径；

• 利用完善的程序分析技术(Sound program analysis techniques): 这种方法主要是使用程序分析和软件验证中的各种思想，以合理的方式降低路径探索的复杂性。

        a）静态地合并路径，然后再求解；

        b）通过函数摘要，缓存或重用已经计算过的信息用于后续的计算中；

        c）通过剪枝，去除无关的变量对路径的求解的影响；

4.2、约束求解(Constraint Solving)

4.3、内存建模(Memory Modeling)

四、符号执行工具