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

本篇文章收录于2021年网络安全顶会NDSS，介绍了最新的符号执行技术，并且清晰地比较了当前流行的各种符号执行的引擎的优劣势，可以比较系统的了解符号执行技术的相关知识
title ={{SymQEMU}: Compilation-based symbolic execution for binaries},author ={Poeplau, Sebastian and Francillon, AurÃ©lien},booktitle =.NETwork and Distributed System Security Symposium},year =2021,organization = {Network & Distributed System Security Symposium},month ={February},affiliations = {Eurecom, Code Intelligence},extralink ={Details: tools/symbolic_execution/symqemu.html}download_address = https://www.ndss-symposium.org/wp-content/uploads/2021-118-paper.pdf`
摘要

符号执行技术是针对软件分析和bug检测的强力技术，基于编译的符号执行技术是最近提出的一种方法，当对象源代码可以得到时可以提升符号执行的性能。本文提出了一种新的基于编译的，针对二进制文件的符号执行技术。此系统名为symqemu，在qemu基础之上开发，在将target程序转换为host架构的机器码之前修改其IR，这使得symqemu能够将编译符号执行引擎的能力应用于二进制文件，并且在维持架构独立性的同时能够获得性能上的提升。
本文提出了这个方法以及其实现，我们利用统计学方法证明了他比最先进的符号执行引擎s2e以及qsym，在某些benchmarks上，他甚至由于针对源码带分析的symcc 。并且利用symqemu在经过多重测试的library上发现了一个位置漏洞，证明了他在实际软件中的可用性。

介绍

符号执行技术近年来大力发展，一种有效但是代价大的技术，其经常与fuzzing技术混合，并成为混合fuzzing，fuzzing用来探索容易到达的路径，而符号执行用来探索不易到达的路径。
针对符号执行技术的重要特征之一就是其是否需要提供源代码进行分析，而真实世界中的大多数程序(由于某些原因)是不提供源代码的。
所以binary-only的符号执行技术被迫切需要，但是面临一个两难的困境，到底是选择性能的提升还是架构的独立性呢？比如，QSYM针对binary有很高的性能，但是其仅限于x86处理器的指令集。它不仅仅造成了系统架构依赖性，并且由于现在处理器指令的庞大提升了其复杂性。SE则是可以被广泛的应用但是性能较差，S2E可以分析多架构代码以及内核代码。然而他这么做的代价是针对target程序的多种翻译的最终表示，导致了复杂性升高以及影响性能。
在本文中，我们提出了一个方法（a）独立于被测试的程序的target架构（b）实现复杂度低（c）具有高性能。symqemu的关键是qemu的cpu 仿真可以同于轻量级的符号执行机制：不是像s2e中使用中的那种计算复杂度高的将target程序向IR的转换方式，我们hook qemu中的二进制转换机制为了将符号处理直接编译到机器码中。这样使得在性能优于最先进符号执行系统的同时可以保持加够独立性。目前，我们针对于linux用户程序(ELF binaries)，但我们可以将其拓展到任何qemu支持的架构中取，同时我们将symqemu开源来加速未来相关领域的研究。
将符号处理编译到target程序中同样是symcc的核心工作，其性能优于其他符号执行引擎，但是symcc只针对于有源码的程序。symqemu性能优于se2以及qsym，并且相比于基于源代码的symcc性能来说，某些情况也是可以比较。
本文工作主要有一下贡献：

分析了当前最先进的binary-only的符号执行引擎并且明确了其设计中的优势和劣势。
提出了一个方法，融合了其他工具的优势，避免了其他工具的缺点，核心idea是应用基于编译的符号执行技术到binary上，我们工具的源代码开源。
进行了详细的评价试验，并且实验数据以及实验脚本开源。

背景

符号执行符号执行的目的是在目标程序的执行过程中跟踪中间值是如何计算的，每一个中间值都可以表示为程序输入的一个公式。在任何点，系统都会使用这个公式查看这个点是否可达，这个指针是否为空等。如果答案是确定的，那么符号执行引擎将会提供测试用例，一个新的输入例子来触发对应的行为。所以符号执行可以被方便的用来探测程序路径以及触发bug 。
为了跟踪程序的计算过程，符号执行系统必须对程序指令集有一个深入的理解，许多实现都是通过将程序翻译为IR，比如LLVM和VEX 。IR随后被符号化执行，因为执行器只需要处理IR(通常由少量的指令集构成)，所以实现相对比较简单。<font color=red>并且在之前的工作中我们发现，在对进行测试的程序的高级表示的查询较低级指令的表示的查询更加容易解决。</font>