CVE-2026-72844

概要

Lean 4 カーネルは、射影式で指定された構造体の名前が、投影される値の型と一致することを検証しません。また、`src/kernel/inductive.cpp` の `environment::add_inductive` は、補助型に置き換えられる入れ子の帰納的適用を型検査しなかったため、それらのパラメトリック引数が検査を逃れていました。Lean プロセス内で実行されるメタプログラムは、無関係な型 `W` の値に `.proj C 0` 射影を適用するコンストラクタを持つ、型が正しくない入れ子の帰納型を登録でき、カーネルは最大のカーネル検査設定において、`sorry`、`unsafeCast`、`debug.skipKernelTC`、`addDeclWithoutChecking`、FFI、または改変された `.olean` ファイルを一切使わずに、通常の checked `addDecl` パスを通じてその宣言を受理します。その結果、型の混乱が生じ、公理を一切伴わない `False` の証明が得られ、そこから任意の命題を導出できます。公開された概念実証ではさらに、ハッシュとおおよその深さが衝突するまで2つの式をパディングしており、これによりカーネルのキャッシュが無効化されます。これは欠陥に到達するために使われた手法であり、原因ではありません。悪用には、プロジェクトのビルドや悪意のある Lake 依存関係のインポートなど、プロセス内でメタプログラムを実行することが必要です。

• lean-cve-pocPoC

  CVE-2026-72844 : Lean 4 カーネルの脆弱性を利用して「0 = 1」を証明する例。