带你搞懂符号执行的前世今生与最近技术( 五 ) _符号执行

我们使用了一种乐观的清除机制，在一种expression garbage collector的基础之上：SYMQEMU跟踪所有从后端获得的符号表达式，如果他们的数目非常大时进行回收。最主要的观测是所有live表达式可以通过扫描如下发现

模拟的CPU符号寄存器
存储对应符号内存结果的符号表达式的，内存中的shadow regions

以上两种，后端都是可感知的。在感知到所有live表达式之后，symqemu将其与所有已经创建的符号表达式进行比较，并且释放那些不再使用的表达式。尤其是当一个程序在寄存器和内存中移除了计算的结果，对应的符号表达式同样被认为不再使用也被移除。我们将 expression garbage collector 和QSYM’s smart pointer based memory management相联系，这两种基础都认为表达式不再使用之后可以被释放。
修改TCG ops我们的方法要求能够像TCG ops中插桩。然而TCG不支持在翻译过程之中的拓展修改功能，作为一个翻译器，他高度关注速度问题。因为，对于TCG ops的程序化修改的工作很少。然而LLVM提供了丰富的API，支持compiler检查和修改LLVM bitcode 。TCG ops单纯的将指令存储在一个平面链表中，而没有任何高层次的类似于基本快的数据结构。并且程序流被期望与翻译块呈线性关系。
为了不和TCG产生不一致，我们的实现对每一个指令生成时进行符号处理。虽然这种方法可以避免与TCG 优化以及代码生成器产生的问题，但是使得静态优化技术不可行，因为我们每次仅仅关注一条指令。尤其是我们无法静态确定给定的值是否是实际值，并且如果所有的操作都是符号值的情况下，我们也不能产生跳过符号计算的阶段的跳转。
因此我们最终于TCG所需要的运行环境的限制条件达成了妥协，同时允许我们有相关很高的执行速度：我们在支持的调用库中进行实际值性检查，这样，如果实际计算的输入都是准确值的话，就可以直接跳过符号值计算，但是这样会导致额外的库调用开销。
shadow call stackQSYM引入了上下文敏感的基本快剪枝，如果在同样的调用堆栈环境中频繁调用确定的计算会导致压抑符号执行(基于如下直觉，在同样的上下文环境中重复的执行分析并不会导致新的发现) 。为了实现这个优化，符号执行需要维护一个shadow call stack，记录跟踪call以及return指令。
在qemu基础之上，我们面临一个新的挑战，TCG ops是一个非常低级别的target程序的中间表示。尤其是，call以及return指令不是被表示为单独的指令而是被翻译为一系列TCG ops 。比如一个在x86架构下的程序调用会生成TCG ops，其将返回地址push到模拟的stack上，调整guest的stack pointer，并且根据被调用函数来修改guest的指令。这使得仅仅通过检测TCG ops来以一个可靠并且架构独立的方式来识别call以及return是不可能的。我们选择了如下优化来提高鲁棒性：在架构独立的，能够将机器代码转换为TCG ops的qemu 代码中，每当遇到call和return时，我们会通知代码生成器。缺点就是针对每个target架构，类似的通知代码都必须被插入到翻译代码中去，但这并不复杂。
评价
详见原文，主要是一些指标与测试效果
未来工作全系统仿真SYMQEMU目前运行符号执行针对linux用户态二进制程序，之后将会对其拓展到全系统分析，尤其是针对嵌入式设备而言，分析此类程序要求全系统仿真。
我们认为在SYMQEMU实现这一改进是可能的。将target翻译为TCG ops，对其插桩，并将其编译为机器码，这些基本过程不改变。需要添加的一个机制是将符号化数据引入到guest系统中，这是受到S2E fake-instruction技术的启发，以及当在guest内存以及符号表达式之间存在映射时，shadow-memory系统需要记录虚拟MMU的数量。最终将会产生一个不仅可以对用户态程序进行测试，同样可以对内核代码进行测试的系统，并且其同样可分析非linux系统的代码以及裸固件等。
caching across executions混合fuzzing技术的特点之一是能够对同一程序进行大量的连续执行。作为动态翻译器，SYMQEMU在运行态按需翻译target程序。并且翻译的结果在单个运行的过程之中被缓存，但是当目标程序执行终止时这些缓存结果会被丢弃。我们猜想，可以通过缓存多个执行过程中的翻译结果，可以显著提升结合SYMQEMU的混合FUZZ的性能。主要的挑战就是需要确定目标是确定性加载的，以及针对自我修改代码需要进行特殊处理。所以，这些潜在的优化性能提升主要在于被测程序的特点。
symbolic QEMU helpersQEMU利用TCG ops表示机器码，然而一些target的指令难以用TCG ops来进行表示，尤其是在CISC架构之上。针对这情况，QEMU使用helpers:可以被TCG调用的内置变异函数，仿真target架构的每一个复杂指令。由于helpers工作在常规的TCG架构之外，SYMQEMU在TCG层级的插桩不能插入符号处理到他们之中。这样的结果是implicit concretization，在分析使用大量目标的指令时会产生精读损失。