TyPatch：将补丁转换为用于内核错误检测的 Typestate 规则

历史 Linux 内核补丁捕获了适用于其原始修复站点之外的缺陷知识。最近的工作表明，大型语言模型（LLM）可以从历史补丁中生成静态分析检查器，并使用它们来发现新的内核错误。然而，完整的检查器生成要求模型既能恢复补丁所表达的缺陷语义，又能实现复杂的程序分析机制，包括对象跟踪、别名分析、路径状态维护和过程间传播。将这些职责耦合到单个端到端代码生成任务中可以将简单的缺陷规则转变为不稳定且昂贵的分析器实现问题。为了解决这个问题，我们提出了 TyPatch，它将特定于补丁的缺陷语义与分析器实现分离。 LLM 将每个补丁转换为类型状态规则，指定其跟踪对象、操作、防护、转换和违规。然后，共享后端执行这些规则，将它们的操作绑定到程序事件，跨别名跟踪对象身份，沿着程序路径传播类型状态，并为所有规则生成报告。在 Linux v6.16 上，TyPatch 发现了 559 个不同的错误，其中 121 个已被内核开发人员确认。在与最先进的完整检查器构建工作流程进行的 38 个补丁比较中，TyPatch 使用的生成词元减少了 88.3-90.1%，而其初始报告池的精度比该工作流程生成的报告池的精度高出 3.42-14.95$\times$。