Rust借用チェッカーのバグ：健全性が本当に意味すること

Rustの型システムは大きな約束をしています。安全なコードがコンパイルを通るなら、ダングリングポインタ、データ競合、use-after-freeは起きない、という約束です。ところがGitHubのissueに、一見安全そうなRustのコードが、すでに解放されたスタックフレームから値を読み出してゴミを表示するスニペットが投稿されました。さらにこの穴が11年間もRustの借用チェッカーに潜んでいたと分かり、多くの人が足元が揺らぐような感覚を覚えました。このバグでは、共変なフィールドへの代入を通じて構造体の寿命要件をすり抜けられます。悪意のあるDrop実装を組み合わせれば、ローカル変数への参照をグローバル領域に隠し、変数が消えた後で読み出せてしまいます。AddressSanitizerはこれをstack-use-after-scopeと呼びます。一方コンパイラは、問題なしと判断していました。

反応は予想どおりでした。Rustの安全性の話はもう終わりだと言う人もいれば、バグくらいあるさと肩をすくめる人もいました。ただ、どちらも肝心な点を見落としています。このバグは、静的な保証がどれほどの価値を持つのか、非公式な推論がどこで破綻するのか、そして「型システムは健全である」と「コンパイラが健全な型システムを強制している」の間の距離にこそ、最も興味深いバグが潜んでいることを示す、きれいな自然実験なのです。そこで、この話題から生まれた一般的な思い込みを一つずつ検証してみましょう。

神話1：健全性のバグはRustの安全性モデルが失敗したという意味だ

最初に浮かぶ反応は、これを理論のひび割れとみなすことです。しかし違います。寿命のルールが書き換えられたわけではありません。所有権と借用の仕組みが根本から壊れていると分かったわけでもありません。ホワイトボードやRFCで設計されたRustの型システムは、このプログラムは拒否されるべきだと言っています。コンパイラがそれを拒否し損ねただけなのです。

仕様と実装の違い、この区別は私たちの分野で最も古い断層の一つです。Tony Hoareは見事な並行逐次プロセスの理論を残しましたが、その後も何十年にわたり、標準の下では正しいコードをC言語のコンパイラが誤ってコンパイルし続けました。理論は成り立っていても、成果物からは漏れが生じる。以前にも仕様と実装のギャップこそバグが生まれる場所であると書きましたが、今回はまさにその典型例です。寿命のルールが間違っていたわけではありません。rustcの変性（variance）推論のコード、つまり&'a Tを&'static Tが期待される場所に置き換えてよいかを判断する部分に、共変なフィールドを経由して代入が流れるケースで穴があったのです。

エクスプロイトの形を簡単に示します。まず、Drop実装がペイロードを'staticなグローバルストアにコピーするラッパーを作ります。通常、コンパイラはペイロードが'staticであることを強制するので、ローカル変数への参照は入り込めません。このバグを使うと、共変な代入を通じて寿命の短い参照をすり抜けさせることができ、ラッパーはローカルのStringであるlに対する&lを保持することになってしまいます。

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

どの行も一見無害です。健全性の穴は組み合わせの中にしか存在しません。共変なフィールド、寿命の境界を緩める代入、そして参照先より長生きする場所へペイロードを移すDrop。これこそ、チェッカーの実装バグに典型的な形です。不変条件はグローバルに成り立っているのに、その強制はローカルでしか行われず、一つのコードパスがチェックを忘れていたのです。

つまり、安全性モデルが失敗したわけではありません。失敗したのは、安全性モデルを強制する仕組みです。規模としては小さな失敗ですが、後で見るように、取るに足らないものではありません。

神話2：11年間見つからなかったのだから、このバグは無害だ

Rustチームのトリアージの判断はおおよそ次のとおりでした。実際に被害が報告されていれば重大（P-critical）だが、11年間も報告がないということは、再現が難しいはずだ、だから優先度は高い（P-high）止まりだ、と。確かにそのとおりの面はあります。メモリ安全性を実際に壊すには、データを'staticな場所に移す、意図的に意地の悪いDrop実装が必要です。そんなものを書く人はほとんどいません。偶発的に露出する範囲はごくわずかなのです。

しかし、「偶然にはめったに起きない」という言い回しは、この文の中で多くの仕事をしています。安全性の保証は偶然の事故だけのためのものではありません。周囲のコードが親切でないときに、何を頼りにできるかが本質です。健全な型システムの強みは、モジュール単位で推論できることにあります。あなたのDrop実装を監査する必要はない。なぜなら、特定の危険な組み合わせは表現不可能だとコンパイラが既に証明しているからです。一度穴が開けば、そのモジュール性は失われます。悪意のある依存ライブラリ、あるいは善意の作者が書いた微妙に誤った依存ライブラリが、言語が不可能だと約束していたことを実行できてしまうのです。

歴史には「悪用できない」とされたバグが、適切な部品が現れた途端に非常に悪用可能になった例が数多くあります。あるコメントが指摘したように、実務上の問題は、この修正がエコシステムの実在するクレートを壊すかどうかです。その答えはおそらく「ごくわずか、あるいはゼロ」で、これは良いニュースです。しかし、11年間の静けさから得るべき正しい教訓は「バグは無害だった」ではありません。偶然ではなく悪意を必要とする故障モードについては、「証拠がないことは、不在の証拠ではない」ということなのです。

神話3：目が多ければ、すべてのバグは浅いうちに見つかる

これは私たちが最も反省すべき神話です。rustcは、これまで書かれたコンパイラの中でも最も精査されているものの一つです。オープンソースであり、専任の型チームがあり、活発な学術コミュニティがあります（RustBeltは数年前にRustのコア部分の形式モデルを示しました）。さらに毎日何百万人ものユーザーが叩いています。それでも、周辺の仕組みが何度も全面的に書き換えられたあとも、寿命推論には10年以上も健全性の穴が残っていたのです。

Linusの法則は、目が正しい場所を、正しいモデルを頭に入れて見ていることを前提にしています。型システムの健全性の穴は、この両方の前提を崩します。それらは変性、ドロップ順序、型強制、トレイト境界といった複数の機能の交差点に生まれ、個々の機能はどれも局所的には正しいのです。レビュアーは意図された不変条件を見て、コードを読みます。コードを書いた人もまた、意図された不変条件を見ていたからです。確証バイアスはプロセスそのものに組み込まれています。反例を見つけるには攻撃者の視点で考える必要がありますが、自分の抽象化に対してそうした敵対的な思考をするのは本当に難しいのです。

counterexamples.orgという、もっともらしい型規則がどう破綻するかを集めたサイトがあります。その共通点は、可変性と何か別の厄介な要素との組み合わせであり、まさに今回のバグと同じ形です。これらは新しい教訓ではありません。MLの型システムには、可変参照と多相性に関する有名な健全性の問題があり、値制限（value restriction）によって修正されました。Javaの配列は共変で、実行時にArrayStoreExceptionを投げることがあります。言語設計者が健全性より利便性を選んだからです。こうした考古学的な話に興味があれば、Lispの60年の歴史を見ると、これらのアイデアがどれほど長く進化してきたかがわかりますし、Rob Pikeの古いルールの単純さに関する教えも、複雑さこそ健全性の穴が育つ場所だと気づくと違った意味を持ちます。

目による確認は役に立ちます。しかし十分ではありません。自分で言語を作っている人から聞いた率直な立場は、次のようなものでした。どれだけレビューしても、すべての問題は解決できない。だから、疲れず、あなたの前提を共有しない機械的な手法が必要なのだ、と。

神話4：非公式な推論は、ほぼ証明と同じだ

Rustの寿命ルールが設計されたとき、それは賢明な人々によって、多くの例を使いながら慎重に議論されました。これは非公式な推論であり、実のところ本番環境のコンパイラはほぼすべてこの方法で作られています。その結果できあがるのは、誰にとっても知る限りでは健全なシステムです。しかし、私たちは二度にわたって学んだとおり、これは健全であることと同じではありません。

両者のギャップを埋めようとしているのが、RustBeltのようなプロジェクトや、次世代のトレイトソルバーに関する現在進行中の取り組みです。RustBeltはCoq（現在はRocq）とIrisの分離論理フレームワーク上に構築され、unsafeの抽象化境界のような危うい部分を含む、Rustのコアな型付け規則のモデルを機械的に検証しました。これは画期的な成果でした。しかし、何を証明したのかに注意が必要です。証明されたのはRustのモデルであって、rustcではありません。この証明はλRust計算に対するものであり、本番のコンパイラは漂流し、機能を増やし、誰も再検証していない実装上の決定を積み重ねてきました。今回の問題は、その漂流のツケが回ってきたものです。

本番のコンパイラ全体を形式化するのは、途方もなく高くつきます。形式検証されたCコンパイラであるCompCertは、Rustよりはるかに小さい言語に対してさえ、専門家による数年の努力を要しました。しかもCompCertが検証するのはコンパイル工程であって、ソースの型システムがあらゆる不正なプログラムを捕まえることを証明するものではありません。rustcの200万行をCoqで証明しようとする人はいないでしょう。現実的な道筋は、多層防御に近いものになります。

• コアな規則の機械検証済みモデル（RustBelt型）。理論そのものに穴がないことを保証する。
• 体系的なファジングとケース解析ツール。人間がテストを思いつかない機能の交差点の隅々を突く、敵対的なプログラムを生成する。
• チェッカーの変異テストとプロパティベーステスト。境界条件を反転させたら失敗するはずのプログラムが、本当に失敗することを確認する。ここではSQLiteのテスト文化がお手本になる。
• 既知の非健全な問題のメンテナンスされたリスト。Rustにはすでに100を超えるものがタグ付けされている。これを言い伝えではなく、エンジニアリング上の優先度を持つバックログとして扱う。

意外なことに、LLMベースの探索が結果的に有益になるかもしれません。ありそうもない方法で機能を組み合わせ続けるツールは、非公式な推論に欠けている、まさに敵対者そのものだからです。多くの人が望んでいる最終形は、形式的に仕様化されたRustと、その仕様に対して証明されたチェッカーです。しかし、そこに至るまでの道のりは、地道で目立たない制約解決の作業の積み重ねになるでしょう。

神話5：健全性が絶対的でないなら、静的な安全性はペテンだ

皮肉な読み方はこうです。Rustは安全性を約束したが、その約束には抜け道があった。だから約束はマーケティングにすぎず、Cでポインタを好き勝手に扱う昔のやり方に戻ればいい、と。しかし、これは完全に逆であり、なぜそうなのかを正確に述べておく価値があります。

型システムにおける健全性とは、数学的対象についての定理です。一方、本番で使える言語が与えてくれるのは、統計的かつ経済的な保証です。use-after-free、データ競合、イテレータの無効化といったバグの種類全体が、「コードベースに常に存在するバックグラウンドノイズ」から、「11年後に見つかってフロントページに載るほど稀な出来事」へと変わるのです。基礎発生率を比べてみてください。大規模なCやC++のコードベースにおけるメモリ安全性のバグは、年々の重大なCVEの大半を占めていますが、今ではその一件一件に誰も驚きません。一方、Rustの非健全性バグは非常に稀なので、一件ごとに専用のGitHub issue、議論スレッド、事後検証の文化が生まれます。数えられるほど稀であることと、数えられないほど稀であることは、まったく別の世界なのです。

失敗がどう積み重なるかにも違いがあります。Cでは、どの行もメモリ安全性の危険の可能性があるため、警戒のコストはコードの規模に比例して永遠に増え続けます。Rustでは、警戒は端に集中します。unsafeブロック、FFI、そして（今わかったように）コンパイラ自身のチェッカーです。この集中こそが、監査、Miriのようなツール、形式手法を現実的なものにしているのです。保証は二値ではなく、リスクがどこに存在するかを大胆に組み替えるものなのです。

既知のバグがある型システムでも、11年間の本番トラフィックで一度も踏まれなかったのであれば、バグそのものが設計になっている言語よりも、はるかに強いと言えます。

本当に持ち帰るべきこと

Rustを書いている人は、何も変える必要はありません。この問題が報告される前から、あなたのコードが静かに安全でなかったわけではありません。実際の悪用経路には意図が必要でした。ライブラリをメンテナンスしている人にとって、正しい対応は昔からと同じです。unsafeの露出面を小さく保ち、難しい箇所ではMiriを走らせ、他人の悪意あるコードに対して借用チェッカーを万能の判定者とみなさないこと。自分自身のミスを捕まえるための、極めて信頼できる道具として扱ってください。

言語やコンパイラを作っている人にとって、このバグは贈り物です。本番環境で健全性がどのように実際に破綻するかを示す、希少でよく記録された標本だからです。理論ではなく強制の部分で、単一の機能ではなく機能の交差点で、レビューではなく敵対的な構築によって見つかったのです。これを真剣に受け止めるチーム、つまりトレイトソルバーの書き直し、リージョン制約の再設計、検証に近いツールへの投資を行うチームこそ、10年後に保証が意味を持つ人たちになるでしょう。

そして、すべての人へ。保証とは何かを再定義しましょう。私たちは何十年もの間、型システム、暗号プロトコル、分散合意において、「証明済み」と「説得力を持って論じられ、まだ反証されていない」を混同してきました。大人の信頼のあり方とは、橋が完璧だと信じ込むことではありません。橋には検査官がいて、その検査結果を公表し、見つけた亀裂を直し、まだ直していない亀裂の公開リストを保っていると知ることです。その点で、穴を見つけるのに11年かかったことは、告発ではありません。コンパイラを取り巻く人間のシステムが、ほぼ想定どおりに機能しているという証拠なのです。