Rustによる書き換え＋差分ファジング＋形式検証でカーネルのCパーサーを堅牢化。最初のターゲット: UVC (CVE-2024-53104)。
セキュリティ上重要な Linux カーネルの C パーサを Rust で書き直すことでハードニングできるのか、しかもその書き直しが元のコードと等価であることを示したうえで形式的に検証できるのか。このスパイクは 1 つのターゲットに対してループ全体を実行する。ターゲットは UVC ビデオディスクリプタパーサ(drivers/media/usb/uvc/ の uvc_parse_format/uvc_parse_frame、v7.2-rc2)であり、16 年の隔たりをもつ 2 つの独立したメモリ安全性 CVE(CVE-2008-3496、CVE-2024-53104。後者は CISA KEV カタログに収録)を抱えていたことから選定した。
C リーフの抽出(c/)。パースロジックはカーネルからバイト単位でコピーし、環境のみをスタブ化した(// SPIKE-STUB)。C-ABI ライブラリとしてコンパイルされる。抽出したリーフにはカウントパスとサイズ付きアロケーションが含まれるため、CVE-2024-53104 のバグクラス(パースがカウントで確保した範囲を超えて書き込む)は抽象化で消されることなく到達可能である。
Rust での書き直し(rust/)。同じパースリーフを安全な Rust で実装し、C ABI と結果構造体も同一にした。C からの逸脱はすべて // DEVIATION でタグ付けし、文書化している。
差分ファジング(fuzz/)。stable rustc 上の LibAFL ハーネスが両実装を同一入力で駆動し、出力をフィールド単位で比較する。結果: コンパイラ依存の符号付きオーバーフロー箇所における移植時の不一致を 1 件修正した後、54,019 回の実行で 93% のエッジカバレッジにわたり乖離はゼロ。忠実な v7.2-rc2 のコードでは範囲外アクセスに到達しない(両 CVE とも修正済み)。オプトインのネガティブコントロール(--features vuln、両言語でミラー)は CVE-2024-53104 の不一致を再導入する。同一入力に対して C はヒープの範囲外書き込みを行い(ASan)、Rust は安全にパニックする。詳細は fuzz/RESULTS.md。
形式的検証(verify/)。忠実な Rust リーフは Charon と Aeneas を経て Lean 4 に抽出され、生成コードに sorry はなく、Binder スパイクと違って union のブロッカーもない。定理は 2 つで、verify/VERIFY-REPORT.md と ROADMAP.md に記載している:
ok / 制御された fail / 非終了のいずれかであり、未定義動作の結果には決してならない): 証明済み、sorry なし。これにより、C が欠いているメモリ安全性の性質を、検査済みの命題として明示する。sorry なしで証明済みであり、再利用可能な Aeneas のループ推論原理 2 つと、構造的に終了する 5 つのループに対する除算不要性も証明済みである。残りは、名前付きの位置走査の関数正しさコア(4 つの提示済み補題)に帰着する。ROADMAP.md を参照。ループは 1 つのターゲット上でエンドツーエンドに実証されている。書き直しが C と等価であることは差分ファジングで示され、メモリ安全性の差異はネガティブコントロールによって具体化され、Rust はクリーンに Lean へ抽出され、その全安全性の性質は機械的に検査されている。非パニック定理については、カウント不変条件(CVE-2024-53104 の中核)が sorry なしで証明され、残りの作業は名前付きの関数正しさコアに帰着しており、提示はされているがまだ証明されていない。証明の完全なステータスと未解決の補題は ROADMAP.md にある。
c/ — 抽出した C リーフとそのスタブrust/ — 安全な Rust による書き直しfuzz/ — LibAFL 差分ファザー、結果、CVE クラスのコントロールverify/ — Charon/Aeneas/Lean の抽出と定理ROADMAP.md — 証明のステータスと残る未解決の補題OPEN_CHALLENGES.md — コントリビューターが着手できる具体的なタスク*/README.md、fuzz/RESULTS.md、verify/VERIFY-REPORT.md — ステージごとの詳細カーネル v7.2-rc2(読み取り専用の参照)。Rust stable 1.94.0。LibAFL 0.15。Charon 909ff09a(v0.1.220、--preset=aeneas)、Aeneas c2015b86、Lean/mathlib v4.31.0。