简单理解符号执行技术

0X00 前言

因为最近看的很多静态检测的论文中涉及到了符号执行的概念，而在我第一次听到符号执行实际上是在我的一些搞二进制学长口中，自然认为是和 web 没啥关系，但是现在看来只是因为我我太菜了，很多知识在更高的层次看起来都是交融的，而不是我现在看到的全部都是互不相关的板块，或许这也就是为什么要读研吧， 不读研那就疯狂努力吧 。好了，废话不多讲了，由于我对符号执行的理解没有达到很高的层次，不能进行更详尽的总结分析 ，故我只能在网上找了一些我个人认为总结的比较好，并且通俗易懂的文章进行一些摘录， 在此之前先对这些优秀的作者表示感谢，文章之后我会附上我引用的文章或者论文的链接。

0X01 通俗地解释符号执行

Wiki中的定义是：在计算机科学中，符号执行技术指的是通过程序分析的方法，确定哪些输入向量会对应导致程序的执行结果为某个向量的方法(绕)。通俗的说， 如果把一个程序比作DOTA英雄，英雄的最终属性值为程序的输出（包括攻击力、防御力、血槽、蓝槽），英雄的武器出装为程序的输入（出A杖还是BKB）。那么符号执行技术的任务就是，给定了一个英雄的最终属性值，分析出该英雄可以通过哪些出装方式达到这种最终属性值效果。

可以发现， 符号执行技术是一种白盒的静态分析技术 。即，分析程序可能的输入需要能够获取到目标源代码的支持。 同时，它是静态的，因为并没有实际的执行程序本身，而是分析程序的执行路径 。如果把上述英雄的最终属性值替换成程序形成的bug状态，比如，存在数组越界复制的状态，那么，我们就能够利用此技术挖掘漏洞的输入向量了。

这里再举一个简单的例子，让大家有深刻的理解。

以下面的源代码为例子：

int m=M, n=N, q=Q; 
int x1=0,x2=0,x3=0;
if(m!=0)
{
    x1=-2;
}
if(n<12)
{
    if(!m && q)
    {
        x2=1;
    }
    x3=2;
}
assert(x1+x2+x3!=3)

上述代码是一个简单的 c语言 分支结构代码，它的输入是M,N,Q三个变量；输出是x1,x2,x3的三个变量的和。我们这里设置的条件是想看看什么样的输入向量 的情况下，得到的三个输出变量的和等于3.

那么我们通过下面的树形结构来看看所有的情况：

上面的分析图把所有可能的情况都列举出来了，其中，叶子节点显示的数值表示当前输入情况下，可以得到的数值。（比如，如果英雄出装是M^(N<12)，那么最终的属性值R=0）。其中M^(N<12)表达的是，M是非零值且N要小于12，Q为任意值的情况下，得到R=0。可以发现，当条件为~M^(N<5)^Q时，得到了最终结果等于3.即，我们通过这种方式逆向发现了输入向量。 如果把结果条件更改为漏洞条件，理论上也是能够进行漏洞挖掘了。

对于如何根据最终得到的结果求解输入向量，已经有很多现成的数学 工具 可以使用。上述问题其实可以规约成约束规划的求解问题（更详细的介绍看这里： Constraint_programming ）。比较著名的工具比如SMT（Satisfiability Modulo Theory，可满足性模理论）和SAT。

但是在实际的漏洞分析过程中，目标程序可能更加复杂，没有我们上面的例子这么简单。 实际的程序中，可能包含了与外设交互的系统函数，而这些系统函数的输入输出并不会直接赋值到符号中，从而阻断了此类问题的求解 。

比如下面的这个包含了文件读写的例子：

int main(int argc, char* argv[])
{
    FILE *fop = fopen("test.txt");
    ...
    if(argc > 3)
    {
        fputs("Too many parameters, exit.", fop);
    }
    else
    {
        fputs("Ok, we will run normally.", fop);
    }
    ...
    output = fgets(..., fop);
    assert(！strcmp(output, "Ok, we will run normally."));
    return 0;
}

上述示例代码中，想要发现什么情况下会得到输出”Ok, we will run normally.”这个字符串。通过一系列的执行到if语句，此时，根据输入的参数个数将会产生两个分支。分支语句中将执行系统的文件写操作。 在传统的符号执行过程中，此类函数如果继续沿着系统函数的调用传递下去的话，符号数值的传递将会丢失。 而在之后的output = fgets(…, fop);这行代码中，符号从外部获得的数值也将无法正常的赋值到output中。因此，符号执行无法求解上述问题， 因为在调用系统函数与外设交互的时候，符号数值的赋值过程被截断了。

为了解决这个问题，最经典的项目就是基于LLVM的KLEE（ klee )它把一系列的与外设有关的系统函数给重新写了一下，使得符号数值的传递能够继续下去。从比较简化的角度来说，就是把上面的fputs函数修改成，字符串赋值到某个变量中，比如可以是上面的fop里面。再把fgets函数修改成从某个变量获取内容，比如可以是把fop的地址给output。这样，就能够把符号数值的传递给续上。当然，这里举的例子是比较简单的例子，实际在重写函数的时候，会要处理更复杂的情况。在KLEE中，它重新对40个系统调用进行了建模，比如open, read, write, stat, lseek, ftruncate, ioctl。感兴趣的读者可以进一步阅读他们发表在OSDI2008年的论文（ KLEE-OSDI08 )他们的文章深入浅出，非常适合学习。

0X02 从公式原理上理解符号执行

符号执行的关键思想就是， 把输入变为符号值，那么程序计算的输出值就是一个符号输入值的函数 。这个符号化的过程在上一篇AEG文章中已有简要阐述，简而言之，就是一个程序执行的路径通常是true和false条件的序列，这些条件是在分支语句处产生的。在序列的i^{th} 位置如果值是true，那么意味着i^{th} 条件语句走的是then这个分支；反之如果是false就意味着程序执行走的是else分支。

那么，如何形式化地表示符号执行的过程呢？程序的所有执行路径可以表示为树，叫做执行树。接下来我们就以一个例子来阐述通过符号执行遍历程序执行树的过程。

左边的代码中，testme()函数有3条执行路径，组成了右图中的执行树。直观上来看，我们只要给出三个输入就可以遍历这三个路径，即图中绿色的x和y取值。符号执行的目标就是能够生成这样的输入集合，在给定的时间内探索所有的路径。

为了形式化地完成这个任务，符号执行会在全局维护两个变量 。其一是符号状态 $\sigma$ ，它表示的是一个从变量到符号表达式的映射 。其二是符号化路径约束 PC，这是一个无量词的一阶公式，用来表示路径条件 。在符号执行的开始，符号状态$\sigma$ 会先初始化为一个空的映射，而符号化路径约束PC初始化为true。 $\sigma$ 和PC在符号执行的过程中会不断更新。

在符号执行结束时，PC就会用约束求解器进行求解，以生成实际的输入值。这个实际的输入值如果用程序执行，就会走符号执行过程中探索的那条路径，即此时PC的公式所表示的路径

我们以左图的例子来阐述这个过程。当符号执行开始时，符号状态$\sigma$ 为空，符号路径约束PC为true。当我们遇到一个读语句，形式为var=sym input()，即接收程序输入，符号执行就会在符号状态$\sigma$ 中加入一个映射$var\rightarrow s$，这里s就是一个新的未约束的符号值。左图中代码，main()函数的前两行会得到结果$\sigma =\left{ x\rightarrow x {0}, y\rightarrow y {0}\right}$，其中$x {0}$ 和$y_{0}$ 是两个初始的未约束的符号化值。

当我们遇到一个赋值语句，形式为 v=e，符号执行就会将符号状态$\sigma$ 更新，加入一个v到$\sigma \left( e \right)$ 的映射 ，其中$\sigma \left( e \right)$ 就是在当前符号化状态计算e得到的表达式 。例如，在左图中代码执行完第6行时，$\sigma =\left{ x \rightarrow x {0}, y \rightarrow y {0}, z \rightarrow 2y_{0}\right}$ 。

当我们遇到条件语句if(e) S1 else S2，PC会有两个不同更新 。首先是PC更新为PC$\wedge \sigma \left( e \right)$，这就表示then分支 ；然后是建立一个路径约束PC’ ，初始化为PC$\wedge \neg \sigma \left( e \right)$ ，这就表示else分支 。如果PC是可满足的，给一些实际值，那么程序执行就会走then分支，此时的状态为：符号状态$\sigma$ 和符号路径约束PC。反之如果PC’是可满足的，那么会建立另一个符号实例，其符号状态为$\sigma$ ，符号路径约束为PC’，走else分支。如果PC和PC’都不能满足，那么执行就会在对应路径终止。例如，第7行建立了两个不同的符号执行实例，路径约束分别是$x {0} =2y {0}$和$x {0} \ne 2y {0}$。在第8行，又建立了两个符号执行实例，路径约束分别是$\left( x {0} =2y {0} \right) \wedge \left( x {0}>y {0}+10 \right)$ ，以及$\left( x {0} =2y {0} \right) \wedge \left( x {0} \leq y {0}+10 \right)$ 。

如果符号执行遇到了exit语句或者错误（指的是程序崩溃、违反断言等），符号执行的当前实例会终止，利用约束求解器对当前符号路径约束赋一个可满足的值，而可满足的赋值就构成了测试输入：如果程序执行这些实际输入值，就会在同样的路径结束。例如，在左图例子中，经过符号执行的计算会得到三个测试输入：{x=0, y=1}, {x=2, y=1}, {x=30, y=15}。

当我们遇到了循环和递归应该怎么办呢？ 如果循环或递归的终止条件是符号化的，包含循环和递归的符号执行会导致无限数量的路径 。比如上图中的这个例子，这段代码就有无数条执行路径，每条路径的可能性有两种：要么是任意数量的true加上一个false结尾，要么是无穷多数量的true。我们形式化地表示包含n个true条件和1个false条件的路径， 其符号化约束如下：

$$(\wedge {i\in [1,n]}N {i} >0) \wedge (N_{n+1}\leq 10)$$

其中每个$N {i}$ 都是一个新的符号化值，执行结尾的符号化状态是$\left{ N\rightarrow N {n+1} ,sum\rightarrow \sum {i\in [1,n]}^{}{N {i}} \right}$ 。其实这就是符号执行面临的问题之一，即如何处理循环中的无限多路径。在实际中， 有一些方法可以应对，比如对搜索加入限制，要么是限制搜索时间的长短，要么是限制路径数量、循环迭代次数、探索深度等等。

还需要考虑到的一个问题就是， 如果符号路径约束包含不能由求解器高效求解的公式怎么办 ？比如说，如果原本的代码发生变化，把twice函数替换为下图中的语句，那么符号执行就会产生路径约束$x {0}\ne (y {0} y {0}) mod 50$以及$x {0}= (y {0} y {0}) mod 50$。

我们做另外一个假设，如果twice是一个我们得不到源码的函数，也就是我们不知道这个函数有什么功能，那么符号执行会产生路径约束$x {0}\ne twice(y {0})$ 和 $x {0}= twice(y {0})$ ，其中twice是一个未解释的函数。这两种情况下，约束求解器都是不能求解这样的约束的，所以符号执行不能产生输入。

解决方法是一种叫做动态符号执行的技术，我们会在后面的小节中介绍。

0X03 符号执行的具体流程

符号执行分为 过程内分析 和 过程间分析 （又称全局分析）。 过程内分析是指只对单个过程的代码进行分析，全局分析指对整个软件代码进行上下文敏感的分析。 所谓上下文敏感分析是指在当前函数入口点要考虑当前的函数间调用信息和环境信息等。程序的全局分析是在过程内分析的基础上进行的，如果过程内分析中包含了函数调用，就引入了过程间分析， 因此两者之间是相对独立又相互依赖的关系。

(1)过程内分析流程如下图所示

首先，对待分析的单个过程代码对象构建控制流图（Control Flow Graph，CFG）。控制流图（CFG）是编译器内部用有向图表示一个程序过程的一种抽象数据结构，图中的节点表示一个程序基本块，基本块是没有任何跳转的顺序语句代码块，图中的边表示代码中的跳转，它是有向边，起点和终点都是基本块。在CFG上从入口节点开始模拟执行， 在遇到分支节点时，使用约束求解器判定哪条分支可行，并根据预先设计的路径调度策略实现对该过程所有路径的遍历分析 ，最后输出每条可执行路径的分析结果。其中约束求解是数学上的判定过程，形象地说是对一系列的约束方程进行求解。

如果要进行源代码的安全性检测，则需要在过程内分析时，根据具体的安全知识库来添加安全约束。例如，如果要添加缓冲区溢出的安全约束，则在执行时遇到对内存进行操作的语句时，就要对该语句所操作的内存对象的边界添加安全约束。以上面的方式来进行安全约束的添加， 并且每次在添加之后就使用约束求解器对所有的安全约束进行求解，以判定当前是否可能潜在一个安全问题。

(2)程序全局分析流程如下图所示：

首先，为整个程序代码构建函数调用图（Call Graph，CG），在函数调用图中，节点表示函数，边表示函数间的调用关系。根据预设的全局分析调度策略，对CG中的 每个节点（对应一个函数）进行过程内分析 ，最终给出CG每种可行的调用序列的分析结果。

0X04 动态符号执行

符号执行在发展过程中出现了一种叫做动态符号执行的方法（concrete and symbolic， concolic）。 动态符号执行是以具体数值作为输入来模拟执行程序代码 ，与传统静态符号执行相比，其输入值的表示形式不同。动态符号执行使用具体值作为输入，同时启动代码模拟执行器，并从当前路径的分支语句的谓词中搜集所有符号约束。然后修改该符号约束内容构造出一条新的可行的路径约束，并用约束求解器求解出一个可行的新的具体输入，接着符号执行引擎对新输入值进行一轮新的分析。通过使用这种输入迭代产生变种输入的方法，理论上所有可行的路径都可以被计算并分析一遍。

动态符号执行相对于静态符号执行的优点是每次都是具体输入的执行，在模拟执行这个过程中 ，符号化的模拟执行比具体化的模拟执行的开销大很多 ；并且模拟执行过程中所有的变量都为具体值，而不必使用复杂的数据结构来表达符号值，使得模拟执行的花销进一步减少。 但是动态符号执行的结果是对程序的所有路径的一个下逼近，即其最后产生路径的集合应该比所有路径集合小， (但这种情况在软件测试中是允许的)

我们依旧以上图的这个程序的例子来说明。Concolic执行会先产生一些随机输入，例如{x=22, y=7}，然后同时实际地和符号化地执行程序。这个实际执行会走到第7行的else分支，符号化执行会在实际执行路径生成路径约束$x {0} \ne 2 y {0}$。然后concolic执行会将路径约束的连接词取反，求解$x {0} = 2 y {0}$得到一个测试输入{x=2, y=1}，这个新输入就会让执行走向一条不同的路径。之后，concolic执行会在这个新的测试输入上再同时进行实际的和符号化的执行，执行会取与此前路径不同的分支，即第7行的then分支和第8行的else分支，这时产生的约束就是$(x {0}=2y {0})\wedge (x {0}\leq y {0}+10)$，生成新的测试输入让程序执行没有被执行过的路径。再探索新的路径，就需要将上述的条件取反，也就是$(x {0}=2y {0})\wedge (x {0}> y {0}+10)$，通过求解约束得到测试输入{x=30, y=15}，程序会在这个输入上遇到ERROR语句。如此一来，我们就完成了所有3条路径的探索。

这个过程中，我们从一个实际输入{x=22, y=7}出发，得到第一个约束条件$x {0} \ne 2 y {0}$，第一次取反得到$x {0} = 2 y {0}$，从而得到测试输入{x=2, y=1}和新约束$(x {0}=2y {0})\wedge (x {0}\leq y {0}+10)$；$(x {0}=2y {0})\wedge (x {0}> y {0}+10)$，从而求解出测试输入{x=30, y=15}。

注意在这个搜索过程中 ，其实concolic执行使用了深度优先的搜索策略。

Cristian Cadar在2006年发表EXE，以及2008年发表EXE的改进版本KLEE，对上述concolic执行的方法做了进一步优化。其创新点主要是在实际状态和符号状态之间进行区分，称之为执行生成的测试（Execution-Generated Testing），简称EGT。这个方法在每次运算前动态检查值是不是都是实际的，如果都是实际的值，那么运算就原样执行，否则，如果至少有一个值是符号化的，运算就会通过更新当前路径的条件符号化地进行。例如，对于我们的例子程序，第17行把y=sym_input()改变成y=10，那么第6行就会用实际参数20去调用函数twice，并实际执行。然后第7行变成if(20==x)，符号执行会走then路径，加入约束x=20；对条件进行取反就可以走else路径，约束是x≠20。在then路径，第8行变成if(x>20)，那么then路径就不能走了，因为此时有约束x=20。简言之，EGT本质上还是将实际执行与符号执行相结合，通过路径取反探索所有可能路径。

正是因为concolic执行的出现，让传统静态符号执行遇到的 很多问题能够得到解决——那些符号执行不好处理的部分、求解器无法求解的部分，用实际值替换就好了 。使用实际值，可以让因外部代码交互和约束求解超时造成的不精确大大降低，但 付出的代价就是，会有丢失路径的缺陷，牺牲了路径探索的完全性 。

我们举一个例子来说明这一点。假设我们原始例子程序做了改动，即把twice函数的定义改为返回(v*v)%50。假设执行从随机输入{x=22, y=7}开始，生成路径约束$x {0}\ne (y {0} y {0}) mod 50$。因为约束求解器无法求解非线性约束，所以concolic执行的应对方法是，把符号值用实际值替换，此处会把$y {0}$的值替换为7，这就将程序约束简化为$x {0}\ne49$。通过求解这个约束，可以得到输入${x=49, y=7}$，走到一个此前没有走到的路径。传统静态符号执行是无法做到这一步的。但是，在这个例子中，我们无法生成路径true, false的输入，即约束$x {0}= (y {0} y {0}) mod 50\wedge (x {0}\leq y {0}+10)$，因为$y_{0}$的值已经实际化了，这就造成了丢失路径的问题，造成不完全性。

然而总的来说，concolic执行的方法是非常实用的，有效解决了遇到不支持的运算以及应用与外界交互的问题。比如调用库函数和OS系统调用的情况下，因为库和系统调用无法插桩，所以这些函数相关的返回值会被实际化。

0X05 挑战&解决方案

符号执行曾经遇到过很多问题，使其难以应用在真实的程序分析中。经过研究者的不懈努力，这些问题多多少少得到了解决，由此也产生了一大批优秀的学术论文。这一部分将简单介绍其中的一些关键挑战以及对应的解决方案。

1.路径选择

由于在 每一个条件分支都会产生两个不同约束，符号执行要探索的执行路径依分支数指数增长 。在时间和资源有限的情况下， 应该对最相关的路径进行探索 ，这就涉及到了路径选择的问题。通过路径选择的方法缓解指数爆炸问题， 主要有两种方法：

1）使用 启发式函数 对路径进行搜索，目的是先探索最值得探索的路径；

2）使用一些 可靠的程序分析技术 减少路径探索的复杂性。

启发式搜索是一种路径搜索策略，比深度优先或者广度优先要更先进一些。大多数启发式的主要目标在于获得较高的语句和分支的覆盖率，不过也有可能用于其他优化目的。最简单的启发式大概是随机探索的启发式，即在两边都可行的符号化分支随机选择走哪一边。还有一个方法是，使用静态控制流图（CFG）来指导路径选择， 尽量选择与未覆盖指令最接近的路径 ， 另一个方法是符号执行与进化搜索相结合 ,其fitness function用来指导输入空间的搜索，其关键就在于fitness function的定义，例如利用从动态或静态分析中得到的实际状态信息或者符号信息来提升fitness function。

用程序分析和软件验证的思路去减少路径探索的复杂性，也是一种缓解路径爆炸问题的方式。

(1)通过静态融合减少需要探索的路径:具体说来就是使用select表达式直接传递给约束求解器，但实际上是将路径选择的复杂性传递给了求解器，对求解器提出了更高的要求。

(2)重用:即通过缓存等方式存储函数摘要，可以将底层函数的计算结果重用到高级函数中，不需要重复计算，减小分析的复杂性。

(3)去除冗余路径：RWset技术的关键思路就是，如果程序路径与此前探索过的路径在同样符号约束的情况下到达相同的程序点，那么这条路径就会从该点继续执行，所以可以被丢弃。

2.约束求解

符号执行在2005年之后的突然重新流行，一大部分原因是因为求解器能力的提升，能够求解复杂的路径约束。但是 约束求解在某种程度上依然是符号执行的关键瓶颈之一 ，也就是说符号执行所需求的约束求解能力超出了当前约束求解器的能力。所以， 实现约束求解优化就变得十分重要 。

这里主要介绍两种优化方法： 不相关约束消除 ， 增量求解 。

1.不相关约束消除

在符号执行的约束生成过程中，尤其是在concolic执行过程中， 通常会通过条件取反的方式增加约束 ，一个已知路径约束的分支谓词会取反，然后结果的约束集会检查可满足性以识别另一条路径是否可行。一个很重要的现象是， 一个程序分支通常只依赖一小部分程序变量，所以我们可以尝试从当前路径条件中移除与识别当前分支结果不相关的约束 。

例如，当前的路径条件是$(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的约束，因为对$\neg (y<12)$ 的分支是不会有影响的。 减小的约束集会给出x和y的新值，我们用此前执行的z值就可以生成新输入了。如果更形式化地说，算法会计算在取反条件所依赖的所有约束的传递闭包。

2.增量求解

另一种方法本质上也是利用重用的思想 。符号执行中生成的约束集有一个重要特性，就是表示为程序源代码中的静态分支的固定集合。所以，很多路径有相似的约束集，可以有相似的解决方案 。 通过重用以前相似请求的结果，可以利用这种特性来提升约束求解的速度 ，这种方法在CUTE和KLEE中都有实现。

举个例子来说明，在KLEE中，所有的请求结果都保存在缓存中，该缓存将约束集映射到实际变量赋值。例如，缓存中的一个映射可能是$(x+y<10)\wedge (x="">5)\Rightarrow\left{ x=6, y=3 \right}$使用这些映射，KLEE可以迅速解答一些相似的请求类型，包括已经缓存的约束集的子集和超集。比如对于请求$(x+y<10)\wedge (x="">5)\wedge(y\geq 0)$，KLEE可以迅速检查{x=6, y=3}是一个可行的答案。这样就可以让求解过程加快很多。

3.内存建模

程序语句如何精确地翻译为符号化约束对符号执行得到的覆盖率有很大影响。内存建模就是一个很大的问题，在访问内存的时候， 内存地址用来引用一个内存单元，当这个地址的引用来自于用户输入时，内存地址就成为了一个表达式。当符号化执行时，我们必须决定什么时候将这个内存的引用进行实际化 。一个可靠的策略是，考虑从任何可能满足的赋值加载，但这个可能值的空间很大，如果实际化不够精确，会造成代码分析的不精确 。还有一个是别名问题，即地址别名导致两个内存运算引用同一个地址，比较好的方法是进行别名分析 ，事先推理两个引用是否指向相同的地址，但这个步骤要静态分析完成。KLEE使用了别名分析和让SMT考虑别名问题的混合方法。而DART和CUTE压根没解决这个问题，只处理线性约束的公式，不能处理一般的符号化引用。

符号化跳转也是一个问题，主要是switch这样的语句，常用跳转表实现，跳转的目标是一个表达式而不是实际值。

以往的工作用三种处理方法。

1）使用concolic执行中的实际化策略，一旦跳转目标在实际执行中被执行，就可以将符号执行转向这个实际路径，但缺陷是实际化导致很难探索完全的状态空间，只能探索已知的跳转目标。

2）使用SMT求解器。当我们到达符号跳转时，假设路径谓词为$\Pi$,跳转到e，我们可以让SMT求解器找到符合$\Pi \wedge e$的答案。但是这种方案相比其他方案效率会低很多。

3）使用静态分析，推理整个程序，定位可能的跳转目标。实际中，源代码的间接跳转分析主要是指针分析。二进制的跳转静态分析推理在跳转目标表达式中哪些值可能被引用。例如，函数指针表通常实现为可能的跳转目标表。