Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction

这篇论文提出了一个名为”Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction”的方法，用于修复程序漏洞。该方法通过提取崩溃约束（Crash-Free Constraint, CFC）来指导程序修复，而不需要依赖大量的测试用例。这种方法旨在解决传统测试驱动的程序修复技术中存在的过拟合问题，特别是在修复安全漏洞时。

主要内容和贡献：

概念贡献：
- 提出了一种新的程序修复技术，通过提取崩溃约束来修复安全漏洞，从而避免过拟合问题。
- 这种方法对于检测和修复安全漏洞非常重要，因为许多安全漏洞在被报告为CVE后可能长期未被修复。
技术贡献：
- 崩溃约束提取：通过预定义的模板从违反条件的 exploit 迹象中提取崩溃约束。例如，缓冲区溢出可以表示为访问缓冲区的条件约束。
- 修复定位：使用依赖性分析来确定潜在的修复位置，而不是依赖统计故障定位。
- 约束传播：将提取的崩溃约束从崩溃位置传播到修复位置，确保修复后程序满足约束。
- 补丁合成：使用二阶程序合成和归纳合成技术生成满足约束的补丁。
工具实现：
- 实现了一个名为 ExtractFix 的工具，基于 KLEE 符号执行引擎，用于漏洞修复。
- 该工具在 ManyBugs 基准测试、真实世界的 CVE 和 Google 的 OSS-Fuzz 框架上进行了评估，表现出了较高的修复效率和正确性。
实验结果：
- 在 56 个漏洞中，ExtractFix 成功提取了 43 个正确的崩溃约束，并生成了 43 个补丁，这些补丁通过了失败诱导的测试。
- 与 Prophet、Angelix 和 Fix2Fit 等现有工具相比，ExtractFix 在修复漏洞时表现出更好的效果，特别是在避免过拟合方面。

结论：

该论文提出的方法和工具 ExtractFix 为解决程序修复中的过拟合问题提供了一种有效的方式，通过提取和传播崩溃约束来生成高质量的补丁，适用于各种安全漏洞的修复。

方案设计和技术路线总结

方案设计

该论文提出了一种新的程序漏洞修复方法，旨在解决传统测试驱动修复技术的过拟合问题。其核心思想是通过分析程序崩溃时的约束条件（称为崩溃自由约束，CFC）来指导修复过程，而不需要依赖大量的测试用例。具体方案设计如下：

崩溃约束提取：
- 利用 sanitizers（如 AddressSanitizer、UBSAN）来检测程序中的不安全行为，当检测到问题时程序崩溃。
- 从崩溃中提取 CFC，该约束表示程序在崩溃点应满足的条件，以避免漏洞。
修复定位：
- 由于只有单个失败测试（即 exploit），采用控制和数据依赖性分析从崩溃位置反向寻找潜在的修复位置。
- 通过依赖性分析和支配性分析确定修复位置候选集。
约束传播：
- 从修复位置到崩溃位置传播 CFC，确保在崩溃点满足该约束。
- 使用符号执行探索所有可能的路径，收集路径约束，计算最弱前导条件。
补丁合成：
- 采用二阶程序合成结合归纳合成技术生成满足传播后 CFC 的补丁。
- 通过验证确保补丁在所有可能输入下满足 CFC。

技术路线

崩溃约束提取：
- 使用 sanitizers 捕获程序崩溃，并从崩溃中提取 CFC。
- 通过预定义的模板将崩溃表达式转换为 CFC。
修复定位：
- 从崩溃位置出发，利用控制和数据依赖性分析确定修复位置。
- 通过依赖闭包和支配性分析缩小候选修复位置范围。
约束传播：
- 采用符号执行从修复位置到崩溃位置探索所有路径，收集路径约束。
- 计算最弱前导条件，确保在崩溃点满足 CFC。
补丁合成：
- 使用第二-order 合成技术生成补丁，结合 CEGIS 验证补丁的正确性。
- 确保生成的补丁在所有输入下满足 CFC。

挑战与解决方案

约束提取挑战：通过 sanitizers 和模板化方法准确提取 CFC。
修复定位挑战：仅凭单个失败测试，利用依赖性分析定位修复位置。
约束传播挑战：处理复杂控制流和数据流，包括循环和递归。
补丁合成挑战：生成满足 CFC 的正确补丁，确保其普遍适用性。

评价与展望

有效性：在 ManyBugs 基准测试和真实世界 CVE 上表现出色，生成正确补丁数量多于现有工具。
扩展性：模板化约束提取易于扩展，以支持新的漏洞类型。
性能考量：符号执行的计算复杂性，需在实际应用中考虑时间资源限制。

总体而言，该方法为解决程序修复中的过拟合问题提供了一种有效途径，通过约束导向的修复方式，生成更为健壮的补丁，适用于多种安全漏洞的修复。

CFC

概述

Crash-Free Constraints (CFCs) 是一种用于自动程序修复的创新方法，特别适用于解决安全漏洞。与传统的基于测试的修复方法相比，CFCs 通过提取崩溃时的约束条件来生成补丁，从而确保程序在任何情况下都不会因漏洞而崩溃。

关键概念

定义与目的
- CFC: 一种条件，如果满足该条件，程序将不会因特定漏洞而崩溃。
- 目标: 生成确保 CFC 始终满足的补丁，从而防止漏洞被利用。
提取与应用
- 提取: 使用 AddressSanitizer 或 UBSAN 等工具从崩溃中提取 CFC。
- 模板: 预定义模板将特定类型的崩溃（如缓冲区溢出、空指针解引用）映射到相应的 CFC。
- 示例: 对于缓冲区溢出，CFC 可能是 0 <= i < size_of_a，以确保数组边界被尊重。
修复过程
- 定位: 使用控制和数据依赖性分析从崩溃位置反向寻找潜在的修复位置。
- 传播: 使用符号执行从修复位置到崩溃位置探索所有路径，收集路径约束，计算最弱前导条件。
- 合成: 采用二阶程序合成结合归纳合成技术生成满足传播后 CFC 的补丁，确保其普遍适用性。