符号执行

符号执行引擎是符号执行技术的实现产物，可以用于对程序进行符号执行。一个基本的符号执行引擎由下列部分组成：

1. 状态信息存储器：存储下列符号执行所需状态信息。
   1. ${\displaystyle pc}$ ：指向需要处理的下一条程序语句,其可以是赋值语句、条件分支语句或者是跳转语句；
   2. ${\displaystyle \pi }$ ：指代路径约束信息,表示为执行到程序特定语句需要经过的条件分支，以及各分支处关于符号值${\displaystyle a_{i}}$ 的表达式;
   3. ${\displaystyle \sigma }$ ：表示与程序变量相关的符号值集.
2. 语句执行器：执行每一条语句来获取该程序的控制流程。
3. 约束解算器（英语：constraint solver）：用于在一条路径的符号执行结束后解算路径约束与符号执行结果，为开发者提供一个可供实际执行（英语：concret executino）的值

请看下列代码：

int f() {
  y = read();
  z = y * 2;
  if(z == 12){
    fail();
  }else{
    printf("OK");
  }
}

实际执行时，该方法读入一个值存储于变量y，当y的值为6时，该方法调用fail()，反之打印OK。

在符号执行时，程序读入一个符号值^{[注 1]}λ，并将 λ * 2 赋值给 z。当运行到 if 条件判断语句，由于无法判断 λ * 2 == 12是否为真，符号执行引擎将执行“为真”与“为假”两种分支。执行时，引擎将判断语句处的程序环境与路径约束复制一份并应用于两条分支。本例中， fail() 分支的路径约束指的是判断条件 λ * 2 == 12 ，而print("OK")分支的路径约束为 λ * 2 != 12。路径结束时，约束解算器计算并得出一个对此路径有意义（即能够完成该分支的）输入变量实际值。该值可供帮助开发者复现错误时进行实际执行使用。本例中，fail()分支的一个约束结算结果是6。

路径爆炸

大多数符号执行方法不适用于大型程序：随着程序规模的扩大，程序中有意义的路径成指数级扩大^{[注 2]}。有些程序中存在无尽循环或递归调用，这更大大增加了有意义路径，提高了符号执行难度。^[9] 为解决此问题，马健强（音译，Kin-Keung Ma）等人提出使用启发式路径搜索算法提高代码覆盖率^[10]；马特·斯塔特斯（Matt Staats）等人提出并行执行独立路径的方法来降低符号执行耗时^[11]； 库兹涅佐夫等人则提出了合并相似分支的方法缓解路径爆炸问题^[12]。

待测程序输入变量的特点

由于利用路径分析进行程序分析，对于输入变量范围大，但程序分支较少的程序，符号执行方法比对输入变量进行分析的方法（如动态程序分析）具有较强优势。但是对于输入变量变化范围小，程序分支多的程序，符号执行的效率较低。

内存地址存在别名

由于符号执行根据内存地址分析变量及其变化，对于有内存地址别名^{[注 3]}的程序，符号执行引擎将难以区分不同别名，因此执行结果可能有偏差。^[13]

数组的处理

由于数组是大量不同值（如内存地址）的集合，符号执行引擎需要选择将数组作为一个单独的完整变量处理还是将每一个数组元素作为单独的变量处理。由于引擎无法得知程序中每个数组的意义^{[注 4]}，动态确定每个数组的类型十分具有挑战性。^[13]

存在运行环境交互

当某一程序（如下代码所示）与超出符号执行引擎控制的运行环境有交互（如进行系统调用并获取系统调用返回信息等）时，符号执行将难以完成：

int main()
{
  FILE *fp = fopen("doc.txt");
  ...
  if (condition) {
    fputs("some data", fp);
  } else {
    fputs("some other data", fp);
  }
  ...
  data = fgets(..., fp);
}

该程序将打开一个文件，并根据条件将不同类型的数据写入该文件，然后回读已写入的数据。 从理论上讲，符号执行引擎将在第5行产生两个路径并在第11行返回与在condition变量中的值一致的数据。然而文件操作被实现为内核中的系统调用，符号执行工具无法控制其行为。 解决这一挑战的主要方法是：

在符号执行过程中直接执行系统调用：这种方法的优点是实现起来很简单；缺点是这种调用“并不是符号执行”，其返回内容是实际运行的真实值。

对运行环境建模： 引擎使用模型模拟系统调用，其优点是，能够得到正确的符号执行结果；缺点是需要实现和维护许多可能用到的系统调用模型。 KLEE^[14]、Cloud9和Otter^[15] 等工具通过实现文件系统操作、套接字、IPC等模型采用了这种方法。

创建整个运行环境的状态分支：基于虚拟机技术的符号执行工具通过创建整个VM状态的分支来解决环境问题。比如S2E^[16]中，每个符号执行状态都是一个独立的虚拟机快照。这种方法的空间复杂度较高，对内存的消耗很大。