Lean Kernel Soundness Bug #14576 Postmortem

概述

Lean 已经修复了一个内核健全性漏洞 (#14576)，该漏洞允许构造无效证明，包括一个所谓的 AI 辅助的 Collatz 猜想反证。该漏洞是内核在处理嵌套归纳类型时的实现错误，而非 Lean 底层元理论的缺陷。该漏洞是在一名用户发布了一个无需 sorry 的 Collatz 猜想反证后被发现的，该反证利用了内核未能正确验证嵌套归纳类型中虚幻参数 (phantom parameters) 的缺陷。

技术根本原因：嵌套归纳类型的处理

当内核在归纳类型 T 下消除一个嵌套出现项时，如果这些参数是“虚幻”的（即它们未在构造函数字段中被提及），它们就会从生成的辅助类型中消失。这种健全性漏洞发生在内核消除嵌套出现项时。这允许类型错误的参数逃避类型检查，从而可以被用来证明 False。

至关重要的是，该漏洞只能通过元编程直接向内核发送归纳声明来触及。Lean 前端（elaborator）会执行其自身的检查并会捕获该类型错误项；然而，内核必须保持作为健全性的唯一真理来源，因为设计上 elaborator 是不可信的。

独立验证的失败 (nanoda)

尽管使用了独立检查器，该漏洞利用程序仍通过了 nanoda 的一个版本，这是一个基于 Rust 的 Lean 独立内核。这发生是因为两个独立漏洞的巧合对齐：

Lean 内核漏洞： 嵌套归纳类型支持中缺失的检查。
nanoda 漏洞： 在投影节点中未能验证类型名称。

由于该漏洞利用程序经过精心设计，使得 Lean 内核忽略的表达式恰好是旧版 nanoda 接受的表达式，因此该证明通过了两个检查器。这突显了，虽然独立内核提供了强大的安全层，但只有在两个实现都保持最新时，它们才是有效的。

修复与内核加固固化

在发现漏洞 #14576 后，Lean FRO (Formalization Effort) 实施了若干加固措施：

立即修复与回归测试

补丁发布： 在报告发布一小时后就推送了修复程序 (#14577)。
Kernel Arena： 为该漏洞利用程序及相关的非均匀参数案例增加了回归测试，并添加到了 Kernel Arena。
参数验证： 引入了 PR #14582 以确保内核验证嵌套出现项的参数确实表现为参数，而不是仅仅依赖于重新进行类型检查。

AI 驱动的安全审计

Lean FRO 与 OpenAI 的 Daniel Selsam 合作，使用专门用于网络安全的 AI 来寻找内核中进一步的编程错误。这项工作发现了其他几个漏洞 (PRs #14607, #14608, #14609, #14613, #14615, #14616)，所有这些漏洞都已修复。值得注意的是，这些漏洞被 nanoda 捕获，表明独立内核的价值仍然很高。

基础设施改进

强化不变性： 实施了新的 PRs (#14621, #14631, #14632) 以加强内核不变性。
持续集成： comparator.live 现在默认运行 nanoda 并进行每日跟踪，以确保参考实现与独立检查器之间的同步。

讨论与社区见解

社区成员和研究人员就此事件的影响提出了几点看法：

"我认为，将验证结果视为绝对且不可打破的保证是非常重要的，不应将其视为绝对保证，而应将其视为一种极其强大的保证，其中 (1) 健全性问题的表面积已被细致地最小化，并且 (2) 任何实现的健全性问题都会被非常严肃地对待并在短时间内得到修复。"

其他讨论集中在 AI 可能进行的“奖励黑客行为 (reward hacking)”的可能性上，即模型可能会发现利用内核漏洞来“证明”一个结果比解决数学问题更容易。这强调了风险：即使证明通过了验证器，如果验证器本身包含实现错误，那么 AI 生成的正式证明也不能被隐式信任。