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

我们有如下两种实现qemu helpers符号处理的方式：

第一种方式是为每一个要求的helper手动添加符号等价式，更像在一些符号执行引擎中使用的常用libc功能的函数总结。这个方式非常容易实现，但是不方便应用于大数量的helpers中。
另一种方式是自动化的实现helpers的符号化版本。为了实现这个目的，SYMCC可以被用来编译符号化追踪到helpers中，他的源代码作为QEMU的一部分是公开的。最终得到的二进制文件是和SYMQEMU兼容的，因为SYMCC的使用相同的符号推理的后端。S2E也是使用类似的方式编译helpers到KLEE中的解释器中的LLVM bitcode 。

相关工作

binary-only符号执行Mayhem是一个高性能的基于解释器的符号执行系统，赢得过DAPRA CGC比赛，然而由于其不开源无法比较性能。Triton是可以以两种方式运行的符号执行系统，一种使用二进制文件转换，类似于QSYM，一种使用CPU仿真，类似于S2E以及angr 。Eclipser覆盖了介于fuzzing和符号执行之间的一些中间区域，他认为在分支条件和输入数据之间存在线性关系。这种约束的简化提升了系统的性能，然而他却不能发现常规符号执行系统可以发现的那些路径。Redqueen利用一种启发式的方法寻找路径条件和输入之间的关系。SYMQEMU相比较来说实现了全系统仿真。
运行态bug检测混合fuzzing依靠fuzzer以及sanitizers来检测bugs 。Address sanitizer是一种流行的用来检测确定内存错误的sanitizer 。由于其需要源代码来产生插桩程序，Fioraldi et al设计了QASan，基于qemu的系统来对二进制文件实现类似的检测。有大量的需要源代码的sanitizers 。我们推测通过QASan的思路，可以将大量上述sanitizers用于二进制文件分析。
混合fuzzingDriller是基于angr的混合fuzzer，其设计理念类似于QSYM，但是有其angr的python实现以及基于解释器的方式，其执行速度较低。与QSYM以及SYMQEMU比较，它使用了一种更加精细的策略来融合fuzzer以及符号引擎：他监控fuzzer的进展情况，并且当其似乎遇到自身无法解决的障碍时，会自动切换到符号执行。类似的，最近提出的Pangolin通过不仅提供fuzzer测试用例，以及一些抽象的符号约束，还有快速样本生成方法，强调了fuzzer结合符号执行的优势；利用这些，fuzzer能够生成可以有很大概率解决由符号执行生成的路径约束的输入。
我们认为更加精细的符号执行和fuzzer的组合可以很大程度上提升混合fuzzing的性能
总结

我们提出了SYMQEMU，一种基于编译的，针对二进制文件的符号执行引擎。我们的评价展示了SYMQEMU性能优于最先进的符号执行引擎并且可以在某些方面与基于源代码的符号执行技术相匹配。而且SYMQEMU非常方便的向其他架构进行迁移，只需要几行代码即可。

【带你搞懂符号执行的前世今生与最近技术】