필사 모드: eBPF Verifierは止まった場所しか教えてくれない — 拒否235件を再現して測った診断ギャップ

• はじめに — エラーは止まった場所を指し、バグは別の場所にある
• 診断ギャップとは何か — 証明を失った地点 vs 検証が止まった地点
• データセットをどう作ったか — 936件から235件へ
• 発見1 — 拒否の19%はソースが健全
• 発見2 — 根本原因12種、うち10種がeBPF固有
• 発見3 — エラー文字列一つが原因9種類を隠す
• 既存ツールがこのギャップを埋められない理由
• bpfix — ログから証明の生涯を復元する
• 実際の事例 — aya Issue 1002
• LLMはverifierエラーを直せるか — bpfix-bench
• この数値をどこまで信じるべきか
• 一方、verifier自体も変わりつつある
• では実務者は何をすべきか
• おわりに
• 参考資料

はじめに — エラーは止まった場所を指し、バグは別の場所にある

eBPFプログラムを一度でも本気で書いたことがある人は、この感覚を知っています。パケットポインタを確かにバウンドチェックしたはずなのに、ずっと後のロード命令でR5 invalid mem access 'scalar'が出る。エラーが指す行には疑わしいところが何もない。そこでどうするかというと — 直せそうな箇所を手当たり次第に直し、再ロードし、また弾かれたら別の箇所を直す。eBPF開発が試行錯誤の繰り返しになるのは、まさにこの地点です。

eBPF基礎完全制覇で整理した通り、verifierが存在する理由ははっきりしています。カーネルの中で任意のコードを走らせるには、誰かがそれが安全だと証明しなければならず、verifierがその証明を代わりに行います。問題は、証明に失敗したときにverifierがその失敗をどう説明するかという点です。

2026年7月2日にarXivへ投稿されたCharacterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections(Zhengら、arXiv:2607.02748)が、このもどかしさを初めてきちんと測定しました。著者らはUC Santa Cruz、Virginia Tech、Telecom Paris、University of Washington、University of Connecticut、そしてeunomia-bpfに所属しています。

論文の一文がすべてを要約しています — エラーは検証が止まった場所だけを報告し、プログラムがverifierの要求する証明を失った場所は報告しない。

診断ギャップとは何か — 証明を失った地点 vs 検証が止まった地点

この区別が本稿全体の核心なので、少し丁寧に見ていきます。

verifierは命令を一つずつたどりながら、各値について「この値は安全に使える」という証明を積み上げます。たとえばパケットポインタなら「このポインタはバウンド内に収まる」という証明です。ある命令がその証明を持たないまま値を使おうとすると、そこで検証が止まり、プログラムは拒否されます。

ところが、証明が消えた時点と証明が必要になった時点は、たいてい異なります。論文が挙げる実行例が鮮やかです。ある中間状態でR5はpkt(off=34,r=42)、つまりバウンド情報を持つパケットポインタです。ところが命令37の直前の状態では、同じR5がスカラー値40として表現されています。そして命令37がR5を参照解決します。

• 証明を失った地点: パケットポインタがスカラーに変わったどこか(論文の用語でloss point)
• 検証が止まった地点: 命令37(エラーが教えてくれる唯一の場所)

エラーは後者しか教えてくれません。開発者が直すべきなのは前者です。論文の表現通り、修正は失われた証明を復元しなければならないのに、エラーはその証明を必要とした演算だけに名前を付けます。だから開発者は、トレースから「どの証明が必要で、それがどこで消えたか」を手で再構成しなければなりません。

データセットをどう作ったか — 936件から235件へ

論文の実証パートが誠実なのは、方法論を隠していないからです。

著者らは四つの場所から候補936件を集めました — Stack Overflowの質問、GitHubのIssue、GitHubの修正コミット、カーネルのセルフテストです。そして各候補を一つの固定ツールチェーンで再ビルドしました。カーネル6.15.11、clang 18、ログレベル2です。(6.15は2025年5月に出たメインライン系列のstableポイントリリースです。)

936件のうち、実際にこのビルドで拒否されたのは235件であり、この235件がbpfix-empiricalというデータセットになります。残りが脱落した理由も明記されています — 著者らのツールチェーンでは拒否されない、特定の環境を必要とする、あるいは再ビルドするソースがない、のいずれかです。

各事例は、問題のソースと開発者本人が実際に適用した修正をセットで持っています。これが重要です。「何が本当の原因だったか」の正解は著者らの推測ではなく、元の報告に残された実際の修正が教えてくれるからです。

発見1 — 拒否の19%はソースが健全

235件を「修正がどこに着地したか」で分類した結果が、最初の驚きです。

• 191件(81%): 修正がプログラムのソースを変更した。つまり本物のプログラムバグ。
• 44件(19%): ソースは正しいのに拒否された。修正は別の層で行われた — コンパイラが18件、環境が14件、verifier自体が12件。

論文が挙げる例が印象的です。明らかに安全なコンテキストフィールドの読み取りが拒否されるのですが、理由は-O0がその読み取りをスカラーへ落とす(lowering)ため、verifierがポインタの出自を見られなくなるからです。修正はソースに手を触れないコンパイラフラグです。論文Figure 2のコードはこれほどシンプルです。

// 正しいソース。-O0がフィールド読み取りをスカラーへ落とす
static int add_one(int x) { return x + 1; }
int prog(struct xdp_md *ctx) { return add_one(ctx->rx_queue_index) & 1; }
// verifier: R2 invalid mem access 'scalar'

これは実務的にかなり重要な話です。verifierが拒否したからといって、あなたのコードが間違っているとは限りません。五回に一回程度は、コードは正しく、コンパイラが証明を隠したか、環境が合っていないか、verifierがまだそのパターンを理解していないかのどれかです。ただし、エラーメッセージはこの両者を区別してくれません。

発見2 — 根本原因12種、うち10種がeBPF固有

191件の本物のバグは、12の根本原因に分かれます。ここでいう「根本原因」は、verifierが失敗した検査ではなく、開発者がソースレベルで犯したミスを指します。

論文の指摘は、この12種のうち10種がeBPF固有だということです。パケットのバウンドを証明することや、dynptrをその寿命と正しく対にして扱うことは、一般的なCプログラミングの知識からは出てきません。だから修正には、一般的なプログラミング能力ではなくドメイン知識が必要になります。null検査の欠落だけが例外的に一般的な部類に入ります。

これは、eBPFの学習曲線がなぜあれほど急なのかについての定量的な説明でもあります。問題の大半は「Cをうまく書けば済む」種類のものではありません。

発見3 — エラー文字列一つが原因9種類を隠す

もっとも痛い数値がここにあります。

第一に、errnoはほとんど何も教えてくれません。拒否全体の47%がEINVALしか返しません。半数近くが「何か問題がある」という意味だけのエラーコードにまとめられているわけです。

第二に、エラー文字列も粗すぎます。著者らは各エラー文字列からレジスタ番号とオフセットをマスキングして正規化し、235件をまとめました。互いに異なる文字列167個が、テンプレート82個に縮まります。そして82個のテンプレートのうち15個が、それぞれ二つ以上の根本原因に対応します。

もっともひどいのが下の表の一行目です。

invalid mem access 'scalar'一つが、28件にまたがって互いに異なる根本原因9種類を覆い隠します。このメッセージを見て原因を絞り込めると信じることには、統計的な根拠がありません。論文のTakeawayをそのまま訳すと — 終端エラーは修正を導くには粗すぎる。

既存ツールがこのギャップを埋められない理由

すでにツールがあるのではないか、と聞きたくなるかもしれません。論文は二つを挙げています。

PrettyVerifier(Rizzaら、2025 IEEE CSR)は正規表現で終端エラーをソース行とヒントにマッピングします。BPF Verifier Visualizer(bpfvv)は命令ごとの状態をインタラクティブに描画するフロントエンドです。bpfvvのリポジトリ自身も、自らを原始的なデバッガUIだと説明しています — ランタイム状態ではなくログを解釈するものだと。

論文の評価はこうです — 両方とも開発者がエラーを読む助けにはなるが、証明をどこで失ったかは示さない。

そして、なぜこれが難しいのかについての説明が鋭いです。Rustのようなエラー説明ツールは、チェッカーが作った構造物(AST、型付けの制約)をたどることができます。ところがeBPF verifierはそうしたアーティファクトを外に出しません。残るのはログだけです。

bpfix — ログから証明の生涯を復元する

そこで著者らが作ったのがbpfixです。核心となる洞察はこうです — ログレベル2では、verifierは命令ごとに抽象状態をすべて出力します。つまり失われた証明は、すでにログの中に生きています。誰もそれを読んでいないだけです。

bpfixはRustで約23,000行であり、唯一の必須入力は既存のverifierログです。ソースやオブジェクトのメタデータは任意で、あれば命令からソースへのマッピングが良くなります。パイプラインは三段階です。

1. ログ解析 — 終端エラーと命令ごとの抽象状態を、正規化された証拠ストリームとして抜き出す。
2. 証明の復元 — 終端エラーを証明系列(proof family)にマッピングする。ポインタの出自、パケットのバウンド、スカラーの範囲といったものです。そして、その証明に対する証拠がいつ成立し、維持され、消えるのかを追跡する。
3. 診断の生成 — スパンを選び、証明を再確立するための指示を作る。

出力はRustスタイルの平文診断です。安定したエラー識別子、必要な証明、関連するスパンと証拠、観測可能な場合のloss point、そしてhelp:の指示から構成されます。「観測可能な場合」という注記は著者ら自身が付けたものです — 常に捕まえられるわけではありません。

もう一つ実用的な機能が責任層の分離です。bpfixは拒否をsource_bug(ソース層)とlowering_artifact(コンパイラ層)にラベル付けします。先に見た「19%はソースが健全」という問題に直接対応する機能です。ただし論文はこれを最善努力ベースの帰属(best-effort attribution)だと明記しています。

論文のFigure 5がこの機能の要点を示しています。二つの拒否がまったく同じ終端メッセージinvalid mem access 'scalar'で終わるのに、片方はソースバグ(Stack Overflow 56965789 — パケットベースなしに整数オフセットをポインタへキャスト)で、もう片方はコンパイラのloweringアーティファクト(Stack Overflow 53136145 — 分岐のマージがパケットポインタの型を隠す)です。修正が着地すべき層はまったく異なるのに、verifierのメッセージは同一です。

実際の事例 — aya Issue 1002

論文が挙げる具体的な例を一つ見てみます。マップオブジェクト&globalsのアドレスを__u64 *にキャストして、直接読み書きするプログラムです。

// 拒否されるプログラム
__u64 *raw_map = (__u64 *)&globals;  // マップオブジェクトポインタ
__u64 v = *raw_map;
*raw_map = v + 1;                    // ここで拒否される

// verifier: only read from bpf_array is supported

verifierのメッセージは間違っていません。ただ症状だけを述べています — マップオブジェクトを通じた書き込みを見た、と。なぜだめなのか、何をすべきなのかは述べていません。

bpfixの診断はこうです — マップポインタが通常のメモリのようにアクセスされている(source_bug)、必要な証明はマップの内容を読み書きする前に適切なマップヘルパーでマップ値ポインタを導出することだ、次の行動は要素をルックアップしてからそのポインタを通じて書き込むことだ。

そして開発者の実際の修正が、まさにその診断の通りになっています。

// 開発者の実際の修正
__u32 key = 0;
__u64 *v = bpf_map_lookup_elem(&globals, &key);
if (!v) return 0;
*v += 1;

LLMはverifierエラーを直せるか — bpfix-bench

論文の最後の軸は、最近の人々が実際に気になっている問いです。どのみちエラーログをLLMに投げるだろうけど、それでうまくいくのか?

著者らはbpfix-benchというベンチマークを作りました。ソースレベルの修復課題75問で、40問は特定のverifier証明を中心に構成し、35問はCilium、xdp-tools、bpftraceのようなオープンソースプロジェクトから最小化して取り出しています。

採点方法は誠実です。各課題はbpfixとは独立した実行可能なテストスイートを備えています。修正が認められるには、(1) 実際のカーネルverifierを通過してロードされ、(2) 機能テストを通過し、(3) ソースセマンティクス検査を通過しなければなりません。つまり「もっともらしいテキスト」では点数がもらえません。verifierを回避するためにロジックを壊すというよくある手口も、ソースセマンティクス検査で引っかかります。

モデルはQwen3.6 27B(主モデル)、GLM 5.2(ホスト型)、Qwen2.5 3Bの三種類で、temperature 0です。3Bを入れた理由は、利得が小さいモデルでも生き残るかを見るためです。結果は以下の通りです(すべて75問中、著者自身の測定)。

ここから二つのことが読み取れます。

第一に、元のverifierログだけを渡すと、今のモデルはうまく直せません。ワンショットの成功率は0〜37%です。論文の表現では、3Bから27Bまでの三モデルにわたって、verifierの拒否は有能なモデルにとってもなお難しい。

第二に、ログをbpfixの診断に置き換えると改善します。論文がアブストラクトで主張する幅は11〜21ポイントです。ワンショット基準で見ると、Qwen3.6が21.4ポイントでもっとも大きく、Qwen2.5 3Bが10.7ポイント、GLM 5.2が13.4ポイントです。ただし、GLM 5.2のリトライモードでの利得は6.6ポイントとずっと小さいという点は、表で直接確認する必要があります — このアブストラクトの幅はワンショット基準で読むのが正しいです。

失敗がどの段階で消えるのかも著者らが分解しており、これがむしろ説得力があります。Qwen3.6 27Bでは、verifierロードの失敗が19件から10件へ、ソースセマンティクスの失敗が22件から16件へ減りました。GLM 5.2も同じ方向です(10 → 5、25 → 22)。コンパイル失敗はどちらも低いまま推移しました。

小さいモデルの話は別に見る価値があります。Qwen2.5 3Bは元のログでは75問中一問も直せませんでした。ワンショットの候補62件がverifierロードで失敗し、プロンプト3件はそもそもコンテキストウィンドウを超えてプログラムを返せませんでした。より短いbpfix診断を渡すと、モデル呼び出しの失敗は消え、ロード失敗は39件に減りますが、コンパイル失敗は7件から14件へ増えます。著者らの解釈は誠実です — bpfixは小さいモデルにも、より意味のある修復を試みるだけのverifier関連情報を与えるが、ありふれたコード生成の誤りはそのまま残る。

この数値をどこまで信じるべきか

ここから先は、論文自身が語っている限界と、私が読みながら付け加えた留保です。本稿の数値の大半が著者自身の測定であることを、まず明確にしておきます。bpfixもベンチマークも同じチームが作りました。

選択効果が大きいです。936件中、生き残ったのは235件だけです。生き残った理由は著者らの固定ツールチェーンで再現したからで、脱落した701件の相当数は環境依存であるか、ソースがないものです。そして、そもそもデータの出所がStack OverflowとGitHubのIssueです — 人々がわざわざ質問を投稿するほど混乱した拒否が過大代表されます。「診断が不十分だ」という結論を出すのに有利な方向へ標本が傾いている可能性があります。もっとも、カーネルのセルフテストと修正コミットも混ざっているので純粋な偏りではなく、実務で人を実際に足止めするのはまさにその混乱する拒否だ、という反論も成り立ちます。

ツールチェーンが一つに固定されています。カーネル6.15.11、clang 18です。verifierはリリースごとに変わり、特にエラーメッセージとpruningの挙動は絶えず手が入ります。6.15で測定した47%が最新カーネルでもそのままだと仮定してはいけません。

モデルの選定が限定的です。Qwen3.6 27B、GLM 5.2、Qwen2.5 3Bです。フロンティア級のモデルは評価に含まれていません。だから正確な言い方は「LLMはverifierエラーを直せない」ではなく「この三モデルは元のログで0〜37%を直した」です。

そしてbpfixを使っても天井は低いままです。最高成績はワンショットで50.7%、リトライを足しても69.3%です。診断が良くなれば修復が良くなるという方向性は三モデルで一貫して見られましたが、「もうLLMに任せればいい」という水準とはまだ距離があります。

ツールの成熟度も考慮する必要があります。bpfixのリポジトリはMITライセンスで公開されており、v0.1.0は2026年7月11日に出ました。生まれて五日の0.1.0です。READMEは自ら、これはカーネルパッチでも、verifierの代替物でも、自動ソース修復ツールでもないと明記しています。診断説明ツールです。プロダクションパイプラインに入れる前は、その程度の期待値で臨むのが正しいでしょう。

一方、verifier自体も変わりつつある

この論文が「ログをもっと上手に読もう」というアプローチだとすれば、その対極には「そもそもverifierが拒否する回数を減らそう」という流れがあります。

LWNのBPF loop verification with scalar evolution(Daroc Alden、2026年6月9日)が取り上げたEduard Zingermanの作業がその例です。2026年のLSFMM+BPFサミットで発表された進行中の作業で、目標はZingerman自身の言葉通りverifierが典型的なfor/whileループを、ループを回すことなく単一パスで処理できるようにすることです。

現在のverifierはループに出会うと、終了条件に到達するまで反復ごとに評価しますが、この過程でより良い実装なら引っかからなかったはずの命令数制限に誤って引っかかることがあります。スカラー進化(scalar evolution)は、ループ内で変数が取りうる値の範囲を計算することでこれを避けようとする手法です。

ただし、これはまだプロトタイプであり、マージされていません。スタックへスピル・復元されるレジスタを扱えず、すべてのループ変数を均一に解析することもできません。Zingermanは、スタック操作、符号付き整数演算、より複雑なループへの対応を済ませてから、カーネルへの提出を提案する計画だと述べています。ロード時間については厳密な測定をしていないと本人が語っています。(Starovoitovは、過去の似たようなverifierの変更も最初は懸念を招いたが、結局はロード時間が速くなりメモリ使用量が減った、と述べています。)

二つの流れは同じ問題の両面です — 一方は拒否を減らし、もう一方は拒否されたときに理解可能にします。そして後者が消えることはありません。verifierがどれだけ賢くなっても拒否は残り、残った拒否は説明されなければなりません。

では実務者は何をすべきか

この論文からは、ツールを導入しなくても持ち帰れるものがあります。

ログレベル2をデフォルトにしてください。bpfixが存在しうる理由そのものが「必要な情報はすでにログの中にある」ということです。レベル2ではverifierが命令ごとに抽象状態を出力します。それを有効にしていないなら、診断の原材料を捨てていることになります。

終端エラーの行を信用しないでください。それは検証が止まった場所です。バグは証明が消えた場所にあります。実際にやるべきことは、ログをさかのぼって、問題のレジスタが最後に正しい型だった時点を探すことです。pkt(off=..,r=..)がscalarに変わった地点のようなものです。

拒否をとにかく自分のせいにしないでください。五件に一件はソースが健全です。特に-O0や変わった最適化レベルでビルドしているなら、コンパイラのloweringを疑う統計的な理由があります。

エラー文字列で検索して出てきた答えをそのまま信じないでください。invalid mem access 'scalar'は原因9種類を隠します。Stack Overflowで同じメッセージに付いた回答があなたのケースに当てはまる確率は、思っているより低いです。

LLMに投げるなら、ログだけを投げないでください。この論文が示したのは、診断の質が修復の成功率を左右するということです。どの証明が必要で、どこで消えたのかという文脈を人間が先に絞り込んでやれば、結果は変わります。

おわりに

この論文が価値を持つのは、新しい事実を教えてくれるからではありません。eBPF開発者がすでに体で知っていたことを数字にしたからです。verifierのエラーが役に立たないことは誰もが知っていましたが、47%がEINVALで、一つのエラー文字列が原因9種類を隠していることは誰も知りませんでした。

そして、診断がこれほど難しい根本理由が構造的だという点が興味深いです。Rustのコンパイラは自分が作った型付けの制約をたどることでエラーを説明できます。eBPF verifierはそうしたアーティファクトを残しません。残るのはログだけです。bpfixがやっていることは結局、そのログをアーティファクトへ戻す逆工学です。うまい解法ですが、そもそもverifierが証明の構造を外に出していれば必要なかった作業でもあります。長期的にこのギャップが本当に閉じる道は、カーネル側にあるはずです。

当面はbpfixが生まれて五日の0.1.0であり、改善幅は著者自身の測定であり、一つのツールチェーンで測った数値です。だから本稿の結論は「bpfixを使いましょう」ではありません。verifierが止まった地点と、あなたのバグがある地点は違う — これを明示的に知ったうえでログを読み始めるだけでも、次のinvalid mem access 'scalar'の前で費やす時間は減るはずです。

参考資料

• Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections (Zhengら、arXiv:2607.02748、2026年7月2日)
• eunomia-bpf/bpfix — 論文のツール実装(MIT、v0.1.0 / 2026年7月11日)
• BPF loop verification with scalar evolution (Daroc Alden、LWN、2026年6月9日)
• libbpf/bpfvv — BPF Verifier Visualizer
• eBPF verifier — カーネル公式ドキュメント
• eBPF基礎完全制覇 — プログラム、マップ、そしてVerifierの世界(関連記事)