ハクソク

世界を動かす技術を、日本語で。

Leanはこのプログラムが正しいことを証明したが、その後バグを見つけた

3日前原文(kirancodes.me)

概要

  • Leanによる形式検証済みプログラムでバグが発見された事例
  • AIエージェントやファジングによる脆弱性発見の進化と現状
  • 形式検証の限界と、検証範囲外のバグ発見の実例
  • LeanランタイムのバッファオーバーフローやDoS脆弱性の詳細
  • 形式検証の有効性と課題についての考察

Leanによる検証済みzlib実装にファジングを適用した事例

  • **Leanで形式検証されたzlib実装（lean-zip）**を対象にAIエージェント（Claude）とファジングツール（AFL++、AddressSanitizer、Valgrind、UBSan）を適用
  • 105,823,818回のファジング実行により、アプリケーションコード自体にはメモリ脆弱性がゼロであることを確認
  • しかし、Leanランタイム（lean_alloc_sarray）にバッファオーバーフローを発見
  • lean-zipのアーカイブパーサー部分にDoS脆弱性（大容量メモリ割当によるOOM）も発見
  • 検証対象外の部分にバグが集中し、検証範囲内は非常に堅牢であったことを実証

ファジング実験のセットアップと手法

  • lean-zipコードベースから定理や仕様・C FFIバインディング・ドキュメントを除去し、純粋に検証済み部分のみを対象
  • CLI経由でファジング対象を操作し、AIエージェントがバイアスなくコードを解析
  • **6つの攻撃面（ZIP抽出、gzip展開、DEFLATE展開、tar抽出、tar.gz、圧縮）**を用意
  • AddressSanitizer、UBSan、Valgrind、cppcheck、flawfinderによる多角的な静的・動的解析
  • 既知のzlib CVEパターンを模した48種の手書きエクスプロイトファイルも投入

発見されたバグの詳細

  • バグ1：Leanランタイムのバッファオーバーフロー

    • lean_alloc_sarray関数で容量計算時のオーバーフローが発生
    • **SIZE_MAX（2の64乗-1）**を指定すると小さいバッファが割り当てられ、nバイト読み込みでオーバーフロー
    • 全Lean 4バージョンに影響、再現コード5行で容易に発生
    • PRにて修正予定

  • バグ2：lean-zipのアーカイブパーサーにおけるDoS

    • ZIPヘッダのcompressedSizeフィールドを検証せずにメモリ割当
    • 巨大な値を指定するとプロセスがOOMでパニック
    • 他のunzip実装では適切な検証があるが、lean-zipでは未検証
    • この部分は形式検証の対象外

形式検証の限界と有効性

  • DoS脆弱性は検証未実施領域（アーカイブパーサー）で発生
    • lean-zipの証明範囲は圧縮・展開処理のみ
    • ヘッダ解析やファイル抽出処理は未検証
  • ランタイムのバッファオーバーフローは信頼基盤の問題
    • Leanの全証明はランタイムの正しさに依存
    • ランタイムのバグは全Leanアプリに波及
  • 形式検証が適用された範囲ではC/C++実装に比べて極めて高い堅牢性
    • ヒープ・スタックバッファオーバーフロー、use-after-free、未定義動作ゼロ
    • CVEクラスの脆弱性が構造的に発生しない

まとめと考察

  • 形式検証は適用した範囲で圧倒的な堅牢性を実現
  • 検証範囲外や信頼基盤（ランタイム）のバグは防げない
  • 検証の強さは「どこまで・何を」問うかと「信頼する基盤」に依存
  • AIやファジングの進化により、従来のソフトウェアは脆弱性発見コストが劇的に低下
  • 今後のソフトウェア開発には形式検証の適用範囲拡大と、信頼基盤の再検証が必須

形式検証時代の課題と展望

  • 形式検証済みコードの安全性は高いが、全体の安全性は信頼基盤・検証範囲次第
    • trusted computing base（TCB）の最小化と検証拡大が重要課題
  • AIや自動化ツールによる脆弱性発見能力の向上
    • 「Quis custodiet ipsos custodes?（誰が監視者を監視するのか）」という根本的問い
  • 今後は形式検証＋AIファジングの組み合わせが主流となる可能性
    • 形式検証の証明範囲・信頼基盤の明確化と継続的な再検証が求められる時代

Hackerたちの意見

私も似たような経験があるよ。自分が正しいと証明したコードでも、問題が起きることがあるんだ。特に、オーバーフローの問題よりも一般的な、微妙な仕様のバグが多いかな。投稿では、サービス拒否の問題がこれに関連しているって言ってるね。正しくない仕様があると、その仕様に従ったコードを書くことはできるし、それをサポートする証明も書ける。でも、それはあなたが意図したこととは違う動作をするプログラムを検証したってことになる。これが検証の難しい部分の一つで、人間としての意図を明確に表現することなんだ。プログラムが複雑になるほど、これを書くのが難しくなるから、leanやrocqの証明がうまくいかないこともよくある。何度かこれを経験すると、leanやrocqのツールを効果的に使うのが難しいって気づくよ。「証明支援ツールがAIの正しさを保証する」っていうのは、もし人間の意図を捉えた仕様がしっかり見直されないと、誤った安心感を生むんじゃないかと心配してる。そうじゃないと、仕様の欠陥で人間が実際に意図したコードとは違うコードの証明がたくさんできちゃうよ。
└
私も似たようなことを経験したことがある！でも、証明が問題だとは言えないよ。通常、leanや他の証明器、例えばTLA+やZ3を使って合理的に証明できる仕様は、過度に単純化されていて多くの仮定が必要なんだ。でも、それは強力だよ。プログラムにバグがないってことじゃなくて、あなたがうまくいくと思っている複雑なアルゴリズムにはバグがないってこと。だから、バグに遭遇したときは、実際の原因がどこにあるのかを探し始める。仮定が本当に正しいのか、仕様が間違っている可能性がある境界を見直すことになるんだ。これが最近、私にとって非常に価値があることになった。AIの助けがなければ、こういうことはできなかったと思う。プログラムに関する証明を雰囲気でコーディングするのは、AIの素晴らしいアプリの一つだと思う。まだうまくやるためのリソースがあまりないからね。
└
最近これについてずっと考えてる。仕様を検証する方法が必要だと思う。形式論理と対抗的思考（多分LLMから来てる）を組み合わせて、プログラムが何をするか、何をしないか、何が不明確かを網羅的にリストアップするんだ。まだ具体的なイメージは掴めてないけど、プログラム生成が証明可能だと仮定すれば、正しさの課題は仕様に移る（それを解決すれば、要件にまで押し上げられる…）。
└
形式検証システムについての記事を読むたびに、頭の中にいつも引っかかる考えがある。なんで自分の形式検証システムはバグがないと信じられるのに、プログラムは信じられないんだろう？ 両者のバグの可能性は同じくらいであるべきじゃない？ 何かをするプログラムがあって、それを証明するための別のプログラムを書く。どちらのプログラムがバグが少ないか、どうやって保証するの？ なんで一方のプログラムにはバグがあって、もう一方にはないの？ 正しいことを証明しているってどうやって証明するの？ これはハイゼンベルグの不確定性原理にもつながる。システムはそのシステム内から完全には説明できない。誤解しないでほしいけど、これらは素晴らしいシステムで素晴らしい仕事をしてると思う。でも、いつも物語に何かが欠けている気がする。もっと実用的な見方をすると、プログラムはすでに一種の証明なんだ。解決すべき何かがあって、プログラムがそれを証明するメカニズムを提供している。でもこの証明は間違っている可能性が高いし、バグが修正されるにつれてどんどん正確になっていく。正しさを強制しようとする強力だけど時間のかかる手法は、異なるメカニズムを使ってマシンを二回構築することだ。そうすれば、不一致の出力がどちらかに問題があることを示す。エンジニアとしての仕事は、どちらに問題があるかを見つけることなんだ。これが形式検証がもたらすもの、つまり第二のメカニズムだよ。
記事を読み間違えてるかな？著者は証明の主張をテストしていないみたいだね。この場合の「バグ」って、圧縮アルゴリズムを通過したときに生き残らなかった入力を見つけたってことじゃないの？アップデート：実際、これが彼女の言いたかったことかも。「見つかった二つのバグは、証明がカバーする範囲の外にあった。」だから、タイトルはちょっとクリックベイトっぽいかもね。
└
こんにちは！著者です。検証されたソフトウェアシステムのバグについて話すとき、全体のバイナリを対象にするのは公平だと思う。バッファオーバーフローが原因でシステムが悪用されて、ビットコインが盗まれたら、バグが言語のランタイムにあるってことはあまり慰めにならないと思う。特に、実行していたソフトウェアがバグがないと正式に検証されていると宣伝されていた場合はね。さらに、私はアルゴリズムの中にバグを見つけたよ。Archive.leanの圧縮アーカイブヘッダーのパースにおいて、それがクラッシュの原因になった入力だった。
パーサーを検証しないのはかなりの見落としだと思う。バイナリフォーマットのパースは危険すぎるからね！
この記事の枠組みとタイトルは変だね。著者は、実際には証明されたコードにバグやエラーを見つけていないって言ってる。記事の最後でこう言ってるよ：> 見つかった二つのバグは、証明がカバーする範囲の外にあった。サービス拒否は仕様の欠如によるもので、ヒープオーバーフローは信頼できるコンピューティングベース、つまり全体の証明が正しいと仮定しているC++ランタイムの深い問題だった。それでも、Leanランタイムでバグを見つけるのは興味深くて有用な結果だけど、タイトルを正当化するものではないと思う。「全体の証明構造」が不安定だという主張も同様に。これはバグがあるのはLeanランタイムであって、実際に検証を行うLeanカーネルではないってことを強調するのが重要だよ。[1] だから、このバグが本当に何に適用されるのかは明確じゃない。だって、誰もコンパイルされたLeanコードを本番環境で実行しているわけじゃないから。[1] https://lean-lang.org/doc/reference/latest/Elaboration-and-C...
└
繰り返しになるけど、検証されたソフトウェアシステムのバグについて話すとき、全体のバイナリを対象にするのは公平だと思う。バッファオーバーフローが原因でシステムが悪用されてビットコインが盗まれたら、バグが言語のランタイムにあるってことはあまり慰めにならないと思う。特に、実行していたソフトウェアが正式にバグがないと検証されていた場合はね。次に、コードにはバグがあった。機能的な正しさのバグではないかもしれないけど、私や多くのエンドユーザーにとって、クラッシュするプログラムはバグがあると見なされるだろう。もしかしたら、私たちのソフトウェアの品質に対する基準が違うだけかもしれない。Leanを本番環境で使っている人たちについては、驚くかもしれないけど…
└
このサイトの記事リスト、面白いと思ったよ：https://kirancodes.me/posts/log-who-watches-the-watchers.htm... 時間が経つにつれてクリックベイト感が増してるのがわかる。
└
俺にとって、リーンランタイムにバグがあるって言うのは、リーンZIPにバグがあるってことと同じで、JREにバグがあるからってJavaアプリにバグがあるわけじゃないのと同じだと思う。Javaアプリのコード自体にはバグがあるのにね。著者が自分の発見についてわざと誤解を招くようなことを言ってる気がする。
└
> このバグがあるのはリーンランタイムであって、実際に検証（証明）を行うリーンカーネルではないってことは重要だよ。[1] だから、このバグが実際に何に適用されるのかもすぐにはわからない。まあ、リーンはリーンで書かれているから、こういうランタイムバグが`False`を証明するために悪用される可能性は高いと思う。カーネルはC++で書かれているから、技術的にはこのバグの影響を受ける部分ではないけど、リーンコンパイラなしではリーンカーネルを使えないから、この違いはあまり関係ないよね。
└
うん、タイトルを見て著者がリーンカーネルにバグを見つけたのかと思ったよ。無効な証明がリーンのチェックを通過するってことになるからね。記事はリーンランタイムとリーンZIPのバグを明らかにしてるけど、これらのバグはカーネルのように信頼されるべきものとは比べ物にならないよ。カーネルが正しいと信じられないと、リーンの証明も信じられなくなるからね。
└
> 明らかに誰もコンパイルされたリーンコードを生産環境のホットパスで実行していない。 無知な質問だけど、なんで？ 受け入れられないパフォーマンスペナルティがあるの？ その場合、同じ保証を保ちながら生産環境で証明されたリーンコードを使うための推奨方法は何？
「上記のコードにはバグに注意せよ。私はそれが正しいと証明しただけで、試してはいない。」 -- ドナルド・クヌース
クリックベイトなタイトルだね。プログラムの証明部分にはバグがなかったの？ それにしても、なんで人は事実に基づいて書けないんだろう？ ここは広告収入を狙ったニュースサイトじゃないのに。もっと簡単なのにね。この投稿は大体、侮辱的な時間の無駄だと感じた。HNには面白いことを読みに来てるんだ。
└
うん、技術的には意味的に正しいとしても、非常に誤解を招くタイトルだね。表現が、証明の境界の一部として`lean-zip`にバグが見つかった印象を与えてるけど、実際は検証されていないアーカイブ処理コードの一部なんだ。
└
形式的に検証されたソフトウェアについて、証明を違反するバグだけを考慮して、他のすべてを無視するのは公平なのかな？ 形式的に検証されたソフトウェアは「見て、バグがない！」って宣伝されるけど、「見て、バグがない*」ってわけじゃない。* この複雑な補題の連鎖が、私たちが気にするすべての正しさを適切に表現している限り。ボートの世界では、特定の状況での優先権ルールについてよく議論があるけど、巨大なタンカー船が小さな帆船に道を譲るべきだと指摘する人が多くて、みんなそれに熱くなるよね。聞いた中で一番良い答えは：彼らは完全に正しい！ つまり、彼らが死んでいるのと同じくらい正しい（譲らなかったら）笑。同じように、形式的に検証されたソフトウェアが完璧だと仮定してハッキングされたりしたら、その人はちょっと不安になるだろうね。* = 技術的には、ルールは「操縦能力が制限されている」場合、タンカーを優先するけど、みんなそれについて議論するのが好きなんだ。
みんな、木を見て森を見失ってるよ。AIエージェントを使ってアイデアをファジングに送って、Leanでヒープバッファオーバーフローを発見したんだ。これは大きなニュースだよ。
└
確かにこれは素晴らしい発見だし、自体としても役に立つと思うよ。
ここでの仕様完全性の問題は、分散システムの検証でも同じように悩まされる：証明は運用範囲内で成立する（対抗的入力なし、信頼できるランタイム、サイズ制限あり）、そして興味深い失敗は境界に存在する。TLA+も同じ特性を持っていて、デプロイメントが静かに違反している公平性の仮定の下で生存性を証明できるけど、証明の中には現実がいつ外れたかを教えてくれるものはない。実際にツールから欲しいのは、そのエンベロープ自体の機械検証可能な記述で、それをコンパイル時のコメントではなくランタイムガードとして伝播させること。そうすれば、「証明が成立する」と「まだ証明の範囲内にいる」というのは、別々の観察可能な特性になって、未検証のパーサーや未検証のランタイムのケースが見えなくなることはなくなる。
└
以前、チップベンダーには知られていなかったCPUのバグを発見した者として、深い穴にハマることになるってことを指摘したい。逆に、ハードウェアバグではないバグを何千も発見したし、ハードウェアのエラッタ文書を読んでいない人たちによるバグも何十もあったから、我々がモデル化できるものを正式にモデル化するだけで、バグの数は驚くほど減るよ。
圧縮/解凍は、正しさの証明にとって良い問題だよね。仕様はすごくシンプル（入れたものがそのまま戻ってくるべき）だけど、実装は複雑なんだ。ここで起こったことは、下のストレージアロケータが未検証ってことみたい。これも比較的シンプルな仕様があるんだけどね - すべてのバッファは独立していて、バッファが失われることもなく、クラッシュもない。
こういうツール（形式的検証、スパースなど）や組み込みメカニズム（型、ジェネリクス、RAII、Rustの借用チェッカー）は、そのフレームワークの範囲内でしか問題を検証できないんだ。それぞれの型や実装にはトレードオフや制限もあるしね。型チェックを使うことで、オブジェクトが特定の型であることを確認できる（C/C++のような型キャスティングやJavaのジェネリックコンテナのオブジェクトへのキャスティングを除いて）。これによって、きちんとしたプログラムがランダムなオブジェクトをリストに入れたりすることがないって確信できる。C#やScala、Kotlinのような言語は、コンテナや他のインターフェース/型のジェネリック型を型システムの一部にすることでJavaのジェネリクスを改善している。これにより、ジェネリック型のジェネリック型が内部の型を保持できるようになる。モナドやマッピング関数を実装してジェネリック型を保持することも可能になる。ユニオン型やシールドインターフェース/トレイトなどでも同様のことが可能で、戻り値の型をチェックして検証できるようになる。デフォルトでジェネリックオブジェクト/任意の型にしないで済むからね。同様に、nullable/non-nullアノテーション（Kotlinや最近のC#バージョンのnullable型アノテーションなど）などの他の機能でも同じことが言える。これらは悪用されたり回避されたりすることもあるけど、フレームワーク内でコードを保てば、コンパイラがそのコードのコンパイルを止めてくれる。こういうのは限られたバグを解決するけど、例えばnullable型ではメモリ管理や関連するバグを検証できない。