符号执行

foresta.yang2023-12-182024-04-25

符号执行

符号执行是什么

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

符号执行的优势

生成具体测试输入的能力是符号执行的主要优势之一：

从测试生成的角度来看，它允许创建高覆盖率的测试套件，而从bug查找的角度来看，它为开发人员提供了触发bug的具体输入，该输入可用于确认和调试打开的错误。

符号执行过程

在任何时候，符号执行引擎都维持一个状态（stmt，σ，π）。

stmt是下一个要评估的语句。目前，我们假设stmt可以是赋值，条件分支或跳转。
σ是一个符号存储，它将程序变量与具体值或符号值αi上的表达式相关联。
π表示路径约束，即，是表示由于在执行中为了达到stmt而采取的分支而对符号αi的一组假设的公式。在分析开始时，π=真。

下面是一个简单的符号执行的样例。

在沿着程序的执行路径的符号执行结束时，使用约束求解器来求解π以生成具体的输入值。

符号执行实现的两种方案

1）基于IR的符号执行:IRs实现解释器比直接为机器代码实现符号解释器容易得多，因此这是许多系统所采用的方法,但是IR生成可能需要大量的工作, 而且解释IR要比相应二进制文件的本机执行慢得多。
2）无IR的符号执行:不是将被测程序翻译成IR然后解释，而是执行未修改的机器代码，并在运行时对其进行检测, 但是一般机器指令较多, 实现起来没有基于IR的符号执行简单。

Concolic执行

Concolic执行维护一个实际状态和一个符号化状态：实际状态将所有变量映射到实际值，符号状态只映射那些有非实际值的变量。Concolic执行首先用一些给定的或者随机的输入来执行程序，收集执行过程中条件语句对输入的符号化约束，然后使用约束求解器去推理输入的变化，从而将下一次程序的执行导向另一条执行路径。

简单地说来，就是在已有实际输入得到的路径上，对分支路径条件进行取反，就可以让执行走向另外一条路径。这个过程会不断地重复，加上系统化或启发式的路径选择算法，直到所有的路径都被探索，或者用户定义的覆盖目标达到，或者时间开销超过预计。

我们依旧以上面那个程序的例子来说明。我们从一个实际输入{a=0, b=7}出发，符号化执行得到第一个约束条件a0 == 0，第一次取反得到a0 != 0 ，从而得到测试输入{x=2, y=1}和新约束(a0 != 0) & (b0 !=0)；第二次取反得到(a0 != 0) & (b0 ==0)，从而求解出测试输入{x=1, y=0}。

混合模糊

模糊技术可以以近乎自然的速度快速探索输入空间，但它只擅长于发现导致执行路径具有松散分支条件（如x>0）的输入。相反，concolic执行擅长于找到将程序驱动到紧凑而复杂的分支条件的输入，例如x==0xdeadbeef，但是计算和解决这些约束非常昂贵且缓慢。

将模糊化和concolic执行结合起来，希望模糊程序能快速地探索琐碎的输入空间（即松散条件），concolic执行能解决复杂的分支。

Driller

比较早(2016年)将符号执行和模糊测试结合的工具是Driller.Driller是基于fuzz工具AFL和符号执行工具angr来实现的，当模糊程序卡住时调用符号执行来求解能够到达新路径的输入，使得fuzz能够快速突破条件判断语句。

具体实现是，通过监测AFL的执行，可以决定什么时候开始符号执行以探索新路径。如果AFL执行了x轮后，bitmap上显示没有发现新的状态转换（也即新的代码块转移），说明AFL卡住了，这时候调用angr进行符号执行。

每个具体输入对应于PathGroup中的单个路径，在PathGroup的每一步中，检查每个分支以确保最新的跳转指令引入先前AFL未知的路径。当发现这样的跳转时，SMT求解器被查询以创建一个输入来驱动执行到新的跳转。这个输入反馈给AFL，AFL在未来的模糊步骤中进行变异。这个反馈循环使我们能够将昂贵的符号执行时间与廉价的模糊时间进行平衡，并且减轻了模糊对程序操作的低语义洞察力。

QSYM

2018年一款新的混合模糊引擎QSYM被提出，它的作者观察到，他们的 concolic executors的性能瓶颈是阻止他们被复杂的实际应用所采用的主要限制因素。

下面讲述了QSYM的作者任务影响符号执行性能的因素。

1)慢符号执行

现有的协同执行器选择IR来大大降低它们的实现复杂度；然而，这牺牲了性能。此外，加速IR使用的优化禁止了进一步的优化机会，特别是通过以基本块粒度将程序转换为IRs。此设计不允许跳过不涉及符号执行指令的仿真指令。

首先，IR翻译本身增加了开销。在大多数情况下，机器指令的翻译会导致多条IR指令。从而产生了大量的符号模拟处理.

如果基本块不处理任何符号变量，它们就不会在模拟器中执行。虽然这有效地减少了开销，但仍有优化的空间。根据我们对libjpeg、libpng、libtiff和file等真实软件的测量，符号基本块中只有30%的指令需要符号执行。这个这意味着一个指令级的方法有机会减少不必要的符号执行的数量。然而，由于IR缓存的原因，当前的concolic执行器不容易采用这种方法。

2)无效的快照

常规concolic执行引擎使用快照技术来减少在探索目标程序的多条路径时重新执行目标程序的开销。

引擎在一个分支中备份程序的符号状态，然后探索其中一条路径。

当路径耗尽或卡住时，发动机将符号状态恢复到分支上的先前状态，并移动到另一条路径。

引擎可以探索路径，而无需支付重新执行分支程序的费用。

为什么说快照是无效的?

第一，混合模糊中的concolic执行引擎从fuzzer中获取多个测试用例，这些测试用例与程序的不同路径相关联（即，不共享公共分支）.

第二，快照机制由于打破了进程边界,快照机制成为支持外部环境的问题.

当一个程序通过fork（）发散-就像系统调用一样，内核不再维护与外部环境相关的内部状态。因此，协同执行引擎应该自己维护状态.

通过全系统的concolic执行或外部环境建模来解决这个问题，但是它们分别导致了显著的性能降低和不准确的测试，而且快照无法反映外部状态。

3)缓慢而不灵活的可靠分析

concolic执行试图==通过收集完整的约束来保证可靠性。==这种完整性确保满足约束的输入将导致执行到预期的路径。但是，计算完全约束在各种情况下都是昂贵的,并且有可能陷入对复杂事物的永无止境的分析逻辑.例如。下的上半部分显示了文件程序的代码片段。它卡在计算zlib解压的复杂约束，无法搜索其他有趣的代码。