SymQEMU:基于编译的二进制符号执行

2021-01-20 20:01:17

美国加利福尼亚州圣地亚哥,网络和分布式系统研讨会(NDSS 2021)的议事录符号执行是一种用于软件分析和错误检测的强大技术。基于编译的符号执行是最近提出的一种形式,它已经显示出可以在源代码可用时显着提高符号执行的性能。我们展示了一种新颖的技术,可实现基于编译的二进制符号执行(即无需源代码)。我们的系统SymQEMU建立在QEMU之上,在将目标程序转换为主机体系结构之前对其进行了修改。这使SymQEMU可以将符号执行功能编译为二进制文件并在保持体系结构独立性的同时获得相关的性能优势。

我们介绍了我们的方法和实现,并表明它在统计意义上优于最新的二进制符号执行器S2E和QSYM。在某些基准上,它甚至比基于源的SymCC拥有更好的性能。此外,我们的工具在经过充分测试的libarchive库中发现了一个以前未知的漏洞,证明了它在测试实际软件中的实用性。

SymQEMU是用于二进制文件的快速符号执行引擎。在此页面上,我们提供其源代码,本文中描述的实验的原始结果,以及有关如何自己复制这些实验的说明。

在本文中,我们描述了三组实验:首先使用Google FuzzBench对SymQEMU进行基准测试,然后在实际软件中运行它,最后在对固定路径进行一致执行期间进行基准比较。本部分介绍了如何复制实验,并提供了指向我们结果的链接。

我们将很快分享我们的集成脚本;正在清理它们,以从新的公共存储库中获取SymQEMU及其依赖项。

为了分析实际软件,我们使用了与SymCC评估中相同的设置。 SymQEMU,QSYM和S2E的二进制文件是纯构建,没有任何工具。通过使用/ path / to / symqemu-x86_64为目标命令添加前缀,可以通过SymCC的模糊帮助程序运行SymQEMU。对于S2E分析,我们创建了一个默认项目,然后启用FunctionModels插件并在TestCaseGenerator插件中激活了选项generateOnStateFork。在分析结束时,使用与混合模糊器相同的AFL插入二进制文件,通过afl-showmap评估覆盖率。

OpenJPEG(我们的结果),libarchive(我们的结果),tcpdump(我们的结果):请在我们的SymCC页面上找到详细信息。

在对上述实际软件进行分析之后,我们为每个开源目标随机收集了1,000个生成的测试用例。 我们对每个输入运行了SymQEMU,QSYM和SymCC,并根据QSYM后端的日志记录输出分别记录了执行和SMT解决所花费的时间。 这项工作部分由DAPCODS / IOTics ANR 2016项目(ANR-16-CE25-0015)和部分由国防高级研究计划局(DARPA)支持,协议号为FA875019C0003。 如果有任何不清楚的地方或需要更多信息,请随时与我们联系。