基于VERIBIN的二进制补丁自适应验证研究学术报告

一、 作者、机构与发表信息

本研究的主要作者为：Hongwei Wu（第一作者），Jianliang Wu， Ruoyu Wu， Ayushi Sharma， Aravind Machiry 与 Antonio Bianchi（通信作者）。研究机构为美国普渡大学（Purdue University）和加拿大西蒙菲莎大学（Simon Fraser University）。该项研究成果以题为《VERIBIN: Adaptive Verification of Patches at the Binary Level》的论文形式，于2025年2月24日至28日在美国加州圣地亚哥举办的网络与分布式系统安全研讨会（Network and Distributed System Security Symposium， NDSS）上发表。NDSS是网络安全领域的顶级会议之一，这标志着该研究得到了学术界的认可。

二、 学术背景与研究目的

本研究属于软件安全与程序分析领域，具体聚焦于二进制补丁验证这一细分方向。研究背景源于软件安全维护中的一个核心困境：补丁鸿沟。软件供应商在接收到包含安全修复的新版本软件后，往往因为无法充分保证该补丁不会破坏原有功能（即引入回归错误）而延迟甚至放弃部署。这个问题在仅能获得已编译的二进制补丁时尤为严峻，因为此时无法对源代码进行手动审查，而现有的自动化补丁分析技术大多依赖源代码，无法适用。即使源代码可用，通过修改编译流水线直接在二进制中植入恶意代码（如近期发生的XZ Utils后门事件）的风险，也凸显了在二进制层面进行补丁验证的必要性。美国国防高级研究计划局（DARPA）的“确证微修补”项目也强调了这一需求。

为了弥合补丁鸿沟，帮助供应商安全地部署补丁，本研究旨在开发一种能够直接比较原始二进制程序与其修补后版本，并判断补丁是否“可安全应用”的系统。“可安全应用”的核心定义是：补丁保留了原始程序的功能，即它不会引入可能导致原始功能中断的修改。这特指功能性的保持，而非保证漏洞本身已被修复。具体目标是在仅有二进制文件的情况下，验证补丁满足一系列功能保持属性，即“可安全应用”属性。这些属性借鉴了源代码层面验证工具Spider的定义，但在二进制层面实现面临巨大挑战，如源代码语义信息（变量名、数据类型、标签）的缺失，以及符号执行大型函数的复杂性。

三、 研究详细工作流程

研究团队设计并实现了名为VERIBIN的系统，其工作流程包含预处理、符号执行、错误处理出口路径识别、属性验证以及自适应验证五个核心步骤，研究样本涵盖来自三个数据集的86对原始与已修补二进制文件。

1. 预处理

   • 研究对象与样本：输入为原始二进制文件、修补后二进制文件，以及受补丁影响的函数地址对。在评估中，共处理了来自三个数据集（MicroPatch Bench， AMP挑战集， PatchDB二进制数据集）的125对二进制文件，最终成功支持并分析了其中的86对（支持率68.8%）。这些二进制文件大小从5KB到120MB不等，涵盖了不同复杂度的真实世界安全补丁。
   • 处理与分析：此步骤利用现有二进制分析工具（如BinDiff， IDA Pro， Angr）提取后续验证所需的关键信息。具体包括：
     • 被调用函数信息：收集受补丁影响函数（原始版Fo与修补版Fp）内部所有被调函数的原型（参数数量与类型）以及在两个二进制中的匹配地址。
     • 匹配基本块地址：通过二进制差异分析获取Fo和Fp中相匹配的基本块地址。
     • 控制流图：为Fo和Fp构建控制流图。
   • 新颖方法：为提高函数原型恢复的准确性，VERIBIN采用了逆向反编译策略——在分析一个函数前，先对其所有被调用的函数进行反编译，以提供更多上下文信息。提取的信息存储于配置文件中，分析师可手动校正。

2. 符号执行

   • 研究对象：Fo和Fp函数。
   • 处理与分析：使用欠约束符号执行（Under-constrained Symbolic Execution）从函数入口点开始，系统地探索所有可达的执行路径。研究采用Angr框架执行此任务。为提升可扩展性并避免路径爆炸，设置每个基本块最多被访问两次，并通过前瞻性剪枝（仅当路径约束可满足时才探索新分支）避免不可行路径。对于函数调用，将其视为未解释函数（Uninterpreted Function），生成包含函数名和符号化参数的表达式作为返回值，并相应地更新输出参数指向的内存内容。
   • 数据收集：对于每一条执行路径，收集以下信息：路径约束（PC， 决定输入走该路径的条件）、符号化寄存器值、符号化内存状态以及函数调用及其参数。

3. 错误处理出口路径识别

   • 研究挑战：在二进制层面准确识别EEPs（Error-handling Exit Paths）比源代码层面更困难，因为常见的错误处理模式（如特定函数名、goto标签）在编译后消失。
   • 处理与分析：VERIBIN不依赖固定的错误标记，而是通过结合静态分析和启发式规则，在路径级别直接识别EEDs。
   • 新型启发式规则：
     • 启发式A：调用已知的错误处理函数（如 exit, abort）或标记为 noreturn 的函数。
     • 启发式B：返回值为无效值。通过分析函数所有路径的返回值，通常将负值（如-1）或较短路径对应的布尔值判定为无效。
     • 启发式C：路径长度相对较短。基于添加输入验证的补丁通常会导致一个分支快速终止的观察，将长度小于所有路径平均长度特定比例（如0.8）的路径判为EEP。
   • 结果：识别出的EEP路径将被排除，剩下的路径即为有效出口路径。

4. “可安全应用”属性验证

   • 验证属性：针对Fo和Fp，验证四个核心属性：P1（非扩张输入空间）、P2（非局部内存写等价）、P3（返回值等价）、P4（函数调用等价）。
   • 核心创新方法——匹配路径对：为避免直接组合所有VEPs的路径约束带来的复杂性问题，VERIBIN提出了匹配路径对概念。MPP是一对来自Fp和Fo的VEP，满足Fp中该路径的路径约束蕴含Fo中对应路径的路径约束。通过优先匹配相似度高的路径对，可以显著减少SMT求解器的调用次数。
   • 处理流程：
     • 处理编译器引入的偏移变化：由于重编译导致的变量地址偏移是二进制比较的常见障碍。VERIBIN采用三种技术应对：基于内容的比较（比较不同地址中的内容是否相同）、偏移分析（检查所有不匹配的局部变量地址是否偏移量一致）、结构位置关联（基于抽象语法树中结构位置相似的表达式可能对应同一变量）。
     • 验证P1（非扩张输入空间）：若Fo和Fp是可分的（所有VEPs都能组成MPP），则P1自动成立。若不可分，则将Fo和Fp所有VEPs的路径约束进行逻辑“或”组合，并用SMT求解器检查Fp的组合约束是否蕴含Fo的组合约束。
     • 验证P2（非局部内存写等价）：对于每个MPP（或组合后的情况），比较两个版本在对应路径上对非局部内存（如全局内存）的写入操作，检查写入的地址和值是否符号等价。
     • 验证P3（返回值等价）：比较MPP中两条路径的返回值是否符号等价。
     • 验证P4（函数调用等价）：比较MPP中两条路径上发生的函数调用，要求被调用函数匹配（通过二进制差异分析确定），且每次调用的参数值符号等价。

5. 自适应验证

   • 目的：处理自动化验证无法通过的语义等价变更（如将函数sha1替换为sha256，增加无副作用的日志函数调用等）。
   • 处理流程：当某个属性验证失败时，VERIBIN会内省失败的符号约束，定位根本原因，并将其转换为针对分析师的、易于理解的文本查询（例如，“将foo函数的第6个参数从20改为10是否可被视为安全的？”）。分析师根据其对补丁意图和二进制程序的理解回答“是”或“否”。VERIBIN利用分析师的回答来简化符号约束，并重新进行属性验证。如果分析师不确定，可保守地回答“否”，系统将判定补丁非“可安全应用”。

四、 主要研究结果

1. 有效性结果：在包含86对二进制样本的评估中，VERIBIN在严格遵循属性的标准下，实现了93.0%的准确率，并且零误报。这意味着被VERIBIN判定为“可安全应用”的补丁确实是功能保持的，为部署决策提供了高可信度保障。在剥离符号信息的二进制文件上测试，准确率略有下降（89.4%），但仍保持零误报，表明了其对现实世界场景的适用性。
2. 效率结果：平均每对二进制补丁的分析时间为1293.8秒（约21.5分钟），其中符号执行和属性验证各占约一半时间。研究显示，采用MPP优化可使验证时间相比标准方法（组合所有路径约束）减少75%。处理CIOCs的技术则将准确率提升了12%。
3. 自适应验证评估结果：在启用自适应验证后，VERIBIN能够处理因语义等价变更而不严格满足自动验证属性的补丁。评估显示，58%的补丁在分析师判断下被视为“可安全应用”，而严格自动验证仅能识别37%。在自适应模式下，VERIBIN平均每个补丁会向分析师提出约1.3个问题，估计分析师回答每个问题约需10分钟。
4. 与源代码工具的对比结果：与最先进的源代码补丁验证工具Spider相比，VERIBIN在支持的样本上准确率更高（96.5% vs 62.0%），且误报率极低（0% vs 27.9%）。虽然Spider在理论上能分析更多样本（支持率63.2% vs 68.8%），但VERIBIN在二进制层面的直接分析避免了源代码工具可能遇到的误判问题，并在XZ Utils后门这类源代码分析可能失效的案例中展现了独特价值。
5. 案例研究结果：研究通过多个具体案例展示了VERIBIN的能力：
   • XZ Utils后门检测：VERIBIN成功检测出恶意版本中增加的恶意函数调用（__get_cpuid）和修改的返回值逻辑，从而将其标记为“非可安全应用”，验证了其在发现恶意篡改方面的有效性。
   • 密码学函数替换（AMP挑战案例）：VERIBIN通过自适应验证，在分析师确认evp_des_ede3_cbc与evp_aes_256_cbc语义等价后，成功将该补丁验证为“可安全应用”。
   • 输入空间扩张补丁：VERIBIN正确识别出一个将错误条件放宽、从而扩大有效输入空间的补丁为“非可安全应用”。
   • 编译器偏移变化处理：VERIBIN成功处理了因栈大小调整导致的变量偏移变化，正确判定了一个添加安全检查的补丁为“可安全应用”。

五、 研究结论与价值

本研究得出结论：VERIBIN是首个能够在二进制层面系统化描述补丁行为并验证其功能保持性的系统。它通过形式化“可安全应用”属性、设计高效的基于路径对的验证方法、引入自适应验证机制以及解决二进制分析特有的挑战（如CIOCs），实现了高准确率与零误报。

其科学价值在于： 1. 填补研究空白：开创了二进制补丁自动化形式化验证的先河，为解决“补丁鸿沟”这一实际问题提供了新的技术路径。 2. 方法创新：提出了匹配路径对、针对二进制特性的多种启发式规则和处理技术，丰富了程序分析，特别是二进制差异分析和符号执行在安全验证中的应用。 3. 人机协同范式：自适应验证的设计，为需要领域知识的复杂程序分析任务提供了一种有效的人机交互范式。

其应用价值在于： 1. 提升补丁部署安全性：为软件供应商、系统集成商和安全运维人员提供了一种可靠的工具，用于评估第三方或仅以二进制形式提供的补丁的安全性，降低回归风险。 2. 增强供应链安全：可作为软件供应链安全审查的一环，用于检测二进制分发物中是否存在未声明的、潜在破坏性的修改，如XZ Utils类的后门。 3. 支持遗留系统维护：对于源代码丢失或构建过程复杂的遗留系统，二进制补丁可能是唯一选择，VERIBIN为验证此类补丁提供了可能。

六、 研究亮点

1. 首创性：首个针对二进制补丁功能保持性进行形式化验证的系统。
2. 高保证性：设计目标为零误报，在实际评估中实现，为“可安全应用”的判定提供了高可信度。
3. 高效性：通过匹配路径对优化，大幅提升了验证效率。
4. 实用性：能够处理真实世界、不同规模的二进制程序，并包含自适应机制以应对自动化难以处理的语义等价变更。
5. 前瞻性验证：成功应用于检测著名的XZ Utils后门，证明了其在应对现代软件供应链攻击中的现实意义。

七、 其他有价值内容

研究团队已将VERIBIN的代码公开，以促进该领域的进一步研究。论文也详细讨论了系统的局限性，例如其正确性依赖于底层二进制分析工具（Angr， IDA Pro， BinDiff）的准确性；在处理大型复杂函数或深层循环时可能遇到可扩展性问题；以及当前主要关注修改现有函数的补丁，对增删函数的补丁支持有限。这些为未来的改进指明了方向，例如集成更健壮的反编译器、探索增量分析、以及扩展对增删函数补丁的支持。