CVE-2026-72844: Lean 4 カーネルの健全性バグ

ネスト帰納的射影の検証バイパスによる、公理なしの 0 = 1 の証明。

脆弱性の概要

Lean 4 カーネルは、射影式で指定された構造体が射影される値の型と一致することを検証しません。 また、src/kernel/inductive.cpp の environment::add_inductive は、補助型に置き換えられるネスト帰納的適用を型検査しなかったため、 それらのパラメトリック引数は検査を逃れました。

Lean プロセス内で実行されるメタプログラムは、型不正なネスト帰納的型を登録できます。 そのコンストラクタは無関係な型 W の値に対して .proj C 0 射影を適用し、 カーネルは最大カーネル検査で通常の検査済み addDecl パスを通じて宣言を受理します。 その結果、公理を伴わない False の証明を生じる型混同が発生し、 そこから任意の命題 — 0 = 1 を含む — を導出できます。

このエクスプロイト:

• 検査済みの addDecl カーネルパスのみを使用
• --trust=0（最大検査）で実行
• #print axioms で公理なしを報告
• sorry、unsafeCast、debug.skipKernelTC、FFI、.olean の改ざんは不使用

使用法

docker build -t lean-cve-poc .
docker run --rm lean-cve-poc

脆弱な Lean バージョンでの期待される出力:

[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1

[!] VULNERABILITY CONFIRMED — CVE-2026-72844

    zero_eq_one : 0 = 1
    Depends on: no axioms

パッチ適用済みの Lean バージョンでは、カーネルは型不正な帰納的型を拒否し、スクリプトはそのバージョンが脆弱ではないと報告します。

影響

Lean のカーネル検査済み証明を正として信頼するすべてのシステムが影響を受けます。これには以下が含まれます:

• 形式検証ソフトウェア: コンパイラ、暗号ライブラリ、スマートコントラクト、航空電子機器、自動車 — 影響を受けるバージョンで構築された Lean 証明に基づくすべての安全性ケースは無効です。
• Proof-carrying code（証明運搬コード）: Lake パッケージ内の悪意のある依存関係は、下流のコードが使用する不健全な宣言を静かに導入する可能性があります。
• 独立型チェッカー: 同じ種類のバグが Nanoda 独立型チェッカーもバイパスすることが示されています。

技術的詳細

根本原因は、カーネルによるネスト帰納的型の処理にあります。 ネストした出現 I Ds is を除去するとき、カーネルはパラメトリック引数 Ds が帰納的型の宣言されたパラメータと一致することを検証する必要があります。 脆弱なコードは、Ds 内の射影式 (.proj) が正しい構造体名を参照していることをチェックできないため、w : W かつ W ≠ C の場合でも .proj C 0 w を受け入れてしまいます。

ハッシュ衝突（カーネルは定義上の等価性チェックで Expr.hash 比較を使用）と組み合わせることで、攻撃者はカーネルの内部型割り当てが実際の項の意味論と一致しない宣言を登録でき、型混同と False の証明につながります。

参照

• NVD: CVE-2026-72844
• VulnCheck アドバイザリ
• oss-security 開示
• Lean 4 issue #14576
• 修正 PR #14577
• 修正コミット

クレジット

• バグ発見と最小 PoC: @kiranandcode
• 元の CollatzLean エクスプロイト: @xrchz (Ramana Kumar)
• カーネル修正: Leonardo de Moura (PR #14577)
• CVE 申請と PoC パッケージング: Jonathan Brossard (@endrazine)