Split View: eBPF Verifier는 멈춘 곳만 알려준다 — 거부 235건을 재현해 측정한 진단 격차

The eBPF Verifier Only Tells You Where It Stopped — Measuring the Diagnostic Gap Across 235 Reproduced Rejections

• Introduction — The Error Points to Where It Stopped; the Bug Is Somewhere Else
• What Is the Diagnostic Gap — Loss Point vs. Stop Point
• Building the Dataset — From 936 Candidates to 235 Rejections
• Finding 1 — 19% of Rejections Have Perfectly Fine Source
• Finding 2 — 12 Root-Cause Categories, 10 of Them eBPF-Specific
• Finding 3 — One Error String, Nine Root Causes
• Why Existing Tools Don't Close the Gap
• bpfix — Reconstructing the Proof's Lifetime from the Log
• A Real Case — aya Issue 1002
• Can LLMs Fix Verifier Errors — bpfix-bench
• How Far Should You Trust These Numbers
• Meanwhile, the Verifier Itself Is Changing
• So What Should Practitioners Do
• Closing
• References

Introduction — The Error Points to Where It Stopped; the Bug Is Somewhere Else

Anyone who has written an eBPF program in earnest even once knows this feeling. You clearly bounds-checked the packet pointer, and yet a load instruction much later throws R5 invalid mem access 'scalar'. The line the error points to has nothing suspicious about it. So what do you do — you edit whatever looks editable, reload, and if it bounces again, edit something else. This is the point where eBPF development turns into a loop of trial and error.

As covered in eBPF Fundamentals — Programs, Maps, and the World of the Verifier, the verifier's reason for existing is clear. To run arbitrary code inside the kernel, someone has to prove it is safe, and the verifier does that proof on your behalf. The problem is how the verifier explains the failure when the proof fails.

Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections (Zheng et al., arXiv:2607.02748), posted to arXiv on July 2, 2026, is the first paper to properly measure that frustration. The authors are affiliated with UC Santa Cruz, Virginia Tech, Telecom Paris, University of Washington, University of Connecticut, and eunomia-bpf.

One sentence from the paper sums up the whole thing — the error reports only where verification stopped, not where the program lost the proof the verifier required.

What Is the Diagnostic Gap — Loss Point vs. Stop Point

This distinction is the core of the whole post, so let's go through it slowly.

The verifier walks instruction by instruction, building up a proof for each value that says "this value can be used safely." For a packet pointer, for instance, that proof is "this pointer stays within bounds." The moment an instruction tries to use a value without that proof in hand, verification stops right there and the program is rejected.

But the point where the proof disappears and the point where the proof becomes needed are usually different. The paper's execution example makes this vivid. At some intermediate state, R5 is pkt(off=34,r=42) — a packet pointer carrying bounds information. But in the state right before instruction 37, that same R5 is represented as the scalar value 40. And instruction 37 dereferences R5.

• Where the proof was lost: somewhere the packet pointer turned into a scalar (what the paper calls the loss point)
• Where verification stopped: instruction 37 (the only place the error names)

The error tells you only the latter. The place the developer needs to fix is the former. In the paper's words, the fix has to restore the lost proof, yet the error only names the operation that needed that proof. So the developer has to manually reconstruct, from the trace, which proof was needed and where it vanished.

Building the Dataset — From 936 Candidates to 235 Rejections

The paper's empirical section is honest because it doesn't hide its methodology.

The authors gathered 936 candidates from four sources — Stack Overflow questions, GitHub issues, GitHub fix commits, and kernel selftests. Each candidate was then rebuilt on one fixed toolchain: kernel 6.15.11, clang 18, log level 2. (6.15 is a mainline-series stable point release that shipped in May 2025.)

Of the 936, only 235 were actually rejected under this build, and those 235 became the bpfix-empirical dataset. The reasons the rest fell out are stated too — they weren't rejected under the authors' toolchain, they required a specific environment, or there was no source left to rebuild.

Each case comes paired with the problem source and the fix the original developer actually applied. This matters: the answer to "what was the real root cause" isn't the authors' guess — it comes from the actual fix left in the original report.

Finding 1 — 19% of Rejections Have Perfectly Fine Source

The first surprise comes from classifying the 235 cases by "where the fix landed."

• 191 cases (81%): the fix changed the program source — a genuine program bug.
• 44 cases (19%): the source was correct but got rejected anyway. The fix landed on a different layer — the compiler in 18, the environment in 14, the verifier itself in 12.

The paper's example here is striking. A plainly safe context-field read gets rejected, because -O0 lowers that read into a scalar, so the verifier can no longer see the pointer's provenance. The fix is a compiler flag that never touches the source. The code in the paper's Figure 2 is this simple.

// Correct source. -O0 lowers the field read to a scalar
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'

This matters quite a bit in practice. A verifier rejection does not mean your code is wrong. Roughly one time in five, the code is fine, and either the compiler obscured the proof, the environment doesn't match, or the verifier just doesn't understand that pattern yet. The error message, though, does not distinguish between the two.

Finding 2 — 12 Root-Cause Categories, 10 of Them eBPF-Specific

The 191 genuine bugs break down into 12 root causes. Here, "root cause" does not mean the check the verifier failed on — it means the mistake the developer made at the source level.

The paper's point is that 10 of these 12 are eBPF-specific. Proving packet bounds, or handling a dynptr correctly paired with its lifetime, is not something general C programming knowledge gets you to. So fixing them takes domain knowledge, not general programming skill. Missing null checks are the exception — about the only category that's generically familiar.

This is also a quantitative explanation for why the eBPF learning curve is so steep. Most of these problems are not the kind you solve by just writing better C.

Finding 3 — One Error String, Nine Root Causes

This is where the most painful number shows up.

First, errno tells you almost nothing. 47% of all rejections return nothing but EINVAL. Nearly half get lumped into an error code that just means "something went wrong."

Second, the error strings themselves are too coarse. The authors masked out register numbers and offsets from each error string, normalized them, and grouped the 235 cases. 167 distinct strings collapse into 82 templates. And of those 82 templates, 15 each correspond to more than one root cause.

The worst offender is the first row of the table below.

invalid mem access 'scalar' alone hides 9 distinct root causes across 28 cases. Believing you can narrow down the cause from this message has no statistical basis. To quote the paper's takeaway directly — terminal errors are too coarse to guide a fix.

Why Existing Tools Don't Close the Gap

You might ask whether tools already exist for this. The paper points to two.

PrettyVerifier (Rizza et al., 2025 IEEE CSR) uses regular expressions to map terminal errors to source lines and hints. BPF Verifier Visualizer (bpfvv) is a front end that interactively renders per-instruction state. The bpfvv repository itself describes it as a primitive debugger UI — one that interprets the log, not runtime state.

The paper's verdict is this — both help the developer read the error, but neither points to where the proof was lost.

And the explanation for why this is hard is sharp. Error-explanation tools for languages like Rust can walk the structures the checker already built — the AST, the typing constraints. But the eBPF verifier exposes no such artifact. All that's left is the log.

bpfix — Reconstructing the Proof's Lifetime from the Log

So the authors built bpfix. The core insight is this — at log level 2, the verifier dumps the full abstract state for every instruction. The lost proof is already alive inside the log. No one is reading it, that's all.

bpfix is about 23,000 lines of Rust, and its only required input is the existing verifier log. Source or object metadata is optional — supplying it just improves the instruction-to-source mapping. The pipeline has three stages.

1. Log parsing — extract the terminal error and the per-instruction abstract state into a normalized evidence stream.
2. Proof reconstruction — map the terminal error to a proof family — things like pointer provenance, packet bounds, scalar range — and track when the evidence for that proof holds, is maintained, and disappears.
3. Diagnostic generation — pick spans and produce instructions for re-establishing the proof.

The output is a plain-text, Rust-style diagnostic. It consists of a stable error identifier, the required proof, the relevant spans and evidence, the loss point when it is observable, and a help: instruction. The "when it is observable" caveat is the authors' own — it doesn't always catch it.

Another practical feature is layer-of-blame separation. bpfix labels a rejection as source_bug (the source layer) or lowering_artifact (the compiler layer) — a feature that directly addresses the "19% have a clean source" problem seen earlier. The paper, though, explicitly calls this best-effort attribution.

The paper's Figure 5 shows this point exactly. Two rejections both end in the identical terminal message invalid mem access 'scalar', yet one is a source bug (Stack Overflow 56965789 — casting an integer offset to a pointer without a packet base) and the other is a compiler lowering artifact (Stack Overflow 53136145 — a branch merge obscures the packet pointer type). The layer where the fix must land is completely different, but the verifier message is identical.

A Real Case — aya Issue 1002

Let's look at one concrete example the paper gives — a program that casts the address of the map object &globals to __u64 * and reads and writes it directly.

// Rejected program
__u64 *raw_map = (__u64 *)&globals;  // map object pointer
__u64 v = *raw_map;
*raw_map = v + 1;                    // rejected here

// verifier: only read from bpf_array is supported

The verifier message isn't wrong. It just states the symptom — it saw a write through the map object. It doesn't say why that's not allowed, or what to do instead.

bpfix's diagnostic reads like this — the map pointer is being accessed like ordinary memory (source_bug); the proof needed is deriving a map-value pointer through the appropriate map helper before reading or writing the map contents; the next action is to look up the element and then write through that pointer.

And the developer's actual fix follows that diagnosis exactly.

// Developer's actual fix
__u32 key = 0;
__u64 *v = bpf_map_lookup_elem(&globals, &key);
if (!v) return 0;
*v += 1;

Can LLMs Fix Verifier Errors — bpfix-bench

The paper's final axis is the question people actually care about these days. You're going to throw the error log at an LLM anyway — does that even work?

The authors built a benchmark called bpfix-bench: 75 source-level repair tasks, of which 40 were constructed around specific verifier proofs and 35 were minimized and pulled from open-source projects like Cilium, xdp-tools, and bpftrace.

The scoring method is honest. Each task ships with an executable test suite that is independent of bpfix. For a fix to be credited, it must (1) load by passing the real kernel verifier, (2) pass the functional tests, and (3) pass a source-semantics check. Plausible-looking text alone earns no score, and the common trick of breaking the logic just to dodge the verifier gets caught by the source-semantics check.

The models are Qwen3.6 27B (primary), GLM 5.2 (hosted), and Qwen2.5 3B, all at temperature 0. The 3B model is included to see whether the gain survives on a smaller model. The results are below (all out of 75 problems, author-measured).

Two things stand out.

First, current models don't do well when given only the raw verifier log. Single-shot success ranges from 0% to 37%. In the paper's words, across three models from 3B to 27B, verifier rejections remain hard even for capable models.

Second, swapping the log for a bpfix diagnostic improves things. The range the paper's abstract claims is 11–21 points. On a single-shot basis, Qwen3.6 sees the largest gain at 21.4 points, Qwen2.5 3B gains 10.7 points, and GLM 5.2 gains 13.4 points. Note, though — and this you have to check against the table yourself — GLM 5.2's gain in retry mode is much smaller, at 6.6 points. The abstract's range is correctly read as the single-shot figures.

The authors also broke down at which stage failures disappear, and this is actually more convincing. For Qwen3.6 27B, verifier-load failures dropped from 19 to 10, and source-semantics failures dropped from 22 to 16. GLM 5.2 moves the same direction (10 → 5, 25 → 22). Compile failures stayed low on both sides.

The small-model story is worth looking at separately. With the raw log, Qwen2.5 3B fixed none of the 75 problems. Of the single-shot candidates, 62 failed at verifier load, and 3 prompts blew past the context window entirely and returned no program at all. Given the shorter bpfix diagnostic, the model-call failures disappear and load failures drop to 39, but compile failures rise from 7 to 14. The authors' own interpretation is honest — bpfix gives even a small model enough verifier-related information to attempt a more meaningful fix, but ordinary code-generation mistakes remain.

How Far Should You Trust These Numbers

From here on, these are the limitations the paper states itself, plus reservations I'm attaching as I read it. Let me be clear up front that most of the numbers in this post are author-measured. bpfix and the benchmark were both built by the same team.

The selection effect is significant. Only 235 of the 936 candidates survived. They survived because they reproduced under the authors' fixed toolchain, and a good share of the 701 that fell out were environment-dependent or had no source to rebuild. And the data sources are Stack Overflow and GitHub issues to begin with — rejections confusing enough that someone bothered to post a question are overrepresented. The sample could be tilted toward a conclusion favorable to "diagnostics are inadequate." That said, kernel selftests and fix commits are mixed in too, so it isn't pure bias, and there's a valid counter-argument that confusing rejections like these are exactly what actually stops people in practice.

The toolchain is pinned to a single version — kernel 6.15.11, clang 18. The verifier changes with every release, and error messages and pruning behavior in particular keep getting tweaked. You should not assume the 47% measured on 6.15 holds on the latest kernel.

The model selection is limited — Qwen3.6 27B, GLM 5.2, and Qwen2.5 3B. No frontier-tier model is in the evaluation. So the accurate statement is not "LLMs can't fix verifier errors" but "these three models fixed 0–37% given the raw log."

And even with bpfix, the ceiling stays low. The best score is 50.7% single-shot, 69.3% with a retry added. The direction — better diagnostics mean better repairs — held consistently across all three models, but it's still a long way from "you can just hand this to an LLM now."

Tool maturity has to be factored in too. The bpfix repository is open under the MIT license, and v0.1.0 shipped on July 11, 2026 — a five-day-old 0.1.0. The README itself explicitly states it is not a kernel patch, not a verifier replacement, and not an automatic source-repair tool. It's a diagnostic-explanation tool. That's the right level of expectation to bring before putting it into a production pipeline.

Meanwhile, the Verifier Itself Is Changing

If this paper's approach is "read the log better," the other side of the coin is the movement to "make the verifier reject less in the first place."

Eduard Zingerman's work, covered by LWN's BPF loop verification with scalar evolution (Daroc Alden, June 9, 2026), is one example. It's work in progress presented at the 2026 LSFMM+BPF Summit, and the goal, in Zingerman's own words, is to make the verifier handle a typical for/while loop in a single pass instead of iterating through the loop.

Today, when the verifier meets a loop, it evaluates every iteration until the termination condition is reached, and in the process it can spuriously hit the instruction-count limit — a limit a better implementation wouldn't have tripped. Scalar evolution is a technique meant to avoid this by computing the range of values a loop variable can take.

But this is still a prototype and unmerged. It cannot yet handle registers spilled to and restored from the stack, and it doesn't analyze every loop variable uniformly. Zingerman said he plans to propose it for kernel submission after adding support for stack manipulation, signed integer arithmetic, and more complex loops. He himself said he has not done a rigorous measurement of load time. (Starovoitov noted that similar verifier changes in the past raised concerns at first but ultimately ended up making load times faster and reducing memory use.)

The two currents are two sides of the same problem — one reduces rejections, the other makes a rejection understandable when it happens. And the latter is never going away. However smart the verifier gets, some rejections will remain, and the ones that remain will need explaining.

So What Should Practitioners Do

There are things you can take from this paper even without adopting any tool.

Make log level 2 your default. The very reason bpfix can exist is that "the information you need is already in the log." At level 2, the verifier dumps the abstract state for every instruction. If you're not turning that on, you're throwing away the raw material for diagnosis.

Don't trust the terminal error line. That's where verification stopped. The bug is where the proof disappeared. What you actually have to do is walk the log backward and find the last point the offending register had the right type — the point where pkt(off=..,r=..) turned into scalar, for instance.

Don't automatically blame yourself for a rejection. One in five have a perfectly clean source. If you're building with -O0 or an unusual optimization level in particular, there's statistical grounds to suspect compiler lowering.

Don't take an answer you found by searching the error string at face value. invalid mem access 'scalar' hides 9 root causes. The odds that a Stack Overflow answer attached to the same message applies to your case are lower than you'd think.

If you're handing this to an LLM, don't hand it just the log. What this paper showed is that diagnostic quality governs repair success. Narrowing the context yourself first — what proof was needed, where it disappeared — changes the outcome.

Closing

This paper is valuable not because it tells us something new, but because it put numbers to something eBPF developers already knew in their gut. Everyone knew verifier errors weren't helpful, but no one knew that 47% is EINVAL, or that one error string hides 9 root causes.

And it's interesting that the underlying reason diagnosis is this hard is structural. The Rust compiler can explain an error by walking the typing constraints it built itself. The eBPF verifier leaves behind no such artifact. Only a log. What bpfix ultimately does is reverse-engineer that log back into an artifact. It's a neat solution, but also one that wouldn't be necessary if the verifier had exposed its proof structure in the first place. Over the long run, the real path to closing this gap probably runs through the kernel side.

For now, bpfix is a five-day-old 0.1.0, the improvement figures are author-measured, and they're measured on a single toolchain. So this post's conclusion isn't "go use bpfix." It's this — where the verifier stopped and where your bug actually is are two different places. Just starting to read the log knowing that explicitly should cut down the time you spend in front of the next invalid mem access 'scalar'.

References

• Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections (Zheng et al., arXiv:2607.02748, July 2, 2026)
• eunomia-bpf/bpfix — the paper's tool implementation (MIT, v0.1.0 / July 11, 2026)
• BPF loop verification with scalar evolution (Daroc Alden, LWN, June 9, 2026)
• libbpf/bpfvv — BPF Verifier Visualizer
• eBPF verifier — official kernel documentation
• eBPF Fundamentals — Programs, Maps, and the World of the Verifier (related post)