BPFix: making eBPF verifier errors more friendly

BPFix makes eBPF verifier errors feel closer to Rust compiler errors.

The Linux eBPF verifier is powerful, but its failure logs are hard to read. BPFix is a userspace diagnostic tool for that problem. It reads verifier logs from your existing workflow and turns them into source-level explanations that point to where the verifier lost the required proof.

Quick Start

Install bpfix and load the prebuilt verifier failure:

cargo install bpfix
sudo bpftool -d prog load examples/bpftool/quick-start.bpf.o /sys/fs/bpf/bpfix-demo 2>&1 | tee verifier.log

The command loads a real verifier failure from bpfix-empirical (stackoverflow-53136145). The source parses either IPv4 or IPv6, derives a UDP header pointer on each branch, checks the UDP header against data_end, and then reads the destination port:

if (ethertype == ETH_P_IP) {
    ipv4_hdr = (void *)eth + ETH_HLEN;
    if ((void *)(ipv4_hdr + 1) > data_end)
        return 1;
} else if (ethertype == ETH_P_IPV6) {
    ipv6_hdr = (void *)eth + ETH_HLEN;
    if ((void *)(ipv6_hdr + 1) > data_end)
        return 1;
} else {
    return 2;
}

if (ipv4_hdr)
    udph = (void *)ipv4_hdr + sizeof(*ipv4_hdr);
else
    udph = (void *)ipv6_hdr + sizeof(*ipv6_hdr);

if (udph + sizeof(struct udphdr) > data_end)
    return 1;

dst_port = __constant_ntohs(((struct udphdr *)udph)->dest);

That source shape is normal BPF C: the developer made the packet proof explicit. The failure is in the verifier-visible proof lifecycle. One replay path reaches the shared udph->dest load with r5 as a scalar instead of a packet pointer:

from 31 to 34: ... R5_w=40 ...
; if (udph + sizeof(struct udphdr) > data_end) @ prog.c:267
34: (bf) r3 = r5                      ; R3_w=40 R5_w=40
35: (07) r3 += 8                      ; R3=48
36: (2d) if r3 > r2 goto pc+4         ; R2=pkt_end() R3=48
; dst_port = __constant_ntohs(((struct udphdr *)udph)->dest); @ prog.c:270
37: (69) r2 = *(u16 *)(r5 +2)
R5 invalid mem access 'scalar'

bpfix verifier.log

The raw log says where the verifier stopped, but not the source-level proof story. BPFix turns the trace into a Rust-style multi-span diagnostic:

error[BPFIX-E006]: verifier-visible compiler lowering hides the required proof
  = class: lowering_artifact
  = confidence: medium
  = diagnostic: supported, help: repair_hint, span: exact_pc
  = next action: provenance
  --> prog.c:270
   |
263 | if (ipv4_hdr)
    | ------------- nearby source context for pointer provenance
267 | if (udph + sizeof(struct udphdr) > data_end)
    | -------------------------------------------- verifier state changes from pkt to scalar before the rejected access
270 | dst_port = __constant_ntohs(((struct udphdr *)udph)->dest);
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ rejected here: verifier sees a scalar where a pointer is required
   |
   = verifier[229]: R5 invalid mem access 'scalar'
   = note: nearest BPF instruction pc 37
   = note: parsed 60 verifier state snapshots
   = note[lowering]: compiler-lowered control flow hides an established packet-pointer proof
   = required proof: preserve a verifier-recognized pointer type at the operation that requires a pointer
help: Reacquire a verifier-tracked pointer before the rejected dereference.
help: Use the packet pointer that received the data_end proof, or rederive and recheck it before the load.
help: Keep the final access on a verifier-tracked pointer; rederive it from a checked base after scalar work.

This is the kind of failure that motivates the project: the program is not missing a generic "add a bounds check" hint. The useful answer is the proof lifecycle: where a verifier-recognized pointer proof exists, where branch-local provenance can be merged away, and where the rejected instruction finally needs that proof.

BPFix overview

The example object is copied from bpfix-empirical/cases/stackoverflow-53136145/prog.o; replace it with the object you are debugging in your own project.

Stable CLI Contract

The 0.1.x CLI contract is intentionally small:

bpfix [OPTIONS] [LOG]

LOG can be a verifier, build, bpftool, libbpf, Aya, or BCC log. When LOG is omitted or -, BPFix reads stdin. Positional input and stdin are always log text. Supported public options are --object <OBJECT>, --doctor, --fail-on-unsupported, --help, and --version. The output is plain text; there is no stable JSON output mode in 0.1.x.

BPFix does not execute loader commands in the default path, and there is no default command-execution workflow. Empirical corpus YAML and Docker-based execution are explicit non-default modes; if Docker support is added, it should be selected with an option such as --docker, not inferred from LOG.

Best Workflow

The best user experience is to keep your current BPF workflow and let BPFix explain the verifier log it already produces:

make load 2>&1 | tee verifier.log
bpfix verifier.log

or:

sudo bpftool -d prog load examples/bpftool/quick-start.bpf.o /sys/fs/bpf/bpfix-demo 2>&1 | tee verifier.log
bpfix verifier.log

with feature-gated object metadata, after installing with --features object-analysis:

bpfix --object examples/bpftool/quick-start.bpf.o verifier.log

BPFix does not need case.yaml for normal use. Empirical corpus YAML records are evaluation fixtures; use the evaluation scripts when measuring the bundled corpus.

Check the local rebuild/load environment without reading a log:

bpfix --doctor

Agent Skill

skills/ebpf-verifier-repair/ is a portable agent skill for end-to-end eBPF verifier repair. It works directly from BPF source plus a verbose verifier log; BPFix diagnostics are optional structured evidence, not a runtime dependency. The skill includes raw-log triage, semantic-preservation and retry workflows, repair patterns, and a script for compacting oversized verifier traces without modifying the original log.

Install the Agent Skill for Codex, GitHub Copilot, or another supported agent with GitHub CLI 2.90 or newer:

gh skill install eunomia-bpf/bpfix ebpf-verifier-repair --agent codex --scope user

For Claude Code, add this repository's marketplace and install the same skill as a namespaced plugin:

/plugin marketplace add eunomia-bpf/bpfix
/plugin install ebpf-verifier-repair@eunomia-bpf

The Agent Skill, Codex plugin, and Claude plugin share the same SKILL.md, scripts, and references. The plugin manifests do not duplicate the repair instructions.

Validate the skill and its frozen 75-case prompt surface with:

python3 "${CODEX_HOME:-$HOME/.codex}/skills/.system/skill-creator/scripts/quick_validate.py" skills/ebpf-verifier-repair
python3 -m unittest bpfix-bench/tools/test_run_suite.py -v
python3 bpfix-bench/tools/run_suite.py \
  --split bpfix-bench/splits/main.txt \
  --expected-count 75 \
  --mode skills \
  --prompt-only

The full user workflow is documented in docs/user-guide.md. More copyable integration snippets live in examples/.

Project Status

The maintained implementation is the Rust workspace:

crates/
  bpfix/        command-line diagnostic tool
  bpfanalysis/  verifier-log and BPF bytecode analysis primitives

The earlier Python version has been removed from the maintained tree. Python scripts that remain under bpfix-empirical/tools/ are empirical replay and corpus maintenance helpers, not a second BPFix implementation and not part of the public CLI.

The public CLI design lives in docs/open-source-tool-design.md, and the full user workflow is in docs/user-guide.md. Evaluation methodology and project planning notes live under docs/evaluation/ and docs/project-status.md; they are supporting material, not required reading for normal use.

bpfix-bench/ contains the frozen BPFix-Bench main75 LLM repair benchmark. It is a source-first benchmark: a repair succeeds only when the candidate BPF C file compiles, loads through the kernel verifier, and passes the case oracle. Start with bpfix-bench/README.md for the benchmark contract and docs/evaluation/bpfix-bench-llm-repair-eval.md for the reported raw-log versus BPFix-diagnostic results.

The default bpfix CLI uses the verifier-log parser from bpfanalysis. Object/CFG analysis is behind the object-analysis Cargo feature; that path uses libbpf-sys and the vendor/libbpf submodule for BPF instruction and program-type constants.

The current user-facing pipeline is log-first: bpfix parses verifier state snapshots, instantiates the required verifier proof from the terminal error and verifier state, extracts proof lifecycle events, and maps them back to source comments when the log contains BTF/source annotations. Packet bounds, scalar range, nullable pointer, stack readability, reference lifecycle, helper capability, and pointer-provenance failures now produce parameterized proof requirements instead of only terminal-error categories. When built with --features object-analysis, the CLI accepts --object prog.o, builds ProgramCFG summaries, and correlates verifier-state PCs with CFG sites when the object section layout matches the loaded verifier program. Full BTF source correlation is the next analysis layer, not a runtime requirement for the basic CLI.

What BPFix Handles

Current diagnostics focus on common verifier failures:

  • packet bounds checks
  • nullable map value pointers
  • uninitialized stack reads
  • reference lifetime leaks
  • scalar range and variable-offset problems
  • pointer type/provenance loss
  • verifier-visible compiler lowering artifacts
  • verifier precision limits and likely false positives
  • verifier complexity and loop limits
  • missing kernel/helper/program-type support
  • dynptr lifetime and bounds issues

Non-Goals

BPFix is not:

  • a kernel patch
  • a verifier replacement
  • an automatic source-code repair tool
  • a semantic correctness checker for accepted BPF programs

It explains why the verifier rejected a program and what proof the developer probably needs to make explicit.

Development

Run tests:

cargo test --workspace

Check the workspace:

cargo check --workspace

Run the same lint gate used by CI:

cargo clippy --workspace --all-targets --all-features -- -D warnings

Format code:

cargo fmt --all

Run a smoke test:

cargo run -p bpfix -- bpfix-empirical/cases/stackoverflow-60053570/replay-verifier.log

Check release packaging:

make release-check

This runs packaging checks, example consistency checks, the empirical corpus --reject-fallback gate, and the feature-gated object-analysis CLI tests.

Release automation and the manual fallback are documented in docs/release.md. bpfix depends on the sibling bpfanalysis crate; the publish workflow selects the next unpublished patch version, publishes bpfanalysis first, waits for it to appear in the crates.io index, and then publishes bpfix.

Repository Layout

bpfix-empirical/       replayable verifier-failure corpus and raw examples
crates/bpfanalysis Rust analysis library
crates/bpfix       user-facing CLI
docs/project-status.md project planning and evaluation notes
docs/user-guide.md    install, getting logs, output, and CI usage
docs/open-source-tool-design.md public CLI contract
docs/release.md       release gates and crates.io publishing process
examples/          bpftool, libbpf, Aya, BCC, CI, and editor integration snippets
docs/evaluation/   evaluation and metric notes
bpfix-empirical/tools/ empirical replay and corpus-maintenance tools
vendor/libbpf/     libbpf submodule