Lean 核心漏洞修復：AI 生成的證明暴露弱點

Lean 核心漏洞修復：AI 生成的證明暴露弱點

近期，Lean 核心的 soundness bug （#14576）被報告並修復，這個漏洞的出現與修復過程引起了技術界的關注。這個漏洞是由 AI 生成的證明 所暴露，該證明試圖證明 Collatz 猜想 ，但實際上是利用了 Lean 核心處理 nested inductive types 的一個漏洞。

背景分析

7 月 25 日，Ramana Kumar 發布了一個儲存庫，內含一個使用 AI 助手 生成的、對 Collatz 猜想的「反證」，但這個反證並不是一個有效的證明。它實際上是利用了 Lean 核心的一個漏洞，這個漏洞與 inductive types 的處理有關。7 月 28 日，Kiran Gopinathan 將這個問題簡化為一個小型的 False 證明，並開啟了 #14576 號問題。就在報告後的一個小時內，開發團隊就推出了修復方案 (#14577)。Joachim Breitner 對這個修復方案進行了審查和改進，最終這個修復方案被合併到主分支中。

技術分析

這個漏洞的本質在於當 Lean 核心處理 nested inductive types 時，如果這些型別的參數是 phantom （不在建構子欄位中被提及），則這些參數會在生成的輔助型別中消失，從而逃避型別檢查。這樣就可能使用一個不合法的引數使得核心接受一個 False 的證明。這個漏洞只能通過 metaprogramming 的方式觸發，即直接向核心發送 inductive declaration。Lean 的前端會檢查引數並捕捉不合法的術語，因此這個漏洞並不是 Lean 的 meta-theory 中的漏洞，而是一個實現上的錯誤。

影響與展望

這個事件也涉及到 nanoda，這是一個由 Chris Bailey 使用 Rust 實現的、針對 Lean 的外部檢查器。原來的 Collatz 儲存庫曾經通過了一個一周前的 nanoda 版本，但是令人驚訝的是，這裡涉及到兩個無關的漏洞。官方核心有一個缺失的檢查在 nested inductive type 的支持中，而 nanoda 則沒有驗證型別名稱在投影節點中。nanoda 的漏洞由 Jeremy Chen 報告，並在 Lean 漏洞被報告的一周前就已經被修復。這個證明是這樣構建的，以至於核心永遠不會檢查的表達式，正是老版本的 nanoda 所接受的。

對於這個事件，Ramana Kumar 認為時間上的巧合是偶然的，但不能排除模型可能已經看到 nanoda 的報告。Joachim Breitner 提出了一個假設，認為時間上的巧合是由於強大的模型能夠找到這個漏洞的可用性所致。

未來展望

這個事件對於使用 Lean 的用戶來說是一個警醒，雖然使用獨立的核心進行檢查仍然是有效的，但用戶需要確保自己使用的是最新版本的核心和外部檢查器。這個事件也對 lean4lean 產生了影響，因為其對 inductives 的處理是對參考實現的移植，因此也受到這個核心漏洞的影響。Mario Carneiro 的 lean4lean 是對 Lean 型別理論的形式化，以及一個證明，該證明表明核心實現了這個理論。這項工作仍在進行中，目前的證明還沒有涵蓋 inductive types，而等待驗證的實現也受到同樣的漏洞影響。

最後，針對有人建議移除或限制 metaprogramming 以防止這種攻擊的想法，認為這是誤導性的。因為 elaborator 是一個複雜的系統，限制 metaprogramming 不僅可能限制了 Lean 的表達力，也不一定能夠徹底解決這類問題。因此，開發者和用戶需要共同努力，持續改進和完善 Lean 的實現和檢查機制，以確保其安全性和可靠性。