CVE-2026-72711 — Lean 4 カーネルの健全性バグ: 推論キャッシュポイズニング

不透明宣言の FVar キャッシュポイズニングにより、公理なしで 0 = 1 を証明する。

フィールド	値
バグ報告	leanprover/lean4#14484
修正	leanprover/lean4#14498
影響範囲	Lean 4 ≤ `v4.31.0` / 以前のすべてのバージョン
修正済み	nightly 2026-07-23+、v4.32.1 および v4.33.0 にバックポート
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session)、CWE-20 (Improper Input Validation)
CVE	CVE-2026-72711

脆弱性の概要

Lean 4 カーネルの environment::add_opaque パスは、宣言本体に対して check_no_metavar_no_fvar を呼び出していません。これは、値を型チェックする前にこのクロージャチェックを実行する定義や定理とは異なります。

悪意のあるメタプログラムは、この省略を 推論キャッシュポイズニング によって悪用します:

プライミング — 細工された型式 (cachePrimingType) は、False と定義上等しい閉じたベータ簡約式です。これを型チェックする際、カーネルは一時的なローカル宣言 _kernel_fresh.2 : False を作成し、その推論された型を type_checker インスタンスの推論キャッシュにキャッシュします。
コンテキストの無効化 — ローカルコンテキストは復元されます (一時変数は削除されます) が、推論キャッシュは同じ type_checker インスタンス上に残ります。キャッシュエントリは今や古くなっています — スコープ内の何も参照しなくなった識別子をマッピングしています。
悪用 — 不透明宣言の値は、古い識別子を指す Expr.fvar です。キャッシュ検索は、 FVar ブランチがローカルコンテキストのメンバーシップをチェックする前に発火し、未バインド変数を検出することなく False を型として返します。

その結果、カーネルに受け入れられた False 型の不透明定数が得られ、そこから 0 = 1 が自明に導かれます。

このエクスプロイトは:

チェック済み の addDecl カーネルパスのみを使用
--trust=0 (最大チェック) で実行
#print axioms で 公理なし を報告
sorry、unsafeCast、debug.skipKernelTC、FFI、.olean 改ざんを使用しない
leanchecker --fresh リプレイを通過

使用方法

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

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

[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms

    Bug class:  Inference cache poisoning (CWE-488)
    Root cause: missing check_no_metavar_no_fvar in add_opaque
    Bug report: https://github.com/leanprover/lean4/issues/14484
    Fix:        https://github.com/leanprover/lean4/pull/14498

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

影響

Leanのカーネル検証済み証明を絶対的な真実として信頼するあらゆるシステムが影響を受けます。これには以下が含まれます：

形式検証済みソフトウェア: コンパイラ、暗号ライブラリ、スマートコントラクト、アビオニクス、自動車 — Lean証明に基づいて構築された安全性の根拠は、影響を受けるバージョンで構築された場合、無効となります。
証明付きコード: Lakeパッケージ内の悪意ある依存関係が、下流のコードが使用する不健全な宣言を密かに導入する可能性があります。
独立したチェッカー: 報告者はleanchecker --freshによるリプレイもエクスプロイトを受け入れることを確認しました。comparatorエクスポート形式は FVarを表現できないため、その検証経路は影響を受けません。
AI生成の証明: AlphaProof、DeepSeek-Prover、Kimina-Proverなど、Leanを信頼されたバックエンドとして使用するシステムは、定理を証明するのではなくカーネルのバグを悪用する証明を生成する可能性があります。

技術的詳細

根本原因

src/kernel/environment.cppにおいて、add_opaque関数はopaque値の型をチェックしますが、クロージャチェックを実行しません：

environment environment::add_opaque(declaration const & d, bool check) const {
    scoped_diagnostics diag(*this, check);
    opaque_val const & v = d.to_opaque_val();
    if (check) {
        type_checker checker(*this, diag.get());
        check_constant_val(*this, v.to_constant_val(), checker);
        // ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
        expr val_type = checker.check(v.get_value(), v.get_lparams());
        // ...
    }
}

add_definition と add_theorem はどちらも、型チェックの前に値に対して check_no_metavar_no_fvar を呼び出します。add_opaque におけるこの省略がエントリーポイントとなります。

キャッシュポイズニングの仕組み

type_checker 内の推論キャッシュは、式をその推論された型にマッピングします。infer_type_core では、キャッシュの検索が次のようになります:

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

は、FVar ブランチがローカルコンテキストのメンバーシップを検証する前に発火します:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

攻撃者は型式を通じてキャッシュの生成を制御できるため、古いエントリの名前（_kernel_fresh.2）が予測可能になり、標的にできます。

#14576 との比較

観点	#14484（本バグ）	#14576
バグの種類	キャッシュポイズニング	射影検証による型混同
エントリポイント	`add_opaque` にクロージャチェックがない	ネストした帰納的ファントムパラメータ
関与するキャッシュ	あり — 推論キャッシュ	あり — 式ハッシュの比較
leanchecker への影響	あり	あり
comparator への影響	なし（FVar は表現不可）	あり

クレジット

バグの発見: Patrick Hulin (@phulin)、GPT-5.6 Sol の支援による
カーネルの修正: Joachim Breitner (@nomeata)、PR #14498
PoC のパッケージ化: Jonathan Brossard (@endrazine)

lean-cve-poc-14484

人気