源码：http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
总结：https://zhuanlan.zhihu.com/p/599054963
Introduction
符号执行的目的是帮助软件测试，在计算机辅助推理领域取得了巨大进步。
符号执行成为了软件安全和验证社区研究的主题，并且该技术已经在漏洞搜索和程序测试中确立了自己的地位。
性能仍然是符号执行的核心挑战：
- 缓慢的处理意味着每次执行和测试的代码更少，因此每个投入的资源检测到的bug更少
- Yun等人最近提供了大量证据，证明执行组件是符号执行的现代实现中的主要瓶颈
现有最先进的符号执行方式：
大多数实现将被测程序转换为中间表示(例如，LLVM位码)，然后进行符号计算（executed symbolically）。从概念上讲，系统一个接一个地循环遍历目标程序的指令，执行所请求的计算，并根据任意符号输入（any symbolic input）跟踪语义。
本质上是一个解释器。更具体地说，除了通常的执行之外，它是用于相应中间表示的解释器，它以符号方式跟踪计算。
一般来说，解释的效率低于编译，因为它在每次执行时执行编译器只需执行一次的工作。因此，我们的核心思想是将“编译而不是解释”应用于符号执行，以获得更好的性能。
在编程语言中，它是用执行等效操作的机器码序列替换源语言指令的过程。为了将同样的思想应用到符号执行中，我们将符号处理嵌入到目标程序中。最终结果是一个无需外部解释器即可执行的二进制文件;它执行与目标程序相同的操作，但额外地跟踪符号表达式。这种技术使它能够执行解释器通常应用的任何符号推理，同时保持编译程序的速度。
符号执行的早期实现中也使用了类似的方法:DART、CUTE和EXE在C源代码级别检测被测程序，但有两个基本问题：
源代码插桩（tie）将它们绑定到一种编程语言中。相反，我们的方法是在编译器的中间表示上工作，因此独立于源语言。
【可能解释】每个编程语言都有不同的语法和结构，所以为不同的编程语言编写和维护插桩逻辑会变得非常复杂
【插桩的含义】在符号执行过程中，程序变量会被映射到符号表达式，用于后续路径约束的生成和求解。这种映射关系的构建需要符号执行引擎对原始程序进行插桩来实现。
处理完整编程语言的要求使得实现非常复杂;这种方法对于C来说可能是可行的，但是对于像C++这样的大型语言来说可能会失败。我们基于编译器的技术只需要处理编译器的中间表示，这是一种小得多的语言。【和上面那条其实类似】
我们在LLVM框架的基础上实现了我们的想法，称为SYMCC。它接受被测程序的未修改的LLVM位码，并将符号执行能力直接编译成二进制文件。在程序的每个分支点，“符号化”二进制文件将生成一个偏离当前执行路径的输入。换句话说，SYMCC生成执行聚合执行的二进制文件，这是一种符号执行，它不同时遵循多个执行路径，而是依赖于一个外部实体(比如fuzzer)来确定测试用例的优先级并编排执行（orchestrate execution）。
在最常见的情况下，SYMCC取代了普通的编译器，并将被测程序的C或c++源代码编译成一个仪表化的二进制文件因此，SYMCC被设计用于分析源代码(或至少LLVM位码)可用的程序，例如在开发期间作为安全开发生命周期的一部分。
Contributions：
- 我们提出了基于编译的符号执行，这种技术在保持低复杂度的同时提供了比当前方法更高的性能。支持额外的源语言可以添加很少的努力；
- 我们展示了SYMCC，我们在LLVM框架之上的开源实现。
- 我们根据最先进的符号执行引擎对SYMCC进行了评估，并表明它在分析现实世界的软件方面提供了好处，从而发现了OpenJPEG中的两个关键漏洞。
Background
Symbolic execution
符号执行的每个实现都是由一组基本构建块构建的。
- Execution：被测程序被执行，系统产生表示计算结果的符号表达式。这些表达式是对程序进行推理的基本资产。出于我们的目的，我们区分了基于IR的执行和不使用IR的执行。
- Symbolic backend：唯一目的是对它们进行推理，例如，生成触发某个安全漏洞的新程序输入。符号后端由推理过程中涉及的组件组成。通常，实现使用SMT求解器，可能通过预处理技术进行增强。例如，KLEE使用精心设计的缓存机制来最小化求解器查询的数量，QSYM从查询中删除所有无关信息以减少求解器的负载。
- Forking（分叉） and scheduling（调度）：两类实现方法
- 只执行一次目标程序，可能沿着给定程序输入指定的路径，并基于该单次执行生成新的程序输入。新的输入通常反馈到系统或传递到并发运行的 fuzzer。这种方法通常被称为concolic执行器，包括SAGE、Driller和QSYM等。
- 通过额外的工具来管理沿着不同路径的被测程序的多次执行。通常，它们在程序的分支点“分叉”执行(为了避免必须从一个新输入开始重新执行);调度程序通常编排不同的执行状态，并根据某种搜索策略对它们进行优先级排序。例如，KLEE， Mayhem和 angr 都遵循这种方法。
路径爆炸问题在第二种方法中更加普遍。分叉系统需要管理每个执行状态的大量信息，而concolic执行器只是生成一个新的程序输入，将其写入磁盘，然后“忘记它”。Mayhem实现了一种混合方法，在有足够内存可用时进行分叉，否则将状态持久化到磁盘。
对于SYMCC，我们决定采用concolic方法，因为我们认为它允许更高的执行速度和更简单的实现。
我们的工作专注于改进执行组件，而我们在符号后端重用Yun等人的工作。
我们研究当前符号执行实现中执行组件的两种流行风格。
IR-based symbolic execution
实现符号执行的一种常用方法是通过中间表示(IR)。与流行的CPU体系结构的本地指令集相比，IR通常在高层次上用更少的指令描述程序行为。因此，为IR实现符号解释器要比直接为机器码实现符号解释器容易得多，因此这是许多最先进的系统所采用的方法。
基于IR的符号执行首先需要将被分析的程序转换成IR。例如，KLEE在LLVM位码上工作，并使用clang编译器从源代码生成它;S2E也解释LLVM位码，但从QEMU的内部程序表示动态生成它，在执行过程中翻译遇到的每个基本块;angr将机器码转换为VEX，即Valgrind框架的IR。
一般来说，IR生成可能需要大量的工作，特别是当它从机器代码开始时。一旦目标程序的IR可用，符号解释器就可以运行它并生成对应于每个计算的符号表达式。表达式通常被传递到符号后端进行进一步处理。
IR-less symbolic execution
虽然将目标程序转换为中间表示简化了符号执行的实现，但解释IR比相应二进制的本机执行要慢得多，特别是在没有符号数据的情况下(即，当不需要符号推理时)。这种观察导致了Triton和QSYM的开发，它们遵循一种不同的方法:不是将被测试的程序翻译成IR然后解释它，而是执行未修改的机器码并在运行时对其进行检测。
具体来说，Triton和QSYM都使用Intel的Pin来控制目标程序的执行。Pin提供了在执行某些机器代码指令时插入自定义代码的工具。符号执行器使用这种机制注入代码，这些代码除了由CPU执行的具体计算之外，还以符号方式处理计算。例如，当CPU准备将两个寄存器中的值相加时，Pin调用符号执行器，它获取寄存器值对应的符号表达式，生成描述和的表达式，并将其与接收计算结果的寄存器关联起来。
- Run-time instrumentation（运行时插桩） 也会带来开销，但比解释 IR 快得多
- 健壮性：如果基于 IR 的系统不知道如何处理某个指令或对某些库函数的调用，它就无法继续，因为解释器无法执行请求的计算；然而，在无 IR 符号执行中，CPU总是可以具体地执行目标程序。注入的分析代码将无法生成适当的符号表达式。
然而，直接在机器码上构建符号执行有相当大的缺点。最值得注意的是，实现需要处理更大的指令集：
通常用于符号执行的 IR 包含几十条不同的指令，而 CPU 指令集很容易达到数百到数千条。符号执行器必须知道如何以符号方式表达每条指令的语义，这将导致更加复杂的实现。另一个问题是体系结构依赖性：机器代码的检测自然是一项依赖于机器的工作。另一方面，IR 通常是架构不可知论者。因此，基于IR的系统可以在任何架构上工作，只要存在从各自的机器码到IR的转换器。这与嵌入式设备领域尤其相关，在该领域中，常见的CPU架构种类繁多。
SYMCC使用IR，因此保留了与基于IR的方法相关的灵活性和实现简单性，然而我们基于编译的技术允许它达到(并超越)无IR系统的高性能，正如我们在第5节中所展示的那样。
Reducing overhead
无论是基于 IR 还是不基于 IR 的符号执行，只有在计算涉及符号数据时，才需要构建符号表达式并将其传递给符号后端。否则，结果完全独立于用户输入，因此与在后端执行的任何推理无关。因此，一种常见的优化策略是将符号处理限制为对符号数据的计算，并采用更快的执行机制，我们称之为具体检查的策略。
在基于IR的实现中，IR的符号解释甚至可以与机器代码在真实或快速仿真CPU上的本机执行交替进行;例如，Angr b就采用了这种方法。实现的具体检查范围各不相同——QSYM决定是否在每条指令的基础上调用符号后端，而angr将钩子放在相关操作(如内存和寄存器访问)上。尽可能多地回到快速执行方案是一个重要的优化，我们也在SYMCC中实现了这一点。
Compilation-based symbolic execution
我们的方法的高级目标是通过将计算的符号处理编译到目标程序中来加速符号执行的执行部分。
Overview
我们将符号解释器(或观察者)的逻辑编译到目标程序中。与符号执行的早期实现相反，我们不是在源代码级别执行这种嵌入，而是使用编译器的中间表示，这使我们能够独立于编写被测程序的源语言，以及独立于目标体系结构。
LLVM位码中的一个示例函数
插入目标程序相关附加指令（黄色框），原始代码依然保留，插入的是对运行时支持库的调用该库构建符号表达式并于SMT求解器交互。
Support library
由于我们将符号执行功能编译到目标程序中，所以典型符号执行引擎的所有组件都需要可用。因此，我们将符号后端绑定到一个供目标程序使用的库中。
该库公开了符号后端的入口点，以便从 the instrumented target 调用，例如，用于构建符号表达式和通知后端有关条件跳转的函数。
Symbolic handlers
编译时转换的核心是插入处理符号计算的调用。编译器遍历整个程序，并为每次计算插入对符号后端的调用。例如，当目标程序检查两个变量的内容是否相等时，编译器插入代码来获取两个操作数的符号表达式，构建结果“等于”表达式，并将其与接收结果的变量相关联(%7)。代码在编译时生成并嵌入到二进制文件中。这个过程取代了传统符号执行引擎在运行时必须执行的大量符号处理。我们的编译器对目标程序精确地进行一次检测，然后生成的二进制文件可以在不同的输入上运行，而不需要重复检测过程，这在与 fuzzer 结合使用时特别有效。此外，插入的处理成为目标程序的一个组成部分，因此它受制于通常的CPU优化，如缓存和分支预测。
Concreteness checks
对运行时支持库的每个插入调用都会引入开销:它最终会调用符号后端，并可能将负载放在 SMT 求解器上。
但是，只有在计算接收符号输入时，才需要涉及符号后端。没有必要通知后端完全具体的计算——我们只会产生不必要的开销。在我们基于编译的方法中，有两个阶段的数据可以被确定为具体的:
- Compile time：编译时常量，如数据结构的偏移量、魔术常量或默认返回值，在运行时永远不会变成符号。
- Run time：在许多情况下，编译器无法知道数据在运行时是具体的还是符号的，例如，当它从内存中读取时:一个内存单元可能包含符号数据或具体数据，并且它的具体性在执行过程中会发生变化。在这些情况下，如果计算的所有输入都是具体的，我们只能在运行时检查并动态地防止调用符号后端。
因此，在我们生成的代码中，如果数据在编译时已知为常数，我们就会省略对符号后端的调用。此外，在其余情况下，我们会插入运行时检查，将后端调用限制在计算中至少有一个输入是符号输入（因此结果也可能是符号输入）的情况。
Implementation of SymCC
我们在 LLVM 编译器框架的基础上构建了 SYMCC。编译时工具是通过从头开始编写的自定义编译器传递实现的。该程序将编译器前端生成的 LLVM 位码走一遍，并插入用于符号处理的代码（如第 3.3 节所述）。插入的代码调用符号后端导出的函数：我们提供了 Z3 SMT 求解器的精简封装，以及与 QSYM更复杂后端的可选集成。编译器传递由大约 1000 行 C++ 代码组成；运行时支持库也是用 C++ 编写的，由另外 1000 行代码组成（不包括 Z3 和可选的 QSYM 代码）。相对较小的代码库表明，该方法概念简单，从而降低了出现实施错误的可能性。
Compile-time instrumentation
由于我们的编译器扩展是作为 LLVM 通道（an LLVM pass）实现的，因此它运行在基于 LLVM 的编译器的 “中间端“（in the “middle-end” of LLVM-based compilers）——在前端将源语言翻译成 LLVM 位码之后，但在后端将位码转换成机器码之前。因此，SYMCC 需要支持 LLVM 位码语言的指令和固有函数。
相对于各种优化步骤而言，SYMCC 的传递位置需要权衡利弊。在优化器的早期阶段，比特码仍与前端生成的非常相似，通常效率较低，但相对简单，而且仅限于 LLVM 比特码指令集的一个子集。相比之下，在优化器流水线的后期阶段，死代码已被优化掉，昂贵的表达式（如乘法）已被更便宜的表达式（如位移）所取代；这种优化后的代码允许使用更少、更便宜的仪器，但需要处理指令集的更大一部分。在当前的实现中，我们的代码在优化流水线的中间运行，在消除死代码和降低强度等基本优化之后，但在矢量器（即在支持的架构上用 SIMD 指令替换循环的阶段）之前。在更晚的时间运行我们的代码可以提高编译后程序的性能，但会使我们的实现复杂化，因为我们需要实现矢量操作的符号处理；我们选择了实现简单化。
Shadow memory
首先，符号表达式与数据相关联的信息被存储在内存中的一个影子区域（shadow region）。运行时支持库会跟踪目标程序中的内存分配，并将它们映射到相应的影子区域，这些影子区域以每页为单位包含了相应的符号表达式。然而，有一个特殊情况：与函数局部变量对应的表达式存储在局部变量本身中。这意味着在代码生成过程中，它们被当作普通数据进行处理；特别是，编译器的寄存器分配器可能会决定将它们放入机器寄存器以实现快速访问。
可以用固定偏移量的方式替换当前的内存分配跟踪方案。这种技术被流行的LLVM santizers所使用。这样做可以实现对符号表达式的常数时间查找，而当前的查找时间与包含符号数据的内存页数成对数关系。
然而，由于内存页数通常很小（根据作者的经验，不超过10页），作者选择了更简单的按需分配的实现方式。
Symbolic backend
提供了两个不同的后端：
第一个是他们自己实现的后端，是对Z3的一个轻量级封装。它作为一个共享对象被打包并链接到被插装的目标程序中。编译器插入对后端的调用，后端构造所需的Z3表达式，并查询SMT求解器以生成新的程序输入。
然而，由于后端大部分与执行组件独立，并且只通过一个简单的接口与执行组件进行通信，我们可以在不影响主要的执行组件的情况下替换它。作者通过集成QSYM后端来展示了这种灵活性，可以选择性地使用该后端，取代他们简单的Z3封装。他们从处理符号表达式的QSYM代码部分编译了一个共享库，将其链接到目标程序，并将仪器化程序中的调用转换成对QSYM代码的调用。他们封装的QSYM代码接口包括一组用于创建表达式的函数（例如，
SymExpr _sym_build_add(SymExpr a, SymExpr b)），以及用于传递调用上下文和路径约束的辅助函数；添加路径约束会通过Z3触发生成新的输入。实际上，这意味着他们可以将QSYM后端中的所有复杂表达式处理功能与依赖跟踪和热代码路径的后退策略等相结合，与自己的快速执行组件一起使用。
Concreteness checks
为了获得良好的性能，我们需要将符号推理(即符号后端的参与)限制在必要的情况下。换句话说，当计算的所有操作数都是具体的时，我们应该避免调用符号后端。
在我们的实现中，符号表达式在运行时被表示为指针，具体值的表达式是空指针。因此，在执行过程中检查给定表达式的具体性是一种简单的空指针检查。在位码的每次计算之前，如果所有操作数都是具体的，则插入一个跳过符号处理的条件跳转;如果至少有一个操作数是符号操作数，则根据需要为其他操作数创建符号表达式，并调用符号后端。显然，当编译器可以推断出一个值是编译时常量，因此在运行时绝不是符号值时，我们就省略了符号处理代码的生成。
Interacting with the environment
传统 一步一步算关系
前面后面加两个 hook，编译阶段加好了，不需要再推导，直接算结果就行（且有优化空间）
