注目★★★★★Hacker News
Lean カーネルの健全性バグ #14576、ネストされた帰納型の型検査漏れで False の証明が可能に
30秒で把握
- 1Lean カーネル phantom パラメータ処理に型検査漏れ、メタプログラミング経由で False 証明が可能に
- 2カーネルと独立型検査器 nanoda に 2 つの異なるバグが同時に存在、修正までのタイムウィンドウで悪用可能だった
- 37 件の関連バグをすべて修正・kernel arena で回帰テスト追加・nanoda 日次追跡体制で再発防止
要約
Lean カーネルに型検査の脆弱性が発見され、7 月 28 日に修正された。バグは帰納型の phantom パラメータ (コンストラクタで使われない引数) が生成される補助型から消失し、型検査をすり抜けられる仕組みだった。メタプログラミング経由でのみ到達可能で、フロントエンドの検査は機能していたが、カーネル自体は不正な型付けの宣言を受け入れてしまった。同様のバグが他に 6 件見つかり、すべて修正済み。
あなたへの影響
Lean ユーザーで証明検証の安全性を重視するチームは、公開カーネル修正と nanoda 版の両方を最新に保つ必要があります。
推奨：メタプログラミング経由でのみ到達可能なため、通常の証明開発には直接的な影響は限定的ですが、形式検証システムの堅牢性向上は信頼性向上につながります。