一個 phantom 參數，讓 kernel 收下 False

這篇是 Lean 4 kernel 一次 soundness bug 的事後記錄——從一份看似荒謬的 Collatz「反證」，到一個一小時內修好的 PR，再到後面一連串收緊 kernel 信任邊界的動作。整起事件的核心，是 proof assistant 的 kernel 作為整條信任鏈的根——一旦它能被騙，上面蓋的所有定理都不再可信。這次騙過它的，只是一個「消失的參數」。postmortem 發布在 leodemoura（Leonardo de Moura）自己的部落格上，並經 Sebastian Ullrich 校閱過，記下的不只是修法，還有為什麼團隊選擇不去限制 metaprogramming。

一份 AI 寫的 Collatz 反證，變成一把鑰匙

Ramana Kumar 在 7 月 25 日發布的那份 repository，標題上寫的是「反證 Collatz 猜想」，但 postmortem 說得很直接：這份 repository 是「produced with AI assistance」，而且「It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types.」——目的是利用一個當時還沒被發現的 kernel bug，標題上的「反證」只是包裝。放在 Lean 這種以 kernel 為信任根的系統裡，「證明通過型別檢查」是一句很強的承諾：只要 kernel 點頭，理論上不該有任何漏洞可鑽。

三天後，Kiran Gopinathan 做了一件更有殺傷力的事——把整個攻擊縮到最小。他開的 issue #14576 標題直接寫「Kernel accepts wrong-structure projections, allowing an axiom-free proof of False」，內文附上一份完整的 Bug.lean，最終落在一行：theorem boom : False := nomatch (bad : T false)，而 #print axioms 顯示這個 boom 不依賴任何 axiom。問題出在 kernel 本身：一個「已檢查」的宣告，投影（projection）的結構名稱跟它實際投影的值對不上，kernel 卻沒有察覺。攔下這種不一致，是型別系統存在的目的；這次它偏偏在最需要它的地方沒有發揮作用。

「不依賴任何 axiom」這件事在 Lean 裡有特別的重量。Lean 允許使用者引入額外的 axiom（例如排中律），任何靠 axiom 撐起來的定理，#print axioms 都會誠實列出來，讀者可以自行判斷要不要信任這個 axiom。boom 這個證明繞過的是這整套誠實申報機制本身——這個證明沒有用上任何有爭議的 axiom——kernel 直接判定它為對，什麼都不用申報。Lean 把它定性為 soundness bug，依據是這個繞過機制。「AI 協助寫成」這個描述有個容易滑過去的地方：它沒有說 AI 自己發現了這個 kernel bug；AI 在這裡的角色，是加速產出一份看起來像正經數學論證的展示。用 AI 加速包裝一份帶著漏洞利用的偽證明，跟用 AI 找漏洞是兩件不同的事——postmortem 後段提到的 Daniel Selsam 那條線，才是後者。Collatz 猜想本身是數論裡數一數二有名的未解問題：反覆對一個正整數做「奇數乘三加一、偶數除二」，猜想不管起點是誰，最後都會落回 1，至今沒有人證明、也沒有人找到反例。拿 Collatz 猜想當包裝，比隨便挑一個數論引理更容易吸引非數學背景的讀者點開來看。

把一整套精心包裝的數學反證縮成七、八行不需要任何前提的 False，把 exploit 化簡到最小重現，是排查 soundness bug 的標準做法——它把「這裡有沒有 bug」的問題，從「看懂整個 Collatz 論證」降到「看懂一個 projection」。這幾個關鍵節點連起來是一條時間線：nanoda（獨立的 Rust 版 kernel）在 issue 開出前一週已經修好一個看似不相關的 bug，這個巧合在後面的段落會再回來。這起事件從公開展示到修補合併，前後三天；真正決定性的一小時，會在修補那一段出現。

phantom 參數怎麼從輔助型別上消失

Lean 的 kernel 在處理 inductive type 時，遇到「巢狀」的情況會做一個轉換：如果一個建構子欄位裡出現了形如 I Ds is 的 nested occurrence——也就是另一個 inductive type 套在目前正在定義的型別裡——kernel 會產生一個輔助型別（auxiliary type）把這個巢狀結構攤平，讓後面的型別檢查可以套用一般規則處理，不用特別處理巢狀。postmortem 對根因的描述很精確：「when the kernel eliminates a nested occurrence under an inductive type T with parameters Ds, and these parameters are phantom (not mentioned in constructor fields), they disappear from the generated auxiliary type and thus escape type checking.」——如果外層型別的參數 Ds 是 phantom（沒有出現在任何建構子欄位裡），這些參數在產生輔助型別的過程中就直接消失了，因而逃過了型別檢查。

PR #14577 的說明把同一件事講得更工程：「When eliminating a nested occurrence I Ds is, the parametric arguments Ds are dropped from the generated auxiliary types, so they used to escape type checking.」——這句話跟 issue #14576 標題描述的症狀完全對得上：「Lean accepts a checked declaration containing a projection whose structure name does not match the value being projected.」一個是根因（Ds 在生成輔助型別時被拿掉），一個是症狀（projection 的結構名稱跟被投影的值對不上）——兩者是同一個洞的兩面：Ds 消失了，靠 Ds 撐住的結構一致性也跟著消失，kernel 卻繼續信任這個沒被驗證過的 projection。

這裡的「projection」指的是 Lean 幫每個 structure 自動生成的欄位存取函式——比如一個 pair 型別的 .fst／.snd，本質上就是編譯器自動產生、對映到特定建構子欄位的函式。nested inductive occurrence 之所以需要一個輔助型別，是因為 kernel 的核心遞迴規則只認得「這個型別的建構子直接放什麼」，遇到「這個型別套著另一個型別」的巢狀寫法，就得先攤平成一個等價、kernel 看得懂的形狀，再把攤平前後的對應關係記在生成的 projection 裡。「phantom 參數」這個講法借自更廣義的型別理論慣例——一個型別參數如果只出現在型別簽名裡、沒有真的被任何建構子欄位用到，就叫 phantom，作用通常是幫使用端做額外的型別區分，不影響資料本身怎麼存。放在 kernel 的一般假設裡，「phantom 參數不影響資料表示」這件事沒有錯，問題出在 kernel 的實作把這一步錯誤地簡化成「產生輔助型別時可以不管它」，於是連同該驗證的型別一起略過，缺口就開在這裡。回歸測試後來把這次 exploit 跟 Arthur Adjedj 提出的一個相關 non-uniform-parameter case 一起寫進 Kernel Arena，用意也是同一件事：光是補上這次踩到的具體案例還不夠，得連「同一類假設可能在哪些變體上再犯錯」都覆蓋到。

這個漏洞有一個關鍵限制：它「only reachable through metaprogramming, by sending the inductive declaration to the kernel directly. The frontend checks the arguments and catches the ill-typed term.」——正常寫 Lean 程式碼，走 elaborator 這條路，型別錯誤的宣告根本進不了 kernel。要觸發這個 bug，得繞過 elaborator，用 metaprogramming 直接把構造好的 inductive 宣告塞進 kernel。這條檢查鏈可以拆成四個環節，點開每一個看它實際負責什麼、又假設了什麼它其實無法確認的事。

這張圖也解釋了為什麼「wrong-structure projection」和「phantom 參數消失」聽起來像兩個不同的 bug 描述，卻是同一個環節（Nested occurrence 消去）失守後往下游擴散出的兩種說法——issue 從症狀切入，PR 說明從根因切入，兩者在第三個環節匯合。四個環節裡，唯一一個「知道自己曾經犯錯」的是最後一個：PR #14577 補上型別檢查之後，PR #14582 又回頭確認同一組參數是不是真的表現得像參數，等於是對自己剛做完的修補再多問一次「這樣夠嗎」。

一小時修補，然後是接下來一連串的加固

PR #14577 的標題是「fix: missing check at kernel inductive declaration」，由 leodemoura（Leonardo de Moura 本人）送出，nomeata（Joachim Breitner）審查並改進後合併，關閉了 issue #14576。從 issue 開出到修補合併，postmortem 給出的時間是一小時。一小時聽起來像是跳過了審查，但 postmortem 寫的是「審查並改進後合併」——原作者送出之後，換了另一雙眼睛看過、也動手改過，才真正進主線。這個節奏在 soundness bug 上是合理的取捨——漏洞已經公開，一個可重現的 False 證明擺在那裡，每多等一小時，能觸發它的人就多一分。同一份惡意宣告，修補前後 kernel 的判定差在哪裡？下面的示意根據 issue 與 PR 說明重建，非逐字複製的原始碼。

-- I Ds is 產生輔助型別時
-- 參數 Ds 被拿掉，逃過驗證
theorem boom : False :=
  nomatch (bad : T false)

#print axioms boom
-- 'boom' does not depend
-- on any axioms

-- Ds 在環境中可用之後
-- kernel 重新型別檢查 Ds
theorem boom : False :=
  nomatch (bad : T false)

-- error: type mismatch
-- Ds 未通過檢查，宣告被拒絕

一小時止血只是第一步。postmortem 記下的後續動作有好幾層：先是把這次 exploit 連同一個相關的 non-uniform-parameter case 一起寫進 Kernel Arena 的回歸測試，接著用一個新的 PR 進一步收緊同一個環節的檢查邏輯。再往後，OpenAI 的 Daniel Selsam 用一個專攻資安的 AI 協助 Lean FRO，又在 kernel 裡找出其他程式錯誤，對應六個 PR；另外三個 PR 專門用來強化 kernel invariant；工具鏈也跟著調整，讓一個原本只是「備用意見」的獨立檢查器變成日常流程的一部分。從「有人回報才去看」變成「主動找專家一起去挖」，是事後補救跟事前投資的分野，也是這次 postmortem 花了不少篇幅交代的部分。nanoda 是 Chris Bailey 用 Rust 寫的一套獨立 kernel；兩套完全獨立的實作在同一份宣告上給出不同的判定，多半代表其中一個有 bug。這次事件裡，問題剛好出在兩邊都曾經各自出過瑕疵，只是修復的時間點沒有對齊。這幾個後續動作各自補上什麼？下面每一項都對應一個具體的 PR 或工具變更。

「All of them have been fixed. All of them were caught by nanoda.」——這句話是整起事件裡最實在的證明：這次抓到漏洞的是一個獨立實作的第二顆 kernel，官方 kernel 沒有自己發現；另外三個 PR（#14621、#14631、#14632）則專門用來強化 kernel invariant，postmortem 對這三個 PR 的定性同樣簡短：「We have also hardened kernel invariants.」，沒有進一步展開細節。這幾個後續 bug 沒有一個是靠官方 kernel 自己抓到的——全部先在 nanoda 上冒出來。如果 nanoda 沒有先修好那個「projection 節點沒驗證型別名稱」的舊 bug，這批新問題有沒有可能也一起被漏掉？postmortem 沒有給出答案，而「找一個獨立實作互相校驗」的價值，恰好要在這種答不出來的時候才顯得出來。

kernel 為什麼不能靠 elaborator 把關

修補合併之後，postmortem 花的篇幅比修補本身還長。這種比例分配透露了團隊真正在意的事：一次快速止血不足以讓人放心，得把「為什麼會漏」跟「還有沒有類似的漏」都交代清楚。de Moura 在 postmortem 裡把定性寫得很清楚：這是一個實作層級的錯誤，不是理論基礎出了問題——「This is an implementation bug, not a hole in Lean's meta-theory.」他也順帶處理了一個直覺但錯誤的修法方向：既然這個漏洞只能透過 metaprogramming 觸發，是不是該限制 metaprogramming 直接操作 kernel 的能力？他的回答是否定的，理由是 elaborator 在設計上就不被信任，soundness 不能建立在「一個不被信任的元件會拒絕產生壞項」這個假設上：「The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term.」就算真的限制了 metaprogramming 也擋不住：攻擊者可以直接寫 .olean 檔案或改記憶體，「both of which bypass the elaborator entirely」。真正的防線只能是 kernel 自己，PR #14577 唯一的程式碼變更也落在 src/kernel/inductive.cpp，沒有動 elaborator 的任何規則。

kernel 與 elaborator 的權責分離，在他的定性裡是優點：「This separation and isolation of concerns is one of the main advantages of proof terms.」——elaborator 可以隨便犯錯、可以被繞過，只要 kernel 這一關夠嚴格，整條信任鏈就還站得住。而這次事件暴露的是相反方向的脆弱：kernel 自己出現了一個實作疏漏，而抓到它的又是另一個獨立實作的 kernel。Joachim Breitner 對「nanoda 剛好在 issue 開出前一週修好一個不相關 bug」這個巧合提出的假設是，有能力找到這類 bug 的強模型開始出現了——「the timing coincidence is due to the availability of strong models able to find this bug」。這是一句沒有被進一步證實的猜測，但跟後面 Daniel Selsam 主動找 AI security 專家合作抓 bug 的動作方向一致：Lean 團隊寫下的往後策略是「reaching out to and supporting experts who can find further bugs, develop new kernels, and work on the theory or on verified kernels」：主動接觸並支持能找更多 bug、開發新 kernel、或做理論與 verified kernel 研究的專家；下一次 exploit 出現之前，先把人找齊。「開發新 kernel」不是空話——postmortem 提到 Mario Carneiro 的 lean4lean，用 Lean 自己把 Lean 的型別理論形式化了一次，還附帶一份 kernel 確實實作了該理論的證明，是這條路線上已經存在的另一個獨立驗證點。跟 nanoda 一樣，lean4lean 用完全不同的方式重新推導同一個答案。

對一般工程師來說，「kernel 是信任鏈的根」這句話換到日常開發裡，對應的是任何「理論上不該出錯，一出錯就全盤皆輸」的核心元件——資料庫的 commit 邏輯、支付系統的金額計算、compiler 的型別檢查器。這些元件共同的特徵是：它們的正確性沒辦法靠「上層多做幾次檢查」來彌補，因為上層要依賴它們才能定義什麼叫「正確」。Lean 這次能在一小時內定位並修好，前提是根因足夠具體——一個具名的參數，在一個具名的步驟裡消失，這比「邏輯有問題」這種說法精確得多。把 exploit 化簡到最小重現，比保留原本的 Collatz 包裝更關鍵：根因的範圍窄，修補才有可能在一小時內推出。止血與加固原本就是兩個時間尺度——止血只需要修對一個環節，加固要求團隊重新檢視整組假設，後續那幾個 PR 走的是後一條路。

What changes：kernel 的信任邊界從「相信自己審查自己」變成「靠獨立實作互相校驗」——nanoda 現在是 comparator.live 的預設項、每天追蹤版本，不再是可有可無的第二意見；如果你維護的系統也有一個「理論上不該出錯」的核心元件，這次事件給的具體做法是找一個獨立實作去校對它，而不是加強對周邊元件的限制。