AI 生成的 Lean 证明揭示 CPython 中的 418 个漏洞

通过要求 AI 智能体将 CPython 的内部 C 代码重写为 Lean——一种专为机器检查数学证明而设计的语言——研究人员在 Python 解释器中发现了 418 个漏洞。这一形式化过程已经产生了超过 600,000 行经过验证的代码，它通过强制要求对 Python 在“奇特”边缘情况下的行为进行精确的数学定义，识别出了传统测试可能会忽略的关键问题。

此图表可视化了项目在 CPython 代码库中形式化工作的范围和进展。

形式化流水线

该项目遵循严格的四步流水线，以确保 Lean 模型准确反映 CPython 源代码。首先，AI 智能体将 C 函数重写为 Lean，保留包括错误消息和整数溢出在内的精确逻辑。其次，这些副本与真实的 Python 解释器并行运行，在至少 50,000 个输入上进行测试，以确保它们的一致性。

这张图片展示了流水线的第一个步骤，即 AI 智能体在保留精确逻辑的同时将 C 代码重写为 Lean。

由 HN Digest 根据 broyojo.com 报告的数据绘制；数值与源文件一致。

第三，团队陈述应当始终为真的属性，并使用 Lean 的证明检查器对其进行验证。最后，由未编写原始模型的第二个 AI 智能体对工作进行审查，以确保其对源代码是“忠实”的。只有通过此独立审查的函数才被计入已接受的范围。

“编写关于函数的证明迫使你准确说明它在所有这些情况下的行为。你不能留下任何模糊之处，因为证明检查器不会接受它。”

— Formalizing CPython

识别隐藏漏洞

由于形式化证明需要对每一个可能的状态进行精确定义，该过程揭示了 CPython 的行为偏离其预期逻辑的漏洞。例如，团队发现了一个字典调用，当在对象的属性字典上使用特定键时，会导致段错误。

其他发现包括 XML 编辑中的内存损坏，以及一个根据忽略字符的位置产生错误填充的 base32 解码器。该项目还发现 C 版本和纯 Python 版本 pickle 模块之间的差异，它们在不同的嵌套深度处停止运行。

“有用”证明的挑战

一个显著的障碍是防止 AI 生成“空洞”证明——即在技术上正确但无法捕捉到损坏代码的陈述。例如，一个陈述“如果函数返回，结果至少为零”的证明，即使函数总是崩溃，在技术上也是正确的。

此图表解释了“空洞”证明的概念，即陈述在技术上是正确的，但无法识别功能漏洞。

为了解决这个问题，审查人员现在提出一个具体问题：“损坏版本的函数也能通过这个证明吗？”如果损坏版本能通过，则拒绝该证明。这迫使模型变得更具现实意义，例如考虑到可能失败的内存请求或在操作过程中抛出错误的用户代码。

局限性和权衡

虽然形式化验证提供了高度信心，但目前仅限于代码库的一小部分。该项目已覆盖了范围内约 15.7% 的函数，因为在 CPython 这样庞大且陈旧的代码库中对每一个复杂的边缘情况进行建模是劳动密集型的。

此外，经过检查的证明仅保证一个陈述遵循 Lean 模型，而不一定遵循真实的 Python 解释器。如果模型本身是不完整的——例如假设内存请求总是成功，而实际上可能失败——证明可能仍然有效，而真实软件仍存在漏洞。