# BPF verifier ## 定義 BPF verifier は、ユーザ空間から渡された BPF プログラムをカーネル内で実行する前に解析し、許可できるメモリアクセス、制御フロー、ヘルパー利用、終了性などを検査する安全境界である。信頼できないユーザ空間を保護する役割があるため、開発者支援用の検査をユーザ空間へ移す場合でも、本番の安全性検査そのものをカーネルから外すことはできない。(Source: [[@2026__LWN__BPF in the agentic era]]) ## エージェント時代の開発課題 コーディングエージェントは、生成、実行、エラー観測、修正を短いループで繰り返す。そのため verifier のエラーが大きな内部状態ダンプになり、テストのたびに仮想マシン起動を要する構成は、エージェントの性能を下げる。課題は安全性を弱めることではなく、安全なまま有用なフィードバックを早く返すことである。(Source: [[@2026__LWN__BPF in the agentic era]]) ## 提案されている分業 - Rust コンパイラで、通常のプログラムの単純な型・所有権・構文上の誤りを早期検出する。 - verifier は安全境界としてカーネル内に残す。 - 通常の Rust 製 BPF プログラムが、Rust コンパイラを通過した後に verifier で大量のエラーを出さない状態を目標にする。 - 避けられないエラーには、何が起きたか、なぜ起きたか、どう直すかを含める。 - user-mode Linux 上の検証は、本番の信頼境界を移さず、開発時のエラー返却を速くする手段として検討する。 この分業は記事が報告した提案であり、互換性が保証された実装仕様ではない。(Source: [[@2026__LWN__BPF in the agentic era]]) ## 表現力と検証コストのトレードオフ 候補として、より大きなスタック、深い呼び出し連鎖、間接関数呼び出し、構造体の値返し、128 ビット整数、長いジャンプ、100 万命令制限の見直し、BPF arena の活用が挙げられた。機能を増やすほど verifier が追跡すべき状態空間と、実行時検査へ押し出す責任の境界が広がる。(Source: [[@2026__LWN__BPF in the agentic era]]) ループに対する **widening** は、ループ変数の広い値域を一般化して扱い、検証の反復回数を抑える案である。状態の精度低下を実行時検査で補う可能性があるため、検証時間、安全性、実行時オーバーヘッドを同時に評価する必要がある。(Source: [[@2026__LWN__BPF in the agentic era]]) LSFMM 2026 のスライドはこの方向を具体化し、arena 型メモリ、`PTR_TO_FUNC` による間接呼び出し、5 個を超える引数と構造体返却の拡張呼び出し規約、`panic=unwind` と `.bpf_cleanup`、`bpf_throw()` を組み合わせる設計を示した。verifier の役割を停止性の完全証明からメモリ安全性の検証へ寄せ、証明できない箇所は実行時検査へフォールバックさせる考え方である。(Source: [[@2026__BPFConf2026__BPF in the Agentic Era (LSFMM 2026)]]) スライドは、ループの back-edge で状態を `[5,5]` から `[5,10]`、さらに必要なら `[MIN, MAX]` へ一般化する widening を示す。従来の `O(body × iterations)` に対し、widen の段数に依存する `O(body × widen_steps)` を目指すが、これは資料上の設計目標であり、実装済み性能結果ではない。(Source: [[@2026__BPFConf2026__BPF in the Agentic Era (LSFMM 2026)]]) ## 横断的知見 - **安全境界をカーネル内に固定し、開発者向け説明を外側で改善する二層化が、エージェント対応の基本形になる**: BPF はカーネル内 verifier を必要とする一方、エージェントは短いフィードバックを必要とする。Rust の早期診断、開発用 verifier、説明的なエラー表示を組み合わせる提案は、安全性と反復速度を同じ層で無理に解こうとしない設計である。(Source: [[@2026__LWN__BPF in the agentic era]], [[eBPF]]) - **verifier の改善は、拒否を減らすことと安全性を弱めることを分離する**: LWN の報告は Rust 側で単純な誤りを早期検出し、カーネル内 verifier を安全境界として残す方向を示す。スライドはさらに、証明不能な場合の実行時検査、panic の明示的な unwind、arena と型付きポインタを組み合わせる。両資料を合わせると、目標は「何でも通す verifier」ではなく「安全性を保ったまま、エージェントが修正できる検証経路」である。(Source: [[@2026__LWN__BPF in the agentic era]], [[@2026__BPFConf2026__BPF in the Agentic Era (LSFMM 2026)]]) ## 未解決の問い - Rust コンパイラ通過と verifier 通過の対応を、unsafe コード、インラインアセンブリ、ヘルパーの権限、Linux カーネル版差異を含めてどこまで定式化できるか。 - user-mode Linux 上の検証結果と実カーネル verifier の差異を、エージェントの開発ループでどう扱うか。 - widening が検証時間、誤拒否、実行時検査のオーバーヘッドに与える影響はどの程度か。 - verifier の説明的エラーを、LLM が誤った修正を反復しない形式へどう設計するか。 - BPF arena、長いジャンプ、関数呼び出し拡張を組み合わせたとき、安全性検査の複雑性はどのように増えるか。 - スライドが示す「verifier はメモリ安全性を証明し、停止性は実行時機構で扱う」という分業を、形式的な安全性定義と実カーネルの性能評価へどう落とし込むか。 ## 関連 - 概念: [[BPF]] / [[eBPF]] / [[Rust-BPF]] / [[BPF arena memory]] / [[形式手法]] / [[フィードバックループ]] / [[エージェント型コーディング]] - エンティティ: [[Alexei Starovoitov]] / [[Daniel Borkmann]] - ソース: [[@2026__LWN__BPF in the agentic era]] / [[@2026__BPFConf2026__BPF in the Agentic Era (LSFMM 2026)]] ## 出典 - [[@2026__LWN__BPF in the agentic era]]（verifier の役割分離、Rust 連携、エラー表示、widening の提案） - [[@2026__BPFConf2026__BPF in the Agentic Era (LSFMM 2026)]]（arena、間接呼び出し、widening、panic、ツールキットの設計案）