技術的概要：Heimdall

問題定義

拡張ベアリーパケットフィルタ（eBPF）プログラムは、ネットワーク、観測性、セキュリティにおける Linux カーネル拡張にとって不可欠です。カーネル内 eBPF 検証器は低レベルのメモリ安全性と終了性を強制しますが、初期化の厳格さ、スキーマの一貫性、エラー処理といった高レベルのソースレベルの性質は強制できません。著者は、コンパイルされカーネル検証器を通過するものの、データ silently な破損、機密情報の漏洩、または誤った強制結果をもたらす可能性のある 6 種類のソースレベルのバグを文書化しています。

特定された主要な脆弱性には以下が含まれます：

• 未初期化状態: ゼロ初期化なしでスタック居住構造体を出力するプログラムは、カーネルポインタや KASLR（カーネルアドレス空間レイアウトランダム化）スライドの復元に十分な戻りアドレスを含む、CPU 毎のスタック残留物を漏洩させます。
• 未チェックのヘルパー戻り値: 失敗するヘルパー関数（例：bpf_probe_read_user_str）はしばしば無視され、切り捨てられた文字列の代わりに古くなったスタックデータが出力されます。
• バッファ/サイズ不一致: 開発者が出力ヘルパーに誤ったサイズを渡すと、カーネルポインタを含む隣接するプライベートフィールドが漏洩する可能性があります。
• フック/コンテキスト不一致: 誤ったコンテキスト構造体（例：XDP フックでの __sk_buff）を使用すると、データが誤解釈されます。
• マップタイプ/スキーマの混同: 宣言されたマップ値のサイズと実際のデータとの不一致、またはマップ検索結果を無関係な型として再解釈すること。
• 符号付き/符号なしの混同: エラーを示す符号付きヘルパー戻り値を符号なしフィールドに格納すると、マップキーとして使用される架空の大きな正の値が生成されます。

さらに、eBPF 検証器自体に既知の脆弱性（例：正しくない剪除、契約検証の欠如）があり、これらが悪用される可能性があります。Rust のようなメモリ安全な言語への移行はこれらのギャップを埋めることができますが、大規模な手動書き換えは非現実的であり、既存の自動翻訳ツールは eBPF 文脈における意味的同等性や安全性を確保するための厳密さを欠いています。

手法：Heimdall パイプライン

Heimdall は、レガシーな libbpf C プログラムを慣用的で安全な Aya Rust に翻訳する自動化パイプラインです。これは、大規模言語モデル（LLM）、静的解析、形式検証を組み合わせた 5 段階の反復プロセスを採用しています：

1. LLM 翻訳: LLM が Aya API マッピング、フックマクロ、および実例を使用して、C ソースを Rust に翻訳します。
2. コンパイルとカーネル検証: 生成された Rust コードは eBPF バイトコードにコンパイルされます。コンパイラのリントガード（未使用の unsafe ブロックの拒否など）とカーネル検証器が基本的な安全性と正しさをチェックします。エラーは修復のために LLM にフィードバックされます。
3. 安全性チェック（静的解析）: カスタム静的解析エンジンが、コンパイラや検証器が見逃す可能性のある unsafe なエスケープハッチを Rust ソースからスキャンします。これには、型指定されていないリングバッファ予約の禁止、ゼロ初期化の強制、ヘルパー戻り値に対する Result 型の明示的な処理の要求が含まれます。
4. 記号実行: 元の C バイナリとコンパイルされた Rust バイナリの両方が、カスタム angr 用 eBPF バックエンド に読み込まれます。このバックエンドは eBPF ヘルパー、マップ、再配置、原子操作をモデル化します。記号実行を実行してすべての実行可能なパスを探索し、戻り値とマップの副作用のための構造化された数式を生成します。
5. 同等性チェック: Z3 ベースのソルバーが、C プログラムと Rust プログラムが意味的に同等かどうかをチェックします。著者は、宣言された安全性条件（例：ヘルパー呼び出しの成功）を満たす入力に対してのみ同等性を要求する条件付き意味的同等性を導入しました。これにより、エラーを処理するかメモリをゼロで埋めるより安全な Rust 翻訳が、バグがトリガーされるパスにおいてバグのある C ソースと同等と見なされつつも、有効なパスではロジックが保持されていることが検証されます。反例が見つかった場合、それはターゲットを絞った修復のために LLM にフィードバックされます。

これを支援するために、著者は ELF ローダー、アーキテクチャ定義、VEX IR リフター、ヘルパースタブを含む完全な eBPF バックエンドを angr 用に構築しました。また、記号的キー下でのマップ副作用をモデル化し、「最後の書き込みが勝つ」セマンティクスを捉えるためのカスタム ITE チェーン符号化 も開発しました。

主要な貢献

• Heimdall パイプライン: 観測可能な動作の保持に対するプログラム毎の形式保証を伴って、本番環境の eBPF プログラムを C から Rust に翻訳する最初の自動化システム。
• 条件付き同等性: バグトリガーパスにおいて異なる動作をする安全性向上の翻訳を検証する新しい検証アプローチで、同等性チェックを安全な実行パスに制限するもの。
• eBPF 記号実行バックエンド: カーネルヘルパー、マップ、BPF-to-BPF 呼び出しをモデル化する完全な angr 用 eBPF バックエンドで、バイトコードレベルでの形式的推論を可能にするもの。
• Safe-Aya 静的アナライザ: カーネル検証器を通過する unsafe な Rust パターン（型指定されていないリングバッファ、無視されたヘルパーエラーなど）を拒否するポリシーエンジン。
• セキュリティ発見: KASLR のスタック残留物による回復やリングバッファ内のクロスイベントコンテンツ漏洩など、10 のオープンソース eBPF プログラムにおける未報告の情報漏洩の発見。
• ベンチマークと評価: 102 の eBPF プログラムの公開ベンチマークと、翻訳パイプラインの包括的な評価。

結果

このシステムは、さまざまなソース（libbpf-tools、libbpf-bootstrap、KEN、Suricata など）からの 102 の実世界の eBPF プログラムで評価されました。

• 成功率: Heimdall は 96 の形式検証済み同等翻訳（94.1%） を生成しました。残りの 6 つは、記号実行の制限により部分的に検証されたか、ソルバーのスケーラビリティ制限を超えました。
• バグの解消: 検証済みの 96 の翻訳において、Heimdall は未初期化状態、未チェックのヘルパー戻り値、符号付き/符号なしの混同の観測されたインスタンスの 100% を解消しました。
• ベースラインとの比較: Heimdall パイプラインを持たないベースライン LLM エージェントと比較して、Heimdall（エージェント型）は 98% のトリプルパス率（コンパイル、カーネル検証、安全性、同等性）を達成し、ベースラインの 4〜12% と対照的でした。
• 実行時オーバーヘッド: 10 のプログラムでの実行時検証により、Rust 翻訳は一般的に modest なオーバーヘッド（C に対する幾何平均が 0.44 倍から 3.60 倍の範囲）を伴うことが示され、大部分は 1.14 倍から 1.89 倍の間に収まりました。
• 安全性: 翻訳は、特定された脆弱性を引き起こした特定の unsafe パターン（未初期化メモリ、未チェックのエラー）を排除しました。

重要性

本論文は、Heimdall が本番環境の eBPF プログラムのメモリ安全な移行を自動化し、移行が観測可能な動作を保持することを保証するプログラム毎の形式保証を持つ最初のシステムであると主張しています。これは、カーネル検証器の低レベル保証と現代の eBPF アプリケーションの高レベル安全性要件の間のギャップに対処します。LLM と形式検証および静的解析を組み合わせることで、Heimdall は構文的に正しいだけでなく、意味的に同等であり、かつカーネル検証器が検出できない特定のソースレベルの安全性バグから自由なコードを生成できることを実証しています。この研究は eBPF 移行の新しいベンチマークを確立し、より堅牢でメモリ安全なカーネル拡張を構築するための基盤を提供します。