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

文章插图

最近提出的符号执行工具，SYMCC，同样是本文作者之前的工作，基于源代码的，不支持分析二进制文件。SYMQEMU的灵感来自于SYMCC，所以简要概括一下他的设计。
我们在设计SYMCC时观察到，目前大多数符号执行系统是解释器。然而我们却提出一个基于编译的方法，并且展示了他能够提升执行性能以及系统实际探索能力。SYMCC在编译器内进行hook，并且在target代码内进行插装，并且注入实施支持库的调用。因此符号执行成为了被编译文件的一部分。并且分析代码可以进行优化，并且插装代码并不会在每次执行时进行重复。
SYMCC基于编译的方式需要编译器，所以他只能在被测试程序源代码可用时发挥作用。尽管如此，我们认为这个方式是足够有前途，所以一直寻找一种方式将其应用到binary-only的方面之中，本文的主要工作就是说明基于编译的符号执行系统是如何在二进制文件上高效的工作。
SYMQEMU现在提出针对binry-only设计实现的SYMQEMU 。他的灵感来自于之前的工作并结合了如今最先进的符号执行系统的技术。
design系统两个主要目标：

实现高效能，以致于实际软件。
合理的架构独立性，比如将其迁移到新的处理器架构不需要做过多工作。

基于之前的调查，我们发现流行的最先进的符号执行系统实现了如下两个目标中的一个，但并非全部：angr和s2e是架构灵活的但是性能差；QSYM在性能上比较高但是其只针对x86架构。
如今针对架构独立的解决方案是将被测程序翻译为IR，这样如果想要支持一个新的架构，只有翻译器需要移植，理想情况下，我们选择一种中间语言，其已经存在支持多种架构的相关翻译器。以中间语言灵活地表示程序是一种著名的，已经成功的应用于许多其他领域的技术，比如编译器设计以及静态代码分析。我们也将这种技术合并到我们的设计中来。
当将程序翻译为中间语言获得便利的同时，我们同样需要了解这种方式对于性能的影响：将binary-only程序静态翻译是具有挑战性的，因为反汇编器可能是不可靠的，尤其是存在间接跳转的情况下，并且在分析过程中运行时进行翻译会提升功耗。我们认为这是s2e性能劣于QSYM的主要原因。我们的目标就是找到一种翻译系统同时保持性能优越。
首先，我们主要到s2e以及angr都收到了非重要问题的影响，并且这些问题都是可以通过工程方面的工作解决的：

S2E将被测试程序翻译了两次，然而如果符号执行过程是在第一次中间表示上实现的话，第二次翻译过程其实是可以避免的。
angr的性能受到python实现影响，将其核心代码移植到一种更快速的语言中会显著提升速度。

然而我们的贡献并不仅仅是找出并且避免上述两个问题，我们还观测到：s2e以及angr，以及其他所有的binaty-only的符号执行器，都解释执行被测试程序的中间表示，解释是设计的核心部分。我们推测，将目标程序编译为插桩版本将会带来很高的性能上的提升。虽然SYMCC是基于源代码的，基于编译的符合执行引擎，但是他证明了这一点。
收到上述观测到的启发，我们的设计方法如下：

在运行态将目标程序翻译为IR 。
为符号执行所需的IR插桩。
将IR编译为适合CPU运行分析的机器码并且直接执行。

通过将插桩的目标程序编译为机器码，补偿了在第一阶段将二进制文件翻译为中间代码时的性能损失。CPU执行机器码比解释器运行IR速度快得多，因此我们获得了一个可以与没有翻译的系统的性能相当的系统，同时由于进行了程序翻译可以保持架构的独立性。
implementation

文章插图

我们在qemu的基础之上实现了SYMQEMU，选择qemu的原因是因为他是一个鲁棒性的系统仿真器，并且可以支持许多架构，在他的基础之上进行实现，我们可以实现架构独立性。并且qemu还有另一个特点正好满足我们的需求，他不仅将二进制文件翻译为针对处理器独立的IR，他同时支持将中间语言便已成为host CPU的机器码。qemu的主要优点是他能够将二进制文件翻译为不同host架构的机器代码，并且可以完成全系统仿真，方便于之后拓展支持交叉架构的固件分析。