💻 计算机科学

Directed Symbolic Execution for Path Feasibility Analysis]{Directed Symbolic Execution for Path Feasibility Analysis in Software Security Testing

本文提出了一种定向符号执行方法，该方法通过自动化符号化和循环迭代限制，高效地验证过程间路径的可行性，从而在增强静态安全分析的同时，在显著提高精确度的同时保持了召回率，并在现实世界的基准测试中得到了验证。

原作者： Hovhannes Movsisyan, Hripsime Hovhannisyan, Tigran Avagyan, Hayk Aslanyan

发布于 2026-10-22

📖 1 分钟阅读☕ 轻松阅读

原作者： Hovhannes Movsisyan, Hripsime Hovhannisyan, Tigran Avagyan, Hayk Aslanyan

原始论文采用 CC BY 4.0 许可（https://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

软件安全是一场针对隐藏缺陷的持久战，就像城市规划者试图确保大都市中每一座桥梁和隧道都能抵御地震一样。为了实现这一目标，工程师们使用自动化工具在不实际运行程序的情况下扫描代码，绘制出程序可能采取的每一条路径图。这些被称为控制流图（control flow graphs）的地图极其详尽，展示了程序如何在一条指令跳转到另一条指令之间进行。然而，这些地图往往过于彻底；它们标出了在理论上看起来危险、但在现实世界中物理上无法通行的路径。这造成了大量的虚假警报，迫使人类专家在浪费时间调查这些“机器中的幽灵”。因此，挑战在于构建一个能够快速区分“理论上可行”与“实际上可执行”路径的系统，而不至于迷失在海量的可能性之中。

俄罗斯-亚美尼亚大学的一个研究小组开发出一种新方法来解决这个问题，使用的是一种被称为定向符号执行（directed symbolic execution）的技术。想象一位旅行者试图验证通过复杂城市的某条特定路线是否存在。标准的方法是派出探险家走遍城市的每一条街道以观察它们的去向，这项任务将耗时极长且会让团队不堪重负。相反，研究人员的方法就像是一场导览之旅。它获取安全扫描器报告的一条特定路径，并指挥一名虚拟探险家仅沿着该路径行进，忽略所有不通往目的地的街道。这种“定向”方法使得系统能够在不浪费精力于无关绕路的情况下，检查报告的危险是否真实存在。

这项工作的核心在于系统如何处理“未知”。在真实的软件中，程序经常处理尚未设置的数据，或者调用来自外部库的函数，而这些库的内部代码是隐藏的。传统的探险家在面对这些空白时可能会陷入停滞或放弃。然而，研究人员的系统旨在将这些未知情况视为灵活的变量。如果程序读取了一个尚未填充的内存位置，系统会为其分配一个符号值，从而允许它探索该值可能产生的所有结果。对于外部函数的结果和复杂的指针参数（这些参数作为动态地址，会根据情况指向不同的地方），系统也会进行同样的处理。通过自动用可能性而非具体的猜测来填补这些空白，即使在全貌不可见的情况下，系统也能追踪代码中的路径。

在导航软件时面临的另一个主要障碍是循环（loop），即重复执行的代码段。在实际程序中，一个循环可能会运行几次或数百万次，而在符号分析中，它可能会让探险家陷入无限循环。研究人员引入了一种策略来处理这个问题：设定一个限制，规定系统在强制退出前可以跟随循环多少次。这并非随机的截断；系统会仔细记录这些迭代期间发生的情况，然后跳转到循环自然结束的点。这使得分析能够越过重复部分继续进行，确保工具能够到达其正在调查的路径终点。

为了测试他们的方法，该团队将其应用于真实世界的软件以及一套名为 Juliet suite 的标准测试用例集。他们首先针对从 GNU Coreutils（Linux 操作系统的基础工具集）中提取的路径对系统进行了检查。系统成功验证了其中 95.3% 的真实路径是确实可行的，证明了它能够处理复杂的交织代码。随后，他们将该方法与现有的安全工具 MLH 集成。在此之前，该工具在数千个报告中标记了 666 个虚假警报。应用了这种新的路径可行性分析后，这些虚假警报完全消失了，同时该工具依然能捕捉到之前发现的所有真实漏洞。这意味着在测试的子集中，安全检查的精确度从 56.6% 跃升至 100%，且没有损失发现真实漏洞的能力。

研究人员还将他们的方法与专门设计用于类似任务的工具 KLEEF 进行了对比。在针对另外两个主要安全扫描器（Infer 和 Clang Static Analyzer）生成的报告进行测试时，结果非常悬殊。KLEEF 在验证大多数真实阳性报告方面表现挣扎，导致其性能得分大幅下降。相比之下，新方法保持或略微提升了原始扫描器的性能。它成功验证了 Infer 工具报告的所有真实漏洞，并处理了绝大部分 Clang 报告，证明了其处理工业级代码的鲁棒性。

研究结果表明，这种定向方法为清理软件安全测试中的噪声提供了一种切实可行的方式。通过专注于重要的路径并自动处理内存和外部函数的复杂性，该方法过滤掉了浪费人类时间的无效场景。虽然该系统通过限制循环迭代做出了权衡，但结果显示，这并未以丢失真实危险为代价。这项工作为提高自动化安全工具的可靠性提供了清晰的路径，确保当发出警告时，那是一个值得调查的真实威胁。

技术摘要：用于软件安全测试中路径可行性分析的有向符号执行

问题陈述

静态分析是一种通过分析代码而不执行代码来识别软件漏洞的可扩展技术。然而，静态分析器的一个显著局限性是会产生误报（false-positive）。这些报告通常源于对不可行控制流路径的分析——这些路径在进程间控制流图（ICFG）中看起来是有效的，但由于语义约束，在运行时无法执行。

虽然符号执行在理论上可以通过构建和求解路径约束来确定此类路径的可行性，但其在实际应用中受到“路径爆炸”问题的阻碍。标准的符号执行尝试探索所有可达路径，导致指数级的资源消耗。此外，现有工具通常缺乏自动化能力，难以处理现实世界的复杂情况，如未初始化内存、外部函数调用、符号指针以及循环，而无需人工干预或特定的插桩。

方法论

作者提出了一种专门用于验证预定义 ICFG 路径可行性的有向符号执行方法。与尝试探索整个状态空间的传统符号执行不同，该方法将执行严格引导至目标路径，从而剪枝掉与验证目标无关的分支。

核心算法

该算法运行在一组允许的基本块集合（ $S_{allowed}$ ）和一组必须经过的里程碑集合（ $S_{req}$ ）之上，以到达目标块（ $B_{target}$ ）。

定向剪枝： 在每个分支点，只有当后继块属于 $S_{allowed}$ 时，引擎才会进行探索。这消除了对无关程序区域的探索。
循环绑定： 为了防止循环中的非终止问题，该方法限制了循环迭代次数（ $C_{max}$ ）。如果循环超过此界限，引擎会强制符号状态通过可用的退出边退出循环，仅对循环期间写入的内存位置进行符号化。这使得分析能够继续执行循环之后的代码，而不是直接终止。
验证： 如果符号执行在访问了所有 $S_{req}$ 中的块的同时保持在 $S_{allowed}$ 内并到达了 $B_{target}$ ，则认为该路径是可行的。

自动符号化策略

为了实现无需手动配置的全自动分析，论文引入了几种符号化方法：

入口点参数： 无论该函数是否为程序的 main 入口点，其所有参数都会被符号化。
未初始化内存： 未初始化的局部变量和动态分配的内存区域被视为具有未约束值的符号对象，确保依赖于未定义行为的路径不会被过早丢弃。
外部函数：
- 返回值： 外部函数（如动态库）的返回值被符号化。
- 指针参数： 外部调用中非常量指针参数所引用的内存区域会被重新符号化，以考虑潜在的副作用。
- 特殊全局变量： 对 errno（在外部调用后重新符号化）和 environ（建模为具有固定长度的固定符号变量集合，以避免环境操作函数中的非终止问题）进行了特殊处理。
函数指针与虚函数： 系统通过匹配签名来解析符号函数指针；对于虚函数，通过分析虚表来识别所有可能的派生类重写，并为每个候选对象分叉状态。

内存模型

论文提出了一个针对大小未知的符号指针（例如传递给函数的数组）的灵活内存模型。该模型并非分配固定大小的数组，而是在第一次解引用时按需创建内存对象。

按需分配： 仅当访问符号指针时，才会创建一个内存对象。
别名解析： 当解引用指针时，引擎会检查是否存在具有相同偏移量的现有内存对象。如果可能存在别名，引擎会分叉符号状态，以探索指针引用现有对象与引用一个全新的、不同的内存位置这两种场景。这支持了对复杂数据结构（如链表和树）的分析，而无需预定义大小约束。

核心贡献

有向符号执行算法： 一种通过限制探索范围来确定特定 ICFG 路径可行性的方法。
全自动符号化： 处理入口点参数、未初始化变量、外部函数返回值及指针参数的策略，无需用户干预。
符号内存建模： 支持符号指针和别名场景的内存模型，能够分析任意数据结构。
循环绑定策略： 一种限制循环迭代次数的算法，以确保终止并允许符号执行继续执行后续代码块。
实证评估： 使用真实世界软件（GNU Coreutils）和 NIST Juliet 测试套件进行的全面评估。

实验结果

该方法作为 KLEE 符号执行引擎（v3.1）的一个扩展进行实现，并在三个场景下进行了评估：

在真实路径上的可扩展性：
- 在从 GNU Coreutils 提取的 234 条 ICFG 路径（范围从 22 到 1,218 个基本块）上进行了测试。
- 实现了 95.3% 的召回率，成功验证了 223 条路径。
- 49 条路径需要循环绑定策略（阈值设为 3），而 174 条路径在无需该策略的情况下即可验证。
- 执行时间从简单路径的不到一分钟到涉及重度符号指针算术的复杂路径的约 30 分钟不等。
与 MLH 静态分析器的集成：
- 在 Juliet 测试套件（CWE-401：内存泄漏子集）上进行了评估。
- 集成使 MLH 工具的精度从 56.6% 提升至 100%，通过过滤掉误报实现了这一点。
- 召回率保持在 100%，证实没有丢弃任何真实的漏洞。
与 KLEEF 的比较：
- 使用 Infer 和 Clang 静态分析器（CSA）在 Juliet 子集（CWE-415 和 CWE-416）上的报告与 KLEEF（一种用于工业代码的 KLEE 衍生版本）进行了对比。
- KLEEF 表现： 性能显著下降。对于 Infer，KLEEF 将 F1 分数从 1.0 降低到了 0.0（将所有真阳性分类为不可行或导致崩溃）。对于 CSA，F1 分数从 0.766 降至 0.074。
- 本研究方法表现： 保持了 Infer 的基准 F1 分数（1.0），并略微提升了 CSA 的表现（0.767）。该方法成功验证了所有真阳性，并正确识别了误报报告中的可行路径（这些报告可以通过进一步的检查进行过滤）。

意义与主张

论文声称，所提出的方法有效地弥合了符号执行的高精度与实际软件测试所需的扩展性之间的差距。通过定向执行和自动化符号化，该方法成功地从静态分析报告中过滤掉不可行的路径，从而在不牺牲检测真实漏洞能力的前提下消除了误报。

作者承认，循环绑定策略在完备性与可扩展性之间引入了权衡，可能会允许探索某些逻辑上不可达的路径。然而，他们认为在验证静态分析报告的语境下，这是一个可以接受的权衡，因为此时的首要任务是确保目标缺陷位置的可达性，而非对所有循环行为进行穷举探索。该方法被呈现为一种增强现有静态分析工具可靠性的鲁棒后处理步骤。