Lean Kernel Soundness Bug #14576 Postmortem

概述

Lean 已解決了一個核心（kernel）的一致性漏洞（soundness bug）(#14576)，該漏洞允許構建無效證明，包括一個據稱由 AI 輔助的 Collatz 猜想反證。該漏洞是核心在處理嵌套歸納類型（nested inductive types）時的實作錯誤，而非 Lean 底層元理論（meta-theory）的缺陷。該漏洞是在一名使用者發布了一個不含 sorry 的 Collatz 猜想反證後被發現的，該反證利用了核心無法正確驗證嵌套歸納類型中虛擬參數（phantom parameters）的缺陷。

技術根本原因：嵌套歸納類型的處理

當核心消除（eliminate）一個在具有參數 Ds 的歸納類型 T 下的嵌套出現時，就會發生一致性漏洞。如果這些參數是「虛擬」的（meaning they were not mentioned in the constructor fields），它們會從生成的輔助類型中消失。這使得類型錯誤的參數得以逃避類型檢查，進而可以用來證明 False。

至關重要的是，此漏洞只能透過元編程（metaprogramming）直接將歸納聲明發送給核心來觸及。Lean 前端（elaborator）會執行其自身的檢查，並會捕捉到類型錯誤的項（term）；然而，核心必須保持作為一致性的唯一真理來源，因為設計上 elaborator 是不可信的。

獨立驗證的失效 (nanoda)

儘管使用了獨立檢查器，該漏洞仍通過了 nanoda 的一個版本，這是一個基於 Rust 的 Lean 獨立核心。這發生是因為兩個獨立漏洞的巧合對齊：

  1. Lean Kernel Bug: 嵌套歸納類型支援中的檢查缺失。
  2. nanoda Bug: 在投影節點（projection node）中未能驗證類型名稱。

由於該漏洞的構建方式使得 Lean 核心忽略的表達式恰好是舊版 nanoda 所接受的，因此該證明通過了兩個檢查器。這突顯了雖然獨立核心提供了強大的安全層，但只有在兩個實作都保持最新時，它們才有效。

修復與核心強化

在發現 bug #14576 之後，Lean FRO (Formalization Effort) 實施了幾項強化措施：

即時修復與回歸測試

  • Patch Release: 修復程式在報告後一小時內發布 (#14577)。
  • Kernel Arena: 已將針對該漏洞及相關非均勻參數（non-uniform-parameter）案例的回歸測試添加到 Kernel Arena。
  • Parameter Validation: 引入了 PR #14582 以確保核心驗證嵌套出現中的參數實際上表現為參數，而非僅僅依賴重新進行類型檢查。

AI 驅動的安全審計

  • Lean FRO 與 OpenAI 的 Daniel Selsam 合作，使用專門用於網路安全領域的 AI 來尋找核心中的進一步編程錯誤。這項工作發現了其他幾個漏洞 (PRs #14607, #14608, #14609, #14613, #14615, #14616), 且全部已修復。值得注意的是，這些漏洞被 nanoda 捕捉到了，這表明獨立核心的價值仍然很高。

基礎設施改進

  • Hardened Invariants: 實施了新的 PRs (#14621, #14631, #14632) 以強化核心不變量（invariants）。

  • Continuous Integration: comparator.live 現在預設執行 nanoda 並進行每日追蹤，以確保參考實作與獨立檢查器之間的同步。

討論與社群洞察

社群成員與研究人員針對此事件的影響提出了幾點看法：

"I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are themselves taken very seriously and fixed in short order."

其他討論集中在 AI 可能進行「獎勵黑客行為」（reward hacking）的可能性上，即模型可能會發現利用核心漏洞來「證明」結果比解決數學問題更容易。這強調了 AI 生成的正式證明不能被隱式地信任，即使它們通過了驗證器，如果驗證器本身包含實作錯誤。

Sources