The eBPF validator within DPDK exists to do one job: never let an unsafe program execute on the data plane. A soundness bug in it may lead to a security exploit.

Last year, Konstantin Ananyev, Marat Khalili, and I were chatting about good targets for formal verification, and lib/bpf/bpf_validate.c was the obvious one. We then did what teams often do with good ideas that need real effort: we postponed it, because the cost of starting felt too high.

I’m not a DPDK engineer, but I know which questions to ask about a piece of critical code and which tools can answer them. So, one afternoon in March, I started poking at bpf_validate.c on my own anyway, for fun. I wanted to see what a coding agent could do if I let it write the harnesses and run the tools with minimal oversight.

I had the agent set up CBMC and ESBMC harnesses for one foundational property, range invariant preservation, across the validator’s 27 range-tracking functions. It surfaced about 25 candidate findings. Marat then spent several days triaging them: separating real bugs from duplicates and false positives, rewriting fixes where his judgment differed from the agent’s, and submitting the first batch of ~15 confirmed bugs upstream. Today, we presented the work at the DPDK Summit, in Stockholm:

A closer look

The validator is about 2.2k lines of C code implementing abstract interpretation over eBPF programs. The verifier walks the program statically, maintaining for each register an interval of possible values. The bulk of the abstract interpretation happens in 27 range-tracking functions, one per eBPF operation (eval_add, eval_mul, eval_divmod, and so on), plus call graph construction, jump-condition refinement, and an instruction validation table for the allowed opcodes.

I started by instructing the agent to write both fuzz tests and property-based tests for a couple of functions, one at a time. This proved so easy that I didn’t dig in. Instead, I skipped directly to model checking with CBMC and ESBMC. In my mind, an incremental climb from lightweight to heavyweight tools makes sense only when the harder tools are expensive to set up. As they were not, for me and the agent, I figured I might as well start with model checking.

I picked the simple property ∀ ranges r: r.s.min ≤ r.s.max ∧ r.u.min ≤ r.u.max, which states that for all ranges, the signed (s) and unsigned (u) intervals are well-formed. If those bounds ever invert (min > max), the validator’s abstract model has lost contact with reality, and every downstream decision based on that range is unsound. To check that the property holds, I used two bounded model checkers, CBMC and ESBMC. Bounded model checkers explore every possible input within a fixed bound and either find a violation or confirm none exists within that bound. The agent wrote self-contained harnesses, one per range-tracking function, isolated from the original codebase. It ran the checkers, interpreted the raw counterexamples, produced minimal reproducible test cases, and wrote a report for each finding.

Here’s one example: in eval_divmod, the signed division path looks like this:

/* ... */
if (rd->s.min == rd->s.max && rs->s.min == rs->s.max) {
    if (rs->s.max == 0) return "division by 0";
    if (op == BPF_DIV) {
        rd->s.min /= rs->s.min;
        rd->s.max /= rs->s.max;
    }
    /* ... */
}

ESBMC returned a counterexample with rd.s.min = rd.s.max = INT64_MIN and rs.s.min = rs.s.max = -1. Dividing INT64_MIN by -1 overflows a signed 64-bit integer, which is undefined behaviour in C, and on x86 sends SIGFPE. The validator could crash. The agent’s proposed fix was to add a guard for the INT64_MIN / -1 case, widening the result to top (the full signed range) when the corner case fires. After applying the fix, I asked the agent to verify it under deductive verification using Frama-C with the WP plugin, which proves the property holds for all inputs, not just within ESBMC’s exploration bound. The proof went through. The fix preserved range invariant preservation.

Except: while reviewing the fix, Marat spotted something deeper. DPDK doesn’t actually implement signed division at the bytecode level. The validator was checking abstract-domain semantics that the runtime doesn’t have. The agent had verified what I’d asked. It hadn’t validated that I’d asked the right thing. Nobody told it to. This is the structural limit of AI-assisted verification: the agent compresses execution beautifully, but it can’t choose the right properties.

Not all confirmed bugs made it into the first upstream batch. The most interesting one, in eval_apply_mask, is still pending. When a 64-bit register whose signed lower bound exceeds INT32_MAX is used in a 32-bit ALU operation, the function clamps s.max down to INT32_MAX but leaves s.min at its original value above it. The signed range becomes inverted: s.min > s.max. Fifteen downstream functions then read that inverted range and make decisions on it. The consequence: a check like rd->s.min >= 0 returns true on a register whose concrete value can in fact be negative, enabling a “this is safe” verdict on a register that, used as a pointer offset, is not. Fixing this in eval_apply_mask alone creates more problems than it solves, because mask semantics are reinterpreted differently across the file. The fix is a coordinated refactor, not a patch. What the verification surfaced here isn’t a bug. It’s a design inconsistency that years of testing hadn’t exposed, because it only manifests on inputs no test had thought to try.

What’s next?

We verified one property out of many that soundness requires: termination, memory safety, type safety, pointer subtyping, definite initialisation, and control-flow safety all remain. There’s a real project here, which we haven’t chartered yet.

One property down. The validator is sounder than it was last month. Whether it’s sound is the question we haven’t answered yet.

Thanks to Marat for the careful review and thorough validation that turned candidate findings into landed fixes, and to Konstantin for presenting our work at the DPDK Summit. More details in the slides attached and in the DPDK livestream.