P3：通过产品程序对补丁进行推理

《Proceedings of the ACM on Programming Languages》：P3: Reasoning about Patches via Product Programs

软件系统持续变化，补丁可能引入新错误和漏洞。补丁规格较易编写，但需分析前后版本。本文提出P3框架，通过乘积程序自动推理补丁，支持C语言，处理复杂补丁，并与AFL++、KLEE集成，实验证明有效。

　　

摘要

软件系统在不断变化，每个补丁都可能引入新的错误和安全漏洞。虽然为程序提供完整的功能规范是一项极其困难的任务，但编写补丁规范来描述补丁版本相对于未补丁版本的行为（例如，“补丁后的版本是对补丁前版本的重构”）通常相对容易。为了对这类规范进行推理，程序分析器需要同时分析补丁前后的软件版本。

在本文中，我们提出了P³，这是一个用于通过产品程序自动化推理补丁的框架。尽管之前已经使用过产品程序，尤其是在安全领域，但P³是第一个能够为实际编程语言（即C语言）自动生成产品程序的框架，支持在实际软件中发现的多种复杂补丁，并提供运行时支持，使得灰盒模糊测试和符号执行等技术能够直接在未修改的代码上运行。我们对CoREBench测试集中的复杂软件补丁进行的实验评估表明，P³能够成功处理复杂的代码，与广泛使用的分析工具AFL++和KLEE进行交互，并实现对补丁规范的推理。