CVE-2026-72711

概要

Lean 4 カーネルは、opaque 宣言の本体が閉じていることを検査しない。environment::add_opaque は、definition および theorem の経路が実行する check_no_metavar_no_fvar 呼び出しを省略しているため、ローカルコンテキストに存在しない自由変数を含む値は即座には拒否されない。メタプログラムは、まずカーネルに型 False の一時ローカルを作成させ、その型を型チェッカーの推論キャッシュに記録させ、次に同じ型チェッカーインスタンス上でそのキャッシュエントリが残ったままローカルコンテキストを復元し、最後にその時点で未束縛となった変数を値とする opaque 宣言を提出することができる。キャッシュ参照はローカルコンテキストへの所属を検査する分岐より先に応答するため、カーネルはキャッシュされた型を推論し、型 False の opaque 定数を受理する。そこからは任意の命題が導かれる。この宣言は、最大カーネル検査設定において通常の検査済み経路を通じて受理され、sorry、unsafeCast、debug.skipKernelTC、addDeclWithoutChecking、外部コード、改変された .olean ファイルのいずれも用いず、その結果には公理が含まれない。この問題は、欠落していた閉包検査を追加することで 4.32.2 において修正された。

ソース

• lean-cve-poc-14484PoC

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