Leanがプログラムの正しさを証明したが、その内部でバグが見つかる
(kirancodes.me)- 形式検証済みの zlib 実装をファジングした結果、Lean 4 ランタイムの
lean_alloc_sarrayで ヒープバッファオーバーフロー が発見された - AI ファザー Claude、AFL++、AddressSanitizer などを用いて1億回以上テストした末に、4件のクラッシュと1件のメモリ脆弱性 が確認された
- 見つかった問題は、ランタイムオーバーフロー と
Archive.leanの Out-of-Memory ベースのサービス拒否（DoS） の2種類に分けられる - 検証済みの圧縮・展開アルゴリズムは安全だったが、検証されていないアーカイブパーサーとランタイム層 に脆弱性が存在した
- 結果として形式検証は強力だが、信頼基盤計算ベース（TCB） の安全性が確保されなければ、システム全体の安定性を保証することはできない
Lean の検証を通過したプログラムで見つかったバグ
- Lean で形式検証された zlib 実装をファジングした結果、Lean 4 ランタイムで ヒープバッファオーバーフロー が発見された
- 検証済みのアプリケーションコードにはメモリ脆弱性はなかった
- しかし Lean ランタイムの
lean_alloc_sarray関数でオーバーフローが発生し、すべての Lean 4 バージョンに影響する
- AI ベースのファザー Claude、AFL++、AddressSanitizer、Valgrind、UBSan などを利用して1億回以上のファジングを実施
lean-zipの圧縮・展開・アーカイブ処理など6つの攻撃面を対象に16個の並列ファザーを稼働- 19時間で4件のクラッシュ入力と1件のメモリ脆弱性が見つかった
- 2つの主要なバグ が確認された
- Lean ランタイムの
lean_alloc_sarrayにおける ヒープバッファオーバーフロー lean-zipのArchive.leanモジュールにおける Out-of-Memory ベースのサービス拒否（DoS）
- Lean ランタイムの
- 形式検証の限界 が明らかになった
lean-zipの圧縮・展開アルゴリズムは完全に検証されていたが、アーカイブパーサー (Archive.lean) は検証されておらず、DoS 脆弱性が存在した- ランタイムバグは 信頼基盤計算ベース（Trusted Computing Base） 内部の問題であり、すべての Lean プログラムに影響する
- 結論として、Lean の形式検証はアプリケーションコードの安定性を証明したが、検証範囲外の構成要素 には依然として脆弱性が存在する
- 検証は適用された範囲内でのみ強力であり、基盤となる信頼層の安全性確保 が不可欠である
ファジング実験の概要
- 対象コードベース は
lean-zipの検証済み zlib 実装- すべての定理 (theorem) と仕様 (specification)、ドキュメント、C FFI バインディングを削除し、純粋な Lean コードのみを残した
- Claude がコードが検証済みである事実を認識できないようにしてバイアスを防いだ
-
実験環境
- 16個の並列ファザーが ZIP、gzip、DEFLATE、tar、tar.gz、compression という6つの攻撃面を対象に実行
- AddressSanitizer、UndefinedBehaviorSanitizer、Valgrind memcheck、cppcheck、flawfinder などを併用
- 48個の手作業エクスプロイトファイルを含め、合計 105,823,818回実行、359個のシードファイルを使用
- 19時間で4件のクラッシュ入力と1件のメモリ脆弱性が発見された
バグ1: Lean ランタイムのヒープバッファオーバーフロー
- 脆弱な関数:
lean_alloc_sarray- すべての
ByteArray、FloatArrayなどのスカラー配列を割り当てる関数 sizeof(lean_sarray_object) + elem_size * capacityの計算時に 整数オーバーフロー が発生する可能性がある
- すべての
-
問題の原因
capacityがSIZE_MAXに近い場合、加算がオーバーフローして小さなバッファが割り当てられる- その後、呼び出し側が
nバイトを読み込み、ヒープバッファオーバーフロー が発生する
-
トリガー条件
lean_io_prim_handle_readでnbytesが非常に大きい値のときに発生- ZIP64 ヘッダーの
compressedSizeが0xFFFFFFFFFFFFFFFFである156バイトのファイルで再現可能 - Lean 4 のすべてのバージョン（最新 nightly を含む）に影響
- 再現コード例
def main : IO Unit := do IO.FS.writeFile "test.bin" "hello" let h ← IO.FS.Handle.mk "test.bin" .read let n : USize := (0 : USize) - (1 : USize) let _ ← h.read n- 上記コードを実行すると
lean_alloc_sarrayでオーバーフローが発生する - 修正 PR が提出されている
バグ2: lean-zip アーカイブパーサーのサービス拒否（DoS）
- 脆弱な関数:
readExact(Archive.lean)- ZIP 中央ディレクトリの
compressedSizeフィールドを検証なしにそのまま使用 h.read呼び出し時に異常に大きなサイズを要求し、過剰なメモリ割り当てと OOM 発生 を引き起こす
- ZIP 中央ディレクトリの
-
問題の再現
- 156バイトの ZIP ファイルが数エクサバイト級のサイズを主張すると、
INTERNAL PANIC: out of memoryでプロセスが終了する - システムの
unzipはヘッダーサイズを検証するが、lean-zipはこれを行わない
- 156バイトの ZIP ファイルが数エクサバイト級のサイズを主張すると、
形式検証が見落とした部分
-
DoS 脆弱性の原因
Archive.leanモジュールは未検証の領域- 圧縮・展開パイプライン（例: DEFLATE、Huffman、CRC32）は完全に検証されており問題はない
- 検証が適用されていない部分で脆弱性が発生
-
ランタイムオーバーフローの本質
- Lean ランタイムは 信頼基盤計算ベース（TCB） に属する
- すべての Lean の証明はランタイムの正しさを前提としている
- したがってランタイムバグは、すべての Lean プログラムの安全性に影響する
検証済みコードの安定性
-
1億500万回超の実行結果
- Lean が生成した C コードでは ヒープオーバーフロー、use-after-free、スタックオーバーフロー、UB、配列境界超過 はいずれもなかった
- Claude の評価によれば、最もメモリ安全なコードベースの1つ と分析された
-
Lean の型システムの効果
- 依存型 (dependent types) と well-founded 再帰 の構造により、 C/C++ ベースの zlib 実装で一般的な脆弱性（CVE クラス）を構造的に防いでいる
-
結論
- 検証済みコード領域は非常に堅牢で、ファザーがエラーを見つけるのは難しかった
- しかし未検証の部分とランタイム層には依然として脆弱性が存在する
- 検証は適用範囲と信頼基盤の安全性によって制約される
核心的な教訓
- 形式検証は 適用されたコード領域内では非常に強力 だが、 未検証の周辺コンポーネントやランタイム層 が全体の安定性を脅かす可能性がある
- 信頼基盤計算ベースの安全性確保 が必須であり、 検証済みシステムであっても「誰が監視者を監視するのか（Quis custodiet ipsos custodes）」という問いは残る
1件のコメント
Hacker Newsのコメント
この記事のタイトルとフレーミングは少しおかしいと感じた
実際、著者自身が証明済みコードの中ではバグや不具合は見つからなかったと明記している
見つかった2つのバグは証明の範囲外にあり、1つは仕様の欠落、もう1つはC++ランタイムのヒープオーバーフローだった
バグが見つかったのはLeanのランタイムであって、検証を行うカーネルではないことを強調したい
Leanドキュメントへのリンク を参照
バッファオーバーフローでビットコインを失ったとしたら、そのバグがランタイムにあったという事実は慰めにならない
また、プログラムがクラッシュするなら、ほとんどのユーザーはそれをバグだとみなすだろう
Leanを実際の本番環境で動かしている人もかなりいるはずだ
カーネルでないなら、証明そのものの信頼性には大きな影響はない
「Hello world」プログラムを検証するにしても、出力だけでなく副作用まで仕様化しなければならない
ランタイムとカーネルの境界でメモリ破損が起きるなら、証明の信頼性は下がりうる
結局のところ、何を検証すべきかを明確に定義することが核心だ
関連記事一覧
著者は意図的に誤解を誘っているように見える
私も証明済みコードで似たような経験をしたことがある
私の場合、オーバーフローよりも仕様の欠陥(spec bug) が問題だった
仕様が間違っていれば、コードと証明が完璧でも意図した動作とは違う結果になる
結局、検証の難しさは人間の意図を正確に表現することにある
AIが検証を完全に解決してくれるという信念は、誤った確信を与えかねない
Lean、TLA+、Z3のようなツールで証明可能な仕様は単純化されていて、多くの仮定が必要だ
それでもこれは強力なツールだ
複雑なアルゴリズムのバグを絞り込み、仕様の境界を明確に見えるようにしてくれる
AIのおかげで、こうした証明作業はずっと簡単になった
プログラムを検証する別のプログラムにも、結局はバグがありうる
完全な自己検証は不可能だという点で、ハイゼンベルクの不確定性原理を思い出させる
結局、検証とは「第二の独立した実装」によって信頼度を高めるプロセスだ
(1) 意図した動作と違う動きをする場合
(2) 意図どおりに動くが、その意図自体が間違っている場合
証明支援系は(1)は防げるが、(2)は防げない
つまり、設計の健全性は証明できない
seL4のようにすべてを検証するのは、あまりに高コストで時間もかかる
形式論理 + 敵対的思考(adversarial thinking) を組み合わせて、プログラムがすべきことと、してはいけないことを完全に列挙するやり方が理想的だ
タイトルがクリックベイトのように感じられた
証明された部分にはバグがないのに、なぜこう書いたのかわからない
HNでは事実に基づく投稿を読みたいのであって、これは時間の無駄だった
「バグなし」と宣伝していても、実際には「仕様が完全に表現された範囲内でのみ」だ
完全に正しくても、現実では正しいまま死ぬことがありうる — つまり、理論上は正しくても実際には壊れうる
コード参照もなく、実際のコードを見れば誤解だとわかる
この問題は分散システムの検証でもよく現れる
証明は特定の条件（運用範囲）の中でのみ有効で、面白い故障はその境界で起こる
TLA+も同様で、現実が仮定から外れれば証明は無意味になる
私が欲しいのは、運用範囲を機械的に明示し、ランタイムでそれを監視する機能だ
しかし、ほとんどのバグはハードウェアではなく、人が文書を読まないことから生じる
形式モデリングだけでも、バグの数は大幅に減らせる
これは予想可能な良いニュースだ
LLMが形式検証を通るコードを作れるという意味だからだ
今後はバグがますますハードウェア層へ移っていくだろう
最終的にはハードウェア仕様の形式化が必要になるはずだ
メーカーがそれを公開しなければ、コミュニティとの対立が起きるかもしれない
長期的には、脆弱性の絶滅か意図的な挿入かという二つの方向に分かれるだろう
最初は著者が証明済み部分をテストしていなかったのかと思った
だが読んでいくと、バグは証明の範囲外で見つかったものだった
なので、タイトルはやや誇張した表現に感じられた
検証済みシステムのバグなら、対象はシステム全体のバイナリであるべきだと主張している
実際にArchive.leanの圧縮ヘッダ解析部分でクラッシュを起こす入力を見つけたと述べている
Donald Knuthの有名な言葉を思い出した
「上のコードにはバグがあるかもしれないので注意せよ。私はそれが正しいと証明しただけで、実行してはいない」という警告だ
パーサを検証していないことは大きなミスに見える
バイナリ形式の解析は常に危険な領域だ
要点は、AIエージェントがfuzzerと協調してLeanでヒープバッファオーバーフローを発見したということだ
これはかなり大きな成果だ
Claudeが「これは私が分析したコードの中でも最もメモリ安全なコードベースの一つだ」と言っていた部分が印象的だった
ただ、これではClaudeが初めて分析したコードであるかのような冗談にも聞こえる
彼がこれほどうまくやれる理由は、まさにそこにある