《符号执行研究综述》论文阅读
了解《符号执行研究综述》这篇论文的内容非常有益。
符号执行被视为一种关键的程序分析技术。
它不仅有助于提高程序测试的有效性，
而且能够用于生成具有高覆盖率的测试案例。
通过这种方法，
我们可以更好地揭示潜在的软件缺陷。
定义
在软件工程领域中，符号执行被视为一种关键的形式化分析工具。通过将程序中的变量用抽象符号表示，在此基础上进行运算以求得结果。计算结果则以输入变量对应的函数形式呈现。基于对程序语义的理解，在其所有可能的行为轨迹中展开搜索。
历史
- 1975年,King首次提出了符号执行的思想,并将其应用到了程序分析领域。
- 在短暂的研究热潮过后,符号执行研究逐渐陷入停滞。
- 在过去的几十年间,传统 symbolice xecution经历了逐步演变,发展出了动态 symbolic xecution和选择性 symbolic xecution等阶段.
- 动态 symbolic xecution包含两部分:(1)混合测试;(2)生成测试.
- 其主要优点在于尽可能少的测试用例集能够达到高覆盖率的同时,并能够挖掘出复杂软件中的深层错误.
- 其主要挑战包括路径爆炸问题、约束求解困难以及内存建模等问题.
各类符号执行介绍
经典符合执行
- 经典符号执行的本质在于通过引入符号值取代具体数值作为程序输入参数，并以符号表达式精确表征与这些符号值相关联的变量取值状态。
- 经典符号执行并非实际运行程序,而是建立在解析引擎基础之上,利用符号值模拟程序运行过程。
- 经典 符号 执行 被 视 为 一种 静 态 的 符 号 执行 方法。
- 在 理 论 上 ,经 典 符 号 执行 方 法 能 够 实 现 对 程 序 所 有 执 行 路 径 的 全 部 模 拟 ,并 可 以 根 据 不 同 的 执 行 路 径 有 机 地 产 生 对 应 的 测试 样 本 集。
动态符号执行
- 动态符号执行融合运用了具体执行与符号执行的方法论,这种整合综合运用各自的优势特点,并衍生出混合式 execute（concolic execution）以及生成测试两大类别的 execute 技术。
- 混合式 execute 技术是由 Godefroid 与其合著者 Sen 等人于 2005 年首次提出的. Sen 对该技术的理论基础进行了深入阐述,并对近十年来的技术和研究进展进行了系统性的总结.
- 基于 Cadar 等人在 2006 年提出的 execute 测试概念,在 EXE 工具中实现了这一核心思想；同时在 KLEE 工具中也得到了相应的应用与拓展.
混合测试
混合执行思想：针对特定输入运行程序，在运行过程中运用插桩手段捕获路径相关限制条件；按照一定顺序搜索程序路径；通过调用约束求解器对上一阶段收集的所有限制条件进行运算；从而生成下一阶段的测试案例；在完成当前阶段测试后依据预定策略从候选分支中选取某一判断点施加反向限制条件生成新的限制集合；再次调用约束求解器运算以确定下一个阶段的测试案例；如此循环往复以避免重复运行相同的执行路径最终实现用最少数量的测试集获取尽可能高的覆盖效果
执行生成测试
- 混合式执行中，在处理与符号变量无关的部分时采用具体执行方式；而对于涉及符号变量的部分则实施符号分析以引导测试流程。
- 其核心理念在于利用程序代码自动生成复杂度高的测试案例；在通过符号输入运行程序时，在分支节点记录下无效路径的状态信息，并继续处理仍有效的分支。
- 相较于传统混合式测试方法而言，该方法的优势在于能够系统化地获取所有路径信息及其对应的测试案例；然而其主要缺点在于内存占用较高。
- 为了解决内存占用问题的一种有效途径是采用多线程技术替代传统的分支存储方式。
选择性符号执行
选择性符号执行专注于在特定区域内进行精确的符号分析，在该区域内它会系统地识别和跟踪所有相关的变量和操作；而在区域外则采用直接运行的方式处理所有操作。
主要挑战和解决方法
路径爆炸
路径爆炸问题构成符号执行在现实程序分析中应用的主要障碍。针对上述问题的解决途径主要包括以下几种思路：
- 基于启发式策略的方法对程序路径空间展开探索。
- 对于冗余探索路径进行去除。
- 通过现有的回归测试数据集来设定任务执行的优先级顺序。
- 在约束条件下的符号执行分析。
约束求解
符号执行作为程序分析的核心技术之一，在提升代码理解和验证效率方面发挥着重要作用；其效率往往受到约束求解性能的直接影响，并主要依赖于基于可满足性模理论（SMT）的技术框架的支持。该方法强调对优化思想的深入应用：通过系统化的方法提升算法效率和问题解决能力
- 无关约束消除。
- 缓存求解策略。
- 懒约束求解策略。
主流符号执行工具
EXE 和 KLEE 是基于符号执行分析源代码的工具，并均由斯坦福大学的研究团队开发。
KLEE 具备显著的效果，在用户级别能够达到 90% 的测试覆盖率，在复杂软件系统中则能通过交叉验证机制发现隐藏的程序缺陷。
- DART,CUTE和jCUTE。
- angr。二进制分析工具。
结论
- 符号执行的主要发展方向之一在于应对路径空间启发式搜索、约束求解等技术难题，并结合并行处理问题以及内存建模和执行环境仿真等复杂挑战。
- 另一个主要方向是与Fuzzing技术协同运用，以提升程序漏洞探测的效果。