一句话：提出P³框架，自动为C语言补丁构造乘积程序，支持复杂补丁并无缝对接AFL++与KLEE进行补丁推理。
软件持续变更，补丁易引入新错误或安全漏洞。为程序编写完整功能规约很难，但用未打补丁版本描述补丁后行为的补丁规约往往容易，例如“补丁后版本是补丁前版本的重构”。为推理此类规约，分析器需同时分析补丁前后版本。本文提出 P³，一个通过乘积程序自动推理补丁的框架。P³ 是首个面向真实语言 C 自动构造乘积程序的框架，支持真实软件中多样且复杂的补丁，并提供运行时支持，使灰盒模糊测试与符号执行等技术无需修改即可运行。在 CoREBENCH 复杂补丁集上的实验表明，P³ 能处理复杂代码，与 AFL++ 和 KLEE 互操作，并支持补丁规约推理。
Software systems change on a continuous basis, with each patch prone to int roducing new errors and security vulnerabilities. While providing a full functional specification for the program is a notoriously difficult task, writing a patch specification that describes the behaviour of the patched version in terms of the unpatched one (e.g., “the post-patch version is a refactoring of the pre-patch one”) is often easy. To reason about such specifications, program analysers have to concomitantly analyse the pre- and post-patch software versions. In this paper, we propose P 3 , a framework for automated reasoning about patches via product programs . While product programs have been used before, particularly in a security context, P 3 is the first framework that automatically constructs product programs for a real-world language (namely C), supports diverse and complex patches found in real software, and provides runtime support enabling techniques as varied as greybox fuzzing and symbolic execution to run unmodified. Our experimental evaluation on a set of complex software patches from the challenging CoREBENCH suite shows that P 3 can successfully handle int ricate code, int er-operate with the widely-used analysers AFL++ and KLEE, and enable reasoning over patch specifications.
@article{paperbot2955,
title = {P³: Reasoning about Patches via Product Programs},
author = {Arindam Sharma and Daniel Schemmel and Cristian Cadar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763145}
}