【论文阅读】符号执行研究综述

【论文阅读】符号执行研究综述

芦笑瑜 战略支援部队信息工程大学 2022
一篇综述文章

符号执行：
基本原理在于通过抽象符号来代替具体的程序输入变量，并在执行过程中动态地维护不同路径下的程序状态。这些状态包括用于表示变量状态的符号表达式以及与路径相关的约束条件。同时，在这一过程中也会动态地维护不同路径下的变量状态及其相关约束条件。此外，在这一过程中还会动态地维护不同路径下的变量状态及其相关约束条件，并根据不同的运行路径不断更新相应的信息以确保准确性与完整性。这种技术广泛应用于软件测试与漏洞挖掘领域中以提高代码质量与安全性分析效率

符号执行模式：
经典模式
在符号执行过程中，并不需要提供具体的程序代码。其基本流程如下所述：首先，在编译阶段将程序的预期输入转化为特定的符号表示；然后，在运行阶段从目标程序的角度出发进行符号模拟分析；具体而言，在每条指令被执行时（即每次循环迭代一次），都会相应地更新当前的状态信息以反映操作结果。

混合模式
符号执行的结果受特定输入实例的影响,该混合模式整合了程序的具体运行和基于符号的分析方法。该混合模式通过将程序的具体运行与基于符号的方法相结合,仅在涉及符号的部分展开模拟分析,其余部分则依据常规流程处理即可,从而能够有效规避冗余且低效的symbolic simulation过程。

启动生成测试流程

选择执行模式
在开始之前,确定目标程序的具体执行区域和符号执行区域;同时,支持用户指定需要进行符号化搜索的代码区域,并根据具体输入样例进行相应的操作.随后向目标程序施加合法输入并完成运行流程.

主要挑战
路径爆炸
约束求解困难
符号模拟低效

先进符号执行系统
S2E、 Angr、 QSYM、 SymCC、 SymQEMU

基于符号执行机制的解释性编译器
思想：在符号分析过程中,动态地将机器码指令转化为等效的中间表示,设置动态插桩点,并逐条解析指令以实现深入分析。
代表：S2E、Angr

核心理念：通过在运行时进行多次编译和执行的方式，在保证程序正确性的前提下实现了代码的一次性编写与高效运行的统一目标；该方法的主要优势在于能够有效消除冗余处理步骤，并显著提高运行效率；代表包括 QSYM、SymCC 和 SymQEMU。

将其转换为中间层次的表示形式；将其转换为机器层次的编码方式；通过动态二进制插桩机制实现编码的直接生成

符号执行与模糊测试融合
混合式模糊测试(Hybrid Fuzzing)是一种促进符号执行与模糊测试实例协同工作的技术方案,通过优势互补实现整体效能提升。
QSYM 和 SymCC 均支持使用著名模糊测试工具AFL开展混合式模糊测试工作。

基于模糊逻辑的仿真实验：一种用于符号执行系统的模糊性检验方法。Jingxuan He

【完】