多路复用符号执行：一次求解探索多条路径

一、 研究作者、机构及发表信息

本研究的主要作者为张宇峰（Yufeng Zhang，湖南大学）和陈振邦（Zhenbang Chen，国防科技大学），二人为共同第一作者。其他作者包括帅子奇（国防科技大学）、张天齐（国防科技大学）、李肯立（湖南大学）和王戟（国防科技大学），其中陈振邦和王戟为通讯作者。该研究以论文《Multiplex Symbolic Execution: Exploring Multiple Paths by Solving Once》的形式发表于第35届IEEE/ACM自动化软件工程国际会议（ASE ‘20）的会议录中。会议于2020年12月21日至25日在线上举行（地点：澳大利亚，虚拟会场）。该论文的正式出版时间为2021年1月27日，被收录于ACM的会议录中，并获得由湖南大学和国防科技大学提供的开放获取支持。

二、 学术背景

本研究隶属于软件工程领域中的程序分析与软件验证方向，具体聚焦于符号执行技术。符号执行是一种精确的程序分析技术，通过用符号值替代具体输入来模拟程序执行，生成约束并求解，已被广泛应用于自动化软件测试、缺陷发现和程序修复等领域。

然而，符号执行面临两大关键的可扩展性挑战： 1. 路径爆炸：程序中的分支语句数量呈指数级增长，导致需要探索的路径空间极为庞大。 2. 约束求解：符号执行过程中生成的路径条件需要由底层的约束求解器进行可满足性检查，而约束求解本身是一个计算复杂度高的问题。

作者指出，在传统符号执行框架中存在“双重搜索”的冗余问题。符号执行引擎本身采用一种搜索策略（如深度优先、广度优先）在程序的路径空间中探索；同时，对于每条待探索路径的条件，它调用底层的约束求解器，求解器内部又在路径条件的解空间中进行另一轮搜索。本质上，这两次搜索的目标都是探索程序的输入空间，但它们是分离且重复的。这种冗余极大地限制了符号执行应用于大规模实际程序的能力。

本研究旨在解决上述问题。其核心目标是统一这双重搜索过程，通过更高效地利用约束求解过程来直接指导路径探索，从而提升符号执行的整体可扩展性。为此，作者提出了名为多路复用符号执行（Multiplex Symbolic Execution, MUSE） 的新方法。

三、 研究详细流程与方法

MUSE的核心思想是打破传统上将约束求解器视为“黑盒”的做法，以“白盒”方式利用求解器在搜索过程中的中间结果，在单次求解过程中生成多个可用于探索不同路径的测试输入。这些中间结果被称为部分解，它满足路径条件中的一个子集约束，因此能够触发当前路径上的其他“岔路”分支。MUSE将约束求解器的内部搜索过程映射到程序的路径探索上，实现“一次求解，探索多路”。

为了验证这一思想的普适性和有效性，研究团队从方法设计、实现到评估进行了完整的流程：

1. MUSE框架设计与算法整合

   • 核心算法：研究首先提出了与动态符号执行（DSE）框架集成的MUSE算法（算法1）。该算法在执行符号测试时，对于选定的待探索分支，生成其路径条件φ，然后调用一个经过扩展的、能返回部分解的约束求解器。
   • 数据流：求解器返回一个三元组（结果，完整解，部分解集合）。无论最终结果是可满足还是不可满足，只要产生了部分解，这些部分解都会被保存为新的测试输入，加入到待执行队列中。这确保了昂贵的约束求解计算不会因路径不可达而被浪费，并能从单次求解中挖掘出多个路径探索机会。
   • 关键要求：该框架的关键在于底层约束求解器必须能够生成部分解。

2. 在多种约束求解算法中实例化MUSE 研究团队选择了三种在符号执行中常用的、具有不同代表性的约束求解算法，并详细阐述了如何在其中获取部分解：

   • 基于单纯形法的整数线性算术求解：针对线性整数约束（QF_LIA），主流求解器（如Z3）使用单纯形算法。作者修改了Z3，在单纯形算法的每次“旋转”操作前记录当前变量赋值作为部分解。单纯形算法通过不断调整变量赋值使其满足更多约束，这个迭代过程自然产生了一系列满足不同约束子集的部分解（算法2）。
   • 基于抽象精化的数组与位向量理论求解：针对涉及数组和位操作的约束（QF_ABV），主流求解器（如STP）采用抽象-精化循环。算法首先对包含数组理论的公式进行抽象（移除一些数组公理约束），得到一个较易求解的抽象公式。然后迭代求解抽象公式，并用得到的解去验证原始公式。如果不满足，则精化抽象公式，加入更多约束，重复此过程。作者修改了STP，将在每次抽象-精化循环迭代中得到的、满足抽象公式但不一定满足原始公式的解，记录为部分解（算法3）。这些解可能满足原始公式中除部分数组约束外的所有其他约束。
   • 基于数学优化的浮点数求解：针对浮点算术约束，现代求解方法（如XSat）常将约束求解问题转化为寻找目标函数全局最小值的最优化问题。作者自行实现了一个基于模拟退火算法的浮点数求解器。在模拟退火的蒙特卡洛采样步骤中，算法会访问解空间中的许多点（赋值）。作者将这些采样过程中访问的点，特别是局部最优点，提取为部分解。这些点可能使目标函数值（即不满足程度）降低，对应着满足越来越多的子约束。

3. 系统实现 为了进行广泛评估，研究团队基于两种主流的符号执行引擎和相应的求解器实现了MUSE的原型系统：

   • 针对C程序：在基于Klee的DSE引擎上实现，集成了支持部分解的修改版STP求解器。
   • 针对Java程序：在基于符号路径查找器（SPF）的DSE引擎上实现，集成了支持部分解的修改版Z3（用于QF_LIA）以及自行开发的优化浮点求解器。

4. 实验评估设计与流程 研究团队设计了三个独立的实验，分别对应上述三种约束求解方法，以评估MUSE的有效性和效率。

   • 实验一（QF_LIA）：使用Java符号执行引擎和修改版Z3。测试对象为11个真实世界的开源Java文件解析库（如图片、音频、字节码解析器）。实验将文件中字节符号化，比较了深度优先搜索、广度优先搜索以及它们分别结合MUSE（DFS+p, BFS+p）共四种配置在15分钟内的表现，主要指标为生成的测试用例数和覆盖的新指令数。
   • 实验二（QF_ABV）：使用C符号执行引擎和修改版STP。测试对象为13个GNU科学库（GSL）中的数值计算函数，涉及大量浮点和数组操作（浮点运算通过整数模拟实现）。实验比较了MUSE结合DFS/BFS，与Klee内置的几种默认搜索策略（随机覆盖新、随机状态、DFS、BFS）在15分钟内的LLVM指令覆盖率。
   • 实验三（浮点求解）：使用Java符号执行引擎和自研的优化求解器。测试对象为10个来自线性代数库（如la4j, colt）的复杂浮点计算程序。实验同样比较了MUSE结合DFS/BFS与基础DFS/BFS在15分钟内的表现。
   • 分析工作流：对所有实验，均记录随时间变化的覆盖率增长曲线、最终覆盖率、生成的测试用例数以及每次求解平均产生的部分解数量，并计算了为达到相同覆盖率MUSE相对于基线方法的加速比。

四、 主要结果

实验结果有力地支持了MUSE方法的有效性和高效性。

1. 实验一（QF_LIA）结果：

   • 有效性：在11个程序上，无论是DFS+p还是BFS+p，其平均生成测试用例数（889 vs 108；2536 vs 1139）和平均覆盖新指令数（127 vs 36；202 vs 117）均显著高于对应的基线策略（DFS, BFS）。
   • 效率与加速比：从覆盖趋势图看，MUSE配置能够更快地达到更高的覆盖率。量化来看，DFS+p仅需14.4秒即可覆盖DFS在625.6秒时达到的最大新指令数（约400条），加速比超过43倍。BFS+p达到BFS上限覆盖率（1296条指令）所需时间也远少于BFS，加速比至少为12.9倍。

2. 实验二（QF_ABV）结果：

   • 有效性：在13个GSL函数上，BFS+p获得了最高的平均覆盖率（90.4%），显著优于Klee的所有默认策略（平均覆盖率在54.8%到69.4%之间）。DFS+p也取得了优于大多数基线策略的覆盖率（78.8%）。
   • 效率与加速比：覆盖率趋势图显示，MUSE配置（特别是BFS+p）在整个时间窗口内都保持领先，并且能够以数量级的速度达到DFS和BFS策略的覆盖率上限。

3. 实验三（浮点求解）结果：

   • 有效性：MUSE再次在覆盖新指令数和生成测试数上全面超越基线。值得注意的是，由于DFS倾向于探索更长、约束更复杂的路径，其基线性能很差（部分程序甚至无法扩展执行树），而MUSE对DFS的提升尤为显著。
   • 效率与加速比：趋势图显示MUSE配置能持续覆盖更多指令。DFS+p仅用7.8秒就覆盖了DFS在773.1秒达到的最大指令数（约615条），加速比高达99倍。BFS+p也获得了至少4.6倍的加速比。

4. 关于部分解的统计结果：

   • 数据显示，在单次约束求解过程中可以产生大量的部分解。例如，在QF_LIA实验中，一次求解平均可产生数百个部分解；在QF_ABV实验中，对于复杂函数，一次求解也可能产生数百个部分解。
   • 通常，在DFS策略下（路径条件更长更复杂）产生的部分解数量多于BFS策略，因为求解器需要更多尝试才能找到最终解，从而提供了更多中间状态。

五、 结论与价值

本研究提出并实现了多路复用符号执行（MUSE），这是首次尝试统一符号执行中双重搜索冗余的开创性工作。其核心贡献在于： * 科学价值：揭示了约束求解过程与路径探索过程的内在统一性，提出了“部分解”这一关键概念，并将其成功应用于多种不同类型的约束求解算法中（线性算术、数组理论、浮点优化），证明了该思想的普适性。 * 应用价值：通过利用约束求解的中间结果，MUSE能够显著提升符号执行的效率。大量实验表明，MUSE可以在多种编程语言（C、Java）、多种程序类型（解析库、数值计算、线性代数）和多种约束理论下，实现一到两个数量级的加速比，以达到相同的代码覆盖率。这为将符号执行更有效地应用于大规模、复杂的现实软件系统提供了强有力的新工具。

六、 研究亮点

1. 新颖的核心思想：首次提出并系统性地利用约束求解过程中的“部分解”来直接驱动符号执行的路径探索，打破了传统黑盒使用求解器的模式，是解决符号执行双重搜索冗余问题的创新思路。
2. 方法的普适性与系统性验证：不仅提出了框架，还成功在三种截然不同的主流约束求解算法（单纯形法、抽象精化、数学优化）中实现了部分解的提取，并在两个主流符号执行引擎上构建了原型系统，进行了全面、跨语言、跨领域的实验验证。
3. 显著的性能提升：实验结果展示了数量级的性能加速，且这种提升在不同场景下具有一致性和鲁棒性，证明了MUSE强大的实用潜力。
4. 对未来的启发性：作者在讨论中指出，MUSE是迈向统一符号执行搜索过程的第一步。他们提出了未来可能的方向，如将部分解与轻量级具体执行结合以避免冗余符号计算、在更多理论求解器中实现MUSE等，为该领域的后续研究开辟了新的路径。

七、 其他有价值内容

论文还简要讨论了部分解在其他约束求解算法中普遍存在的可能性，例如： * CDCL框架的SAT求解器：其决策-回溯循环中的部分赋值天然就是部分解。 * DPLL(T)框架的SMT求解器：可以结合其命题骨架求解和理论求解中的部分解。 * 相等逻辑与未解释函数的同余闭包算法：在构建等价类的过程中可以构造部分解。 * 基于覆盖引导模糊测试的浮点求解器（如JFS）：其生成的非最终测试用例也可视为部分解。 这进一步论证了MUSE所基于的“部分解”概念具有广泛的理论基础和应用前景，并非局限于论文中实现的几种算法。