機械語に「落ちない」の証明が付いた、123ライブラリ239入口 — 条件は単一スレッド・静的リンク・RISC-V・64MB未満である

Anthropic の Frontier Red Team が10月22日、Claude に形式検証の証明を書かせた結果を公開した。 協力は形式検証の企業 Theorem である^[1]。 Google の OSS-Fuzz に登録されたオープンソース123ライブラリ・239の入口について、 64MB未満の任意の入力に対してクラッシュせず正常に終了することを、RISC-V の機械語の水準で証明した^[1]。 総量は約1億8,000万行の Rocq コードである^[1]。 形式検証は歴史的に、seL4 カーネルの実装2人年に対し検証20人年という代物で、 だから航空機の航法コードのような極小の領域にしか使えなかった^[1]。 本紙がこれを取るのは、証明の対象がコンパイル後の機械語であること—— つまりコードベースを別の言語で書き直さずに済むこと^[1]——が、 止められない機械を持っている側に、初めて現実的な選択肢の形で出てきたからである。 ただし証明が成立する条件は単一スレッド・静的リンク・固定メモリ予算・RISC-V・Linux であり^[1]、 証明されているのは「正常に終了する」ことである^[1]。制御ループは終了しない。

証明されたのは「仕様を満たすこと」であって「バグが無いこと」ではない#

用語を先に固定する。形式検証では、コードを数学的なモデルに翻訳し、 それが定められた規則に常に従うことを証明しようとする^[1]。 証明に失敗すれば、規則を破るバグがそこにありうるということで、 失敗の様態がバグの形を示す。これを繰り返せば、 最終的にその規則を破るバグが1つも無いという証明が得られる^[1]。

難所は規則のほうである。「正しい」が何を意味するかは仕様が決める。 PNG デコーダなら RFC 2083 に沿って画像を復元すればよいが、 テキストエディタやブラウザが「正しい」とは何なのかは自明でない。 包括的で曖昧でない仕様を得る難しさが、形式検証を大規模化する最大の障害だったと 発表本文は書いている^[1]。

今回の回避の仕方が、この発表の核である。既存のファズテストを仕様に変換した^[1]。 ファズテストは、開発者が自分のコードへの入口を書き、 そこでクラッシュする入力があればそれは作者が気にするバグである、という形の試験である^[1]。 ファザーは半ランダムな入力を膨大に生成して当たりを探すが、 これは原理的に総当たりで、どれだけ入力を試してもすべての経路を通る保証はない^[1]。 そこで発表側は「このファズテストは64MB未満のあらゆる入力で落ちない」という 一文を、コンパイル後の RISC-V 命令列の上の仕様として立てた^[1]。 これが証明できれば、その入口をファジングしてもバグは二度と見つからない—— つまり RISC-V 上のそのファズテストは不要になる^[1]。

OSS-Fuzz を選んだ理由も明快である。OSS-Fuzz には開発者が書いた入口が数千件あり、 C / C++ のプログラムは AddressSanitizer で自動的に計装されていて、 メモリを不正に触った瞬間にクラッシュする^[1]。 メモリ安全性のような広域の仕様は、ほとんどすべてのソフトウェアに当てはまる^[1]。 つまり、仕様を人が書かずに済む入口が最初から大量に積んである場所だった。

公表された規模の数字#

1億8,000万行のうち、人が読む必要はほぼ無いとされる。Rocq の証明検査器が、 その証明が仕様を満たしていることを保証するからである^[1]。 結果として、開発者が信用しなければならないのは上の表の3種だけになる^[1]。 脚注はそこにもう一段を付けている。Rocq の証明検査器が依存している ハードウェア・OS・OCaml コンパイラも、技術的には信用の対象に入る^[1]。

この構図を発表本文はこう言い換えている。証明が通ったライブラリにバグが無いのではない。 残っているバグは上の3種の中にあるか、証明の範囲外にあるかのどちらかである^[1]。 そしてその3種を固めるのは容易ではないが、 証明が覆う全部のコードを1行ずつ追うよりはずっと扱いやすい作業である。 信用の対象の大きさを増やさずに、任意の数のプロジェクトを守れるからである^[1]。

前提——証明が成り立つ機械は、実際に動かしている機械ではない#

発表本文は限界の節を自分で立てている。順に表にする。 「形式検証済み」は「バグが無い」ではない、という一文から始まっている^[1]。 証明検査器は、証明が仕様を満たすかは言えるが、仕様が現実と合っているかは言えない^[1]。

公開の仕方にも但し書きがある。公開されるのは、パッチを必要としなかったファズテストについての完全な Rocq 証明と、 証明できなかったファズテストの仕様である^[1]。 未修整のバグを露出しうる証明は公開されない^[1]。 つまり「証明できなかった入口が存在する」ことは発表側が明示している。

見つかったバグは、ファザーが構造的に見つけにくい形のものだった#

証明を試みる過程で数百件のバグが出た^[1]。 発表本文が挙げている具体例は、どれも入力の大きさか呼び出しの順序に偏っている。

ファザーは小さい入力を変異させ、通常1MB程度で打ち止めにし、 コードカバレッジを頼りに進む^[1]。 20MBの稀な配置や、2GBのメモリを要する64MBの入力は、その探索の外側にある。 発表本文の冒頭は、これらのバグが何兆回の試験実行をもってしても長年検出を免れてきたと書いている^[1]。

クラッシュしない証明が、クラッシュの話に留まらない点も押さえておく。 現実のファズテストは、符号化と復号の往復一致、冪等性、代数法則、 差分試験、自己整合性、参照実装との一致といった高水準の性質を検査していることが多く、 性質が破れればプログラムが落ちる形で書かれている^[1]。 たとえば LZO 圧縮のファズテストは、圧縮して展開した結果が元と同じであることを主張する。 だから落ちないことの証明は、その性質自体の証明と等価になる^[1]。 開発者が明示していない性質にも及ぶ。cpp-httplib の証明を完成させるには、 std::set のデストラクタの再帰によるスタックオーバーフローを排除する必要があり、 Claude は libc++ の赤黒木の再平衡が木の深さを対数的に抑えることを機械語の上で証明しなければならなかった^[1]。

別の手法での事例——x86 の意味論を書かせたら、公式文書の誤りが数百件出た#

発表本文は、ファズテストを証明に変える以外の試みも並べている。 1つは zlib である。Claude に RFC 1950 の形式仕様を書かせ、 Linux カーネルの zlib 実装がその仕様を正しく実装していることを証明させた^[1]。 ここでは RISC-V ではなく、Claude が生成した x86 の意味論を使って x86 バイナリを直接証明している^[1]。 同じ工程を他の広く使われているライブラリ半ダースほどに繰り返し、 隅のほうに軽微な(悪用できない)バグをいくつか見つけて上流に報告中だという^[1]。 発表側の結論は2つ。(1) これら極めてよく試験されたコードベースは既にほぼ完全に正しい、 (2) 実在のコードベースについて端から端までの正しさを証明することは可能である^[1]。

この x86 の意味論について、脚注が本紙にとって最も重い事実を書いている。 意味論が完全である保証はできないが、経験的には、その意味論を1命令ずつ辿ることで Linux カーネルの上に Ubuntu のユーザ空間を起動できたという^[1]。 そして意味論を生成する過程で、公式の参照文書の誤りが数百件と、 それより少数のハードウェア自体のバグが見つかった^[1]。

残り2件も記録しておく。Rust で Python の大きな部分集合のインタプリタを書かせ、 学術論文に書かれた CPython の意味論に従うことを Verus で証明させたうえで、 170万本のランダムな Python プログラムで実測したところ、 CPython と同一の挙動が99.95%だった(残りは既知の隅の場合)^[1]。 もう1件は、広く使われている重要なアプリケーション数件に単純な安全性の性質の検証を試みたもので、 1件では10年以上潜在していた未知の論理バグが出た。 広く使われている PDF ビューアの検証では、通常1年に報告される件数と同じだけのバグが1週間で出た^[1]。

費用は下がる方向にある——が、桁は億トークンである#

費用効率が決定的だと発表側は書き、下がると見る理由を2つ挙げている^[1]。 以下は本文および図の説明文に書かれた数値である。

再利用が効く理由は、証明の中身の偏りにある。 証明の大部分は、どのプログラムにも入っている部分——とくに C ランタイムの初期化と AddressSanitizer——を扱っており、まったく違うプログラムの証明が大きく重なる^[1]。 OSS-Fuzz の本番でも、エージェントの班は他班の完成した証明を複製して 自分のプログラムに合わせる形で進めた^[1]。 発表本文は、Lean の数学ライブラリ Mathlib が700人超の寄与で 30万件近い定理に育った例を引き、同じ積み上がり方を期待している^[1]。

そして戦略が示されている。汎用の仕様を使い、バイナリの水準で作業することで、 コードベース全体を別の言語に書き直す必要を回避する^[1]。 依存関係はべき乗則に従うから、共有ライブラリのごく一部を証明するだけで、 広大な範囲のソフトウェアが証明可能になる^[1]。 協力先の Theorem は、glibc・OpenSSL・cURL を含む Nix エコシステム全体を 検証するロードマップを出している^[1]。

フィジカルAIから見て動いたのは、証明の値段ではなく証明の入口である#

発表本文が形式検証の実用例として名前を挙げたのは、seL4 カーネルと Airbus の航法コードである^[1]。どちらも本紙の領域に隣接している。 自律機械の安全論証は、最終的に「このコードはこの条件で必ずこう振る舞う」という 言い切りを要求するからで、その言い切りを人手の証明で買うと20人年だった^[1]。 そこが落ちるなら、効く場所は確かにある。

ただし本紙は、この発表の射程を「ロボットのコードが証明できるようになった」とは読まない。 前提を1つずつ当ててみると、ほぼ全部が外れる。証明の対象は単一スレッドで、 静的リンクで、固定メモリ予算で、RISC-V で、Linux である^[1]。ROS の上に積まれた制御系はそのどれでもないことが多い。 もっと決定的なのは、証明されている性質が 「メモリ安全性の違反もアサーション失敗も起こさずに正常に終了する」であることだ^[1]。 制御ループは終了しない。終了しないプログラムについて「正常終了する」は言えない性質であって、 言いたい性質は別——制御周期を踏み外さない、指令値が定義域を出ない、 停止要求から規定時間内に安全状態に入る——である。 発表本文には時間に関する性質への言及が無い。

仕様の側も同じ形で詰まる。発表側は、仕様が現実と合っているかは証明検査器には言えない、 合わせるには対象プログラムが動く実機のすべて——CPU と OS を含む——を 仕様が正しく覆っている必要があると書いている^[1]。 ソフトウェアだけを相手にしているなら、その「実機」は CPU と OS で閉じる。 本紙がフェルマーの最終定理の形式化の回で書いた線はここにもう一度引ける。あのとき移せるのは足場であって検証者ではないと書いたが、 今回は検証者のほう(Rocq)が信用の対象として明示され、 信用すべき成果物が3種に縮んだ^[1]。 縮んだのは良い。しかしロボットの側で同じ表を書こうとすると、 3種目の欄に物理が入る。接触、摩擦、たわみ、センサの飽和に、 RISC-V 命令集合に相当する形式意味論は無い。

その欠落の深刻さを、今回の発表自身が逆から示している。 Claude に x86 の意味論を書かせた過程で、公式の参照文書の誤りが数百件、 ハードウェア自体のバグが少数見つかった^[1]。 命令集合という、人類が最も厳密に書いたはずの仕様書がそれである。 機械の挙動を紙で言い切る作業の難しさは、 本紙がModel Hardware Standardの回に見た「装置統合は数時間に、物理の直観だけは埋まらなかった」の裏側と同じものだと考える。 データシートは間違っている。形式検証はそれを教えてくれるが、直してはくれない。

いま効くのは制御コードではなく、その下の依存関係である#

では、ロボットを運用している側が今回の発表から取れるものは何か。 本紙は、制御コードではなくその下の依存関係だと読む。

発表側の戦略は、依存関係がべき乗則に従うから共有ライブラリのごく一部を証明すれば 広大な範囲が証明可能になる、というものだった^[1]。 そして Theorem のロードマップに並んでいる名前は glibc・OpenSSL・cURL である^[1]。 ロボットのコントローラにも、画像のデコーダ、XML と JSON の解析器、圧縮、TLS が入っている。 libexpat の CVE 再発見^[1]や、画像デコーダの範囲外読み出し^[1]が 他人事でない構成は珍しくない。 ここは制御の作り方を変えずに恩恵が届く層であり、しかも依存関係ごとに1回証明すれば 共有できる層である^[1]。

本紙が止められないOTに残る時間差で書いた宿題との関係も、ここで整理できる。 あのとき問題だったのは、修正が工程の都合で待たされ、 まれには数十年という尺度になることだった^[2]。 本紙が直前に書いた攻撃面削減は、その待ち時間を短くする代わりに待っている間の重大度を下げる手口だった。 今回の形式検証は3つ目の方向で、次に入れる部品について、待つ理由を1つ減らすものである。 既に動いている機械の中身は変わらない。 変わるのは、次の更新や次の機種で採る部品に「この入口は64MB未満の入力で落ちない」という 札が付きうることだ^[1]。 止められない機械にとって、更新の回数そのものを減らす方向の答えは、 本紙が追ってきた3方向のうちこれが初めてである。

最後に、札の読み方を1つだけ付けておく。 「形式検証済み」は「バグが無い」ではない、と発表本文が自分で書いている^[1]。 証明の範囲は入口単位であって、ライブラリ全体ではない^[1]。 呼び出し側が誤用すれば、呼び出し側でメモリ破壊が起こる^[1]。 つまり札は、部品の内側について強い保証を与え、部品の使い方については何も言わない。利用規約が自律的に物理行動をとる装置に要求した条件——観察できること、停止できること、切断時に安全状態を保つこと——は、 どれも部品の内側ではなく系の組み方の性質である。 証明が届く境界と、安全要件が置かれている境界は、まだ一致していない。