💻 computer science

Quantitative Symbolic Patch Impact Analysis

本文介绍了定量部分等价分析，这是一种符号化方法，用于量化原始程序与补丁程序之间的行为差异，以评估补丁影响并识别导致分歧的具体输入条件，并在真实世界的 CVE 补丁和基准数据集上验证了其有效性。

原作者： Laboni Sarker, Abdus Satter, Tevfik Bultan

发布于 2026-05-15

📖 1 分钟阅读☕ 轻松阅读

原作者： Laboni Sarker, Abdus Satter, Tevfik Bultan

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

想象一下，你手头有两份巧克力蛋糕的食谱。原始食谱存在一个缺陷：如果面粉放得太多，蛋糕就会塌陷。一位开发者通过添加一条规则来修复这个问题：“如果你使用的面粉超过 5 杯，就停止烘焙。”

现在，假设你想知道：这个修复究竟在多大程度上改变了蛋糕的制作方式？

旧方法（传统检查）： 传统的计算机检查只会说：“这两份食谱不同。”它就此止步。它不会告诉你它们有多不同。这个修复是仅仅阻止了你使用 6 杯面粉，还是也意外地阻止了你使用 1 杯面粉？
新方法（本文的方法）： 本文的作者构建了一个工具，它就像一个超级聪明的品尝测试员。它不只是说“不同”，而是会问：“在哪些确切的面粉用量下，这两份食谱做出的蛋糕完全一样，而在哪些用量下它们做出的蛋糕不同？”随后，它会计算出一个百分比：“90% 的情况下，蛋糕的味道是一样的。只有 10% 的情况下（当你使用大量面粉时），新规则才会改变结果。”

核心问题：“坏”修复 vs. “好”修复

在软件安全领域，开发者修补漏洞（安全缺陷）以阻止黑客。但有时，补丁过于激进。

“好”补丁： 想象一下俱乐部的门卫，他只阻止那个试图持假身份证混进去的家伙。其他人都能进入。俱乐部的运作基本未受影响。
“坏”补丁： 想象一下门卫决定：“为了安全起见，我要阻止所有人进入，即使是持有真实身份证的人。”俱乐部现在空无一人。这个“修复”起作用了（没人混进去），但它破坏了俱乐部的功能。

本文认为，我们需要一种方法来衡量补丁影响了多少“俱乐部”（即程序的输入）。如果一个补丁改变了 90% 所有可能输入的行为，那它就是一个危险且过于宽泛的修复。如果它只改变了 0.1% 的输入（即实际的黑客）的行为，那它就是一个精确且良好的修复。

他们是如何做到的：“范围搜索”启发式方法

为了弄清楚这一点，作者使用了一种称为符号执行的技术。你可以将其想象为在模拟环境中运行程序，其中的输入不是具体的数字（如"5"或"100"），而是“任意数字”。

然而，检查每一个可能的数字是不可能的（数量太多了！）。因此，他们发明了一个巧妙的捷径，称为基于范围的搜索：

“分而治之”策略： 工具不是检查每一个数字，而是查看数字的大块（范围）。
“放大”技术：
- 它检查一个巨大的范围（例如 0 到 1,000,000）。
- 如果两个程序在整个范围内表现相同，那太好了！它将整个块标记为“安全”。
- 如果它们表现不同，工具会将该块一分为二并检查这两个半块。
- 它不断分割，直到找到行为发生变化的确切“边界”。
“零”优先级： 他们注意到，程序通常对小数字（如 0、1 或 2）表现正常，而只有在数字巨大时才会出错。因此，他们的工具优先检查“中心”（小数字），然后再向外扩展到边缘。这使得分析速度快得多。

他们的发现

该团队在来自 Linux、Qemu 和 FFmpeg 等著名开源项目的90 个真实世界安全补丁，以及一个已知“好”补丁和“坏”补丁的数据集上测试了他们的工具。

识别过度反应者： 他们发现，“坏”补丁（那些破坏功能的补丁）改变了近**97%所有可能输入的程序行为。“好”补丁仅改变了约29%**的输入行为。
“Crowdstrike"警告： 论文指出，影响大量输入的补丁是危险的。如果一个补丁改变了 90% 用户的使用程序方式，它更有可能导致大规模中断（就像著名的 Crowdstrike 事件），因为它改变了系统的太多部分。
修正基准测试： 他们还在一个名为EqBench的标准测试套件上测试了他们的工具。他们发现，该测试套件中有 5 个程序被标记为“等价”（相同），但他们的工具证明它们实际上由于特定的数学故障（整数溢出）而不同。这表明他们的工具比现有标准更精确。

结论

本文提出了一种衡量软件补丁“影响范围”的方法。它不再仅仅问：“这个补丁不同吗？”而是问：“它有多不同，确切地说在什么时候才重要？”

通过量化这一点，开发者可以判断一个安全修复是外科手术式打击（仅修复坏输入）还是核选项（几乎让所有人无法使用程序）。这有助于他们决定该补丁是否可以安全部署，或者在上线前是否需要更多测试。

技术摘要：量化符号补丁影响分析

问题陈述

传统的等价性检查将程序分类为“等价”或“非等价”。这种二元分类对于补丁影响分析而言是不够的，因为修补后的版本预期应与原始（存在漏洞的）代码非等价，以修复漏洞。虽然非等价是预期的，但关键挑战在于确定程序在何种条件下存在差异，以及输入域的百分之多少受到了影响。

现有方法往往无法区分“好”补丁（修复漏洞的同时为大多数输入保留了功能）与“坏”补丁（过度限制输入，例如通过硬编码安全值或拒绝所有输入），后者在输入域中引入了显著更大范围的非等价性。目前缺乏能够形式化量化这种行为分歧的技术。

方法论

作者提出了量化部分等价分析，这是一个通过测量输入域上行为分歧的程度来细化非等价性的框架。该方法论包含三个主要组成部分：

1. 部分等价的形式化

论文将程序 $P$ 定义为从输入域 $D_{IP}$ 到输出域 $D_{OP}$ 的全函数。给定两个具有相同输入域的程序 $P_1$ （原始）和 $P_2$ （修补后）：

等价集（ $D_{eq}$ ）： $P_1(\vec{I}) = P_2(\vec{I})$ 成立的输入集合。
非等价集（ $D_{neq}$ ）： $P_1(\vec{I}) \neq P_2(\vec{I})$ 成立的输入集合。
补丁影响面： 定义为 $D_{neq}$ 。目标是计算等价条件（ $F_{eq}$ ）以及 $D_{eq}$ 成立的输入域百分比。

2. 符号分析与摘要

该方法利用扩展符号执行为两个程序生成符号摘要（ $S_P$ ）。符号摘要是一个逻辑公式，表示所有执行路径中输入与输出之间的关系。

算法 1（EqChecker）： 通过检查 $S_1 \Leftrightarrow S_2$ 和 $S_1 \land S_2$ 的可满足性，将程序分类为等价（ $T_{eq}$ ）、完全非等价（ $T_{neq}$ ）或部分等价（ $P_{eq}$ ）。

3. 量化技术（范围搜索启发式）

为了在数值域中高效量化 $D_{eq}$ 和 $D_{neq}$ 的大小，作者提出了一种基于范围的搜索启发式。这避免了枚举所有输入或在大型域中使用昂贵的模型计数所带来的计算不可行性。

关系范围搜索（算法 2）： 递归地将输入域划分为子域（折半范围），并检查这些子域内的等价性或完全非等价性。它能捕捉多个变量之间的关系条件，但具有指数级复杂度 $O((2^N)^{LIMIT})$ 。
迭代范围搜索（算法 3）： 一次处理一个输入参数以提高可扩展性，将复杂度降低至 $O(N \times 2^{LIMIT})$ 。然而，它无法捕捉变量之间的约束关系。
迭代优先级范围搜索（算法 5）： 根据程序更可能在较小绝对值处等价的直觉，按优先级（负值、零、正值分区）划分域，优先处理零附近的区域。
组合范围搜索（算法 6）： 整合迭代方法和优先级方法，为每个输入参数选择最佳等价性下界，从而提供稳健的分析。

4. 基线比较

作者将他们的范围搜索方法与以下方法进行了比较：

枚举模型计数： 通过 SMT 求解器迭代地寻找满足解。
投影与模型计数： 使用量词消除和模型计数工具（SearchMC, Ganak, qCoral, ABC）计算等价百分比。

主要贡献

形式化： 论文形式化了部分等价和补丁影响面的概念，将等价性分析扩展为包含等价/非等价条件及其对应的百分比。
技术开发： 提出了一种专门用于数值输入域高效量化分析的基于范围搜索的技术，提供了等价性的可靠下界。
补丁影响分析： 该技术被应用于评估补丁影响，区分对输入域影响最小的补丁（好补丁）与过度限制输入的补丁（坏补丁）。
基准评估： 该方法在以下基准上进行了评估：
- PatchBench： 来自 Linux、Qemu 和 FFmpeg 的 90 个 CVE 补丁。
- JulietBench： 50 个包含好补丁和坏补丁（包括 LLM 生成的坏补丁）的程序。
- EqBench： 47 个 C 程序，其中该工具识别出 5 个因整数溢出而被错误标记为“等价”的案例。

实验结果

补丁区分： 在 JulietBench 数据集中，坏补丁的平均补丁影响面为96.65%，而好补丁仅影响了**29.03%**的输入域。
现实世界差异： 在 PatchBench 中，36.25% 的补丁对超过 90% 的输入域是非等价的，而 20% 的补丁影响小于 10%。这突显了现实世界补丁影响的显著差异。
准确性与效率：
- 组合范围搜索方法在 PatchBench 上产生了精确等价结果（已知真实值）的准确率达到81.8%，在 EqBench 上达到95.2%，比次优方法高出 30.7%。
- 它提供了比模型计数方法更接近真实值的近似，平均偏差比次优方法低约29.4%。
- 执行时间： RangeSearch 在 PatchBench 上的运行速度比 SearchMC 快约8 倍，在 EqBench 上快2 倍。
EqBench 发现： 分析识别出 EqBench 中 5 个被错误标记为等价的案例；该工具正确地将它们识别为因整数溢出条件而部分等价。

意义与主张

论文声称，量化部分等价分析有效地表征和量化了补丁影响，提供了比二元等价性检查更精细的见解。

安全影响： 它有助于识别可能需要额外审查的补丁（例如那些影响输入域大部分区域的补丁），并区分那些保留功能的secure补丁与那些因过度限制输入而破坏现有假设或 CI/CD 流水线的补丁。
方法论贡献： 该工作引入了一种新颖的范围搜索启发式方法，平衡了可扩展性和精确性，解决了现有符号执行和模型计数技术在补丁影响分析背景下的局限性。
局限性： 作者承认该方法依赖于差分符号执行；如果无法生成符号摘要，分析就无法进行。此外，当前的范围搜索启发式方法专注于数值域，尽管作者指出有扩展到其他域（例如字符串）的潜力。

作者并未声称解决了所有补丁分析问题，而是提出他们的量化方法为理解软件补丁的行为后果提供了必要的粒度层次。