Pith. sign in

REVIEW 2 major objections 5 minor 28 references

eBPF rejections stop where the proof was already lost; localizing that loss is what makes repair work.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-12 07:18 UTC pith:JZB4JT5Y

load-bearing objection Solid eBPF systems paper: real diagnostic gap quantified, practical localization tool, and LLM gains that are useful even if not fully isolated from prompt structure. the 2 major comments →

arxiv 2607.02748 v1 pith:JZB4JT5Y submitted 2026-07-02 cs.OS cs.PLcs.SE

Characterizing and Bridging the Diagnostic Gap in eBPF Verifier Rejections

Yusheng Zheng , Zhengjie Ji , Weichen Tao , Xiangyu Gao , Jianchang Su , Wei Zhang , Andi Quinn , Dan Williams This is my paper
classification cs.OS cs.PLcs.SE
keywords eBPFverifier rejectionsproof localizationdiagnostic gapLLM program repairkernel extensionsbpfix
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

When the Linux eBPF verifier rejects a program, its terminal error names only the instruction where checking stopped, not the earlier place where the program stopped carrying the safety proof the verifier needed. An empirical study of 235 real rejections shows the practical damage: nearly half return only EINVAL, one error string can cover nine different root causes, and most of those causes are eBPF-specific, so developers need both domain knowledge and a way to find the lost proof. The paper introduces bpfix, which reads the verifier's per-instruction abstract-state log, reconstructs when the required proof was established and when it was lost, and emits a Rust-style diagnostic that points at that loss. On a 75-task repair benchmark, large language models fix only 0–37% of cases from the raw log; feeding them bpfix's localization instead lifts success by 11–21 percentage points, with the biggest gains at the stages that actually restore verifier-visible proofs. The central claim is therefore that repair hinges on locating the lost proof, not merely reading the rejection line.

Core claim

The terminal verifier error is too coarse to guide repair: it reports where verification stopped, not where the required proof was lost. Reconstructing that proof lifecycle from the existing per-instruction log closes the gap, and the resulting localization measurably improves both human-facing diagnostics and automated LLM repair.

What carries the argument

bpfix's proof reconstruction: from the verifier log it maps the terminal error to a required proof family (pointer provenance, packet bounds, scalar range, etc.), tracks when evidence for that proof appears and becomes incompatible, and surfaces the observed loss point together with a Rust-like diagnostic.

Load-bearing premise

The verifier's ordinary per-instruction abstract-state log already contains enough register and type transitions for the tool to see when the needed proof was established and when it was lost.

What would settle it

Run the same 75-task repair benchmark with models that receive either the raw verifier log or a deliberately incomplete bpfix diagnostic that omits the loss-point localization; if the 11–21 point gain disappears, the claim that locating the lost proof is what drives repair fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper studies the diagnostic gap in eBPF verifier rejections: the terminal error marks where verification stopped, not where the program lost the required safety proof. From 235 rejections reproduced under a fixed toolchain (kernel 6.15.11, clang 18), it reports that 47% return only EINVAL, one normalized error template maps to as many as nine root causes, and 10 of 12 root causes are eBPF-specific; 191 cases are program bugs and 44 reject correct source due to compiler, environment, or verifier issues. It presents bpfix, which parses log_level=2 per-instruction abstract states to reconstruct proof establishment, loss, and rejection location and emits a Rust-like diagnostic. On bpfix-bench (75 repair tasks with verifier-independent functional and source-semantics tests), three LLMs achieve 0–37% one-shot success with the raw log; replacing the log with the bpfix diagnostic improves one-shot repair by 11–21pp, with the largest reductions at verifier-load and source-semantics failure stages.

Significance. If the results hold, the paper makes a concrete, systems-relevant contribution: it quantifies a real developer pain point with a reproducible corpus, shows that existing pretty-printers do not close the localization gap, and supplies both a practical tool (bpfix, open-sourced) and an external repair benchmark whose acceptance criteria do not depend on bpfix. The stage-wise failure breakdown and the separation of source_bug vs lowering_artifact layers are useful beyond the LLM setting. The work is timely given growing eBPF adoption and the difficulty of verifier-facing repair even for capable models.

major comments (2)
  1. §5.2, Figure 6, Table 3: The central claim that “locating where the proof was lost is key to guiding repair” is not cleanly isolated by the current design. The raw log is a long, low-level instruction trace; the bpfix diagnostic is shorter, structured, and already names the required proof, loss point, class, and next action. For Qwen2.5 3B the raw log also produces three context-window failures that vanish under bpfix. Without an ablation that holds length and structure fixed while removing or scrambling the loss-point localization (e.g., terminal-error-only structured prompt, or diagnostic with loss point redacted), the 11–21pp gains cannot be attributed specifically to proof-loss localization rather than to prompt form. The stage-wise reductions and case studies are consistent with the claim but do not isolate it; this is load-bearing for the paper’s strongest interpretive sentence.
  2. §3.2 and the free parameters of the study: Reconstruction of establishment and loss depends on log_level=2 abstract states as emitted by kernel 6.15.11. The manuscript does not report how often establishment or loss is unobservable (no loss point), how often the inferred proof family is wrong relative to the developer fix, or sensitivity to verifier/logging changes. A quantitative coverage or accuracy table over the 235 cases (or at least over the 75-task subset) is needed to support the claim that the printed states contain enough evidence for the dominant root-cause classes.
minor comments (5)
  1. §2.2: Selection from 936 candidates down to 235 is described only at a high level (“do not reject under our toolchain, need a specific environment, or lack the source”). A short breakdown of drop reasons would help assess selection bias.
  2. Table 1 / Table 2: Root-cause labeling is presented as ground truth from developer fixes, but inter-rater process and agreement are not reported; a sentence on labeling procedure would strengthen the taxonomy.
  3. §4 case studies are clear but abridged; stating how often the layer label (source_bug vs lowering_artifact) matches the developer’s actual fix layer over the 44 non-source cases would make the separation claim quantitative.
  4. Figure 6 and Table 3: Absolute counts are given in the text; adding absolute pass/fail numbers on the figure or an appendix table would improve readability.
  5. Related work: PrettyVerifier and bpfvv are correctly distinguished as not reconstructing proof loss; a one-sentence comparison of diagnostic content (not only UI) would help readers unfamiliar with those tools.

Circularity Check

0 steps flagged

No circularity: repair gains and taxonomy rest on external kernel verifier acceptance and developer-authored fixes, not on self-defined or fitted targets.

full rationale

The paper’s load-bearing chain is empirical and tool-evaluation, not a first-principles derivation that could collapse into its inputs. Root-cause labels for the 191 program bugs are grounded in the developer’s own fix from each original report (§2.2–2.3), not in bpfix’s output. bpfix-bench accepts a candidate only if it loads through the real kernel verifier and passes functional and source-semantics checks that are explicitly independent of bpfix (§5.1). The 11–21pp one-shot gains are therefore differences between two prompt conditions judged by an external oracle, not a quantity fitted from the same data and then re-reported as prediction. Self-citations (e.g., Kgent, bpftime) appear only in related work and do not justify the diagnostic-gap measurements or the repair deltas. Confounding of localization content with prompt length/structure is an experimental-design concern, not circularity by construction. No self-definitional loop, fitted-input-as-prediction, uniqueness import, or renamed known result is present.

Axiom & Free-Parameter Ledger

3 free parameters · 4 axioms · 2 invented entities

The central claims rest on standard program-analysis assumptions about the eBPF verifier’s abstract interpreter and on the representativeness of the reproduced rejection corpus and the LLM benchmark. No fitted physical constants; free choices are engineering (kernel/clang versions, log level, model set, temperature). Invented entities are software artifacts with public code, not unfalsifiable theoretical objects.

free parameters (3)
  • kernel and clang toolchain pin (6.15.11 / clang 18)
    All 235 rejections are reproduced under this fixed pair; different versions can change which programs reject and what the log contains.
  • verifier log_level=2
    bpfix’s reconstruction depends on per-instruction abstract states only printed at this verbosity.
  • LLM evaluation settings (models, temperature 0, one-shot/one-retry)
    Reported 11–21pp gains are measured under these fixed choices; other models or decoding policies could shift absolute rates.
axioms (4)
  • domain assumption The eBPF verifier’s printed per-instruction abstract states are a faithful enough projection of its internal proof obligations to recover establishment and loss of the required proof family.
    Stated as the reconstruction basis in §3.2; without it localization cannot be derived from the log alone.
  • domain assumption Developer-authored fixes in the source reports correctly identify the root-cause category for each of the 191 program bugs.
    Used as ground truth for Table 1 and the diagnostic-gap analysis in §2.3–2.4.
  • domain assumption A repair that loads through the kernel verifier and passes the task’s functional and source-semantics tests is a correct fix for scoring purposes.
    Defines success on bpfix-bench (§5.1); independent of bpfix by construction.
  • standard math Standard static-analysis / abstract-interpretation reasoning over register types, scalar ranges, and pointer provenance.
    Background for tracking proof evidence through the log (§3).
invented entities (2)
  • bpfix proof-lifecycle reconstruction (proof family, establishment, loss point, rejection location) independent evidence
    purpose: Map terminal verifier errors to the earlier instruction where the required proof became unavailable and emit a Rust-like diagnostic.
    Core technical artifact of §3; independent_evidence is true via public implementation and external verifier acceptance of repairs.
  • bpfix-empirical (235 reproduced rejections) and bpfix-bench (75 LLM repair tasks) independent evidence
    purpose: Quantify the diagnostic gap and measure whether localization improves automated repair.
    New evaluation artifacts; their value is empirical rather than theoretical.

pith-pipeline@v1.1.0-grok45 · 15380 in / 3027 out tokens · 25982 ms · 2026-07-12T07:18:09.536671+00:00 · methodology

0 comments
read the original abstract

eBPF lets developers run custom programs inside the Linux kernel, where a verifier proves each program safe. However, when the verifier rejects a program, the unclear error makes repair challenging: the error reports where verification stopped, not where the program lost the proof the verifier required. To quantify this gap, we conduct an empirical study of 235 reproduced rejections, showing that 47% of rejections return only EINVAL, one error string maps to as many as nine distinct root causes, and 10 of the 12 root causes are eBPF-specific. Repair thus requires both domain knowledge and locating where the proof was lost, yet existing tools only help developers read the error. We present bpfix, which reconstructs where the required proof was established and where it was lost from the verifier log, and prints a Rust-like diagnostic. To evaluate bpfix and the ability of LLMs to help repair, we construct a benchmark of 75 LLM repair tasks. Current models achieve 0-37% one-shot success with the raw log, and replacing the log with the bpfix localization improves repair by 11-21pp, suggesting that locating where the proof was lost is key to guiding repair. bpfix is available at https://github.com/eunomia-bpf/bpfix

Figures

Figures reproduced from arXiv: 2607.02748 by Andi Quinn, Dan Williams, Jianchang Su, Weichen Tao, Wei Zhang, Xiangyu Gao, Yusheng Zheng, Zhengjie Ji.

Figure 2
Figure 2. Figure 2: A compiler-lowering rejection: correct source that the verifier reports as invalid mem access ‘scalar’. after each instruction, ending in a one-line terminal error at the rejected instruction. The terminal error names the rejection location, the oper￾ation where verification stopped, which the verifier reaches only after the program lost the proof at an earlier instruction. To repair the program so it pass… view at source ↗
Figure 1
Figure 1. Figure 1: bpfix on a real rejection (Stack Overflow 53136145). The verifier returns one register-level line; from the same log, bpfix reconstructs the discarded proof and localizes the rejection to the point where the required proof was lost, mapping each span back to source. developer reads a rejection (§2.1), and then we assemble bpfix-empirical, a dataset of real rejections (§2.2), characterize the rejections in … view at source ↗
Figure 3
Figure 3. Figure 3: Overview of the bpfix workflow. bpfix analyzes verifier logs, reconstructs the missing proof, and generates a repair-oriented diagnostic. prints its abstract state after every instruction, so the lost proof survives in the printed states, and §3 reconstructs the proof from those states to localize the loss. Takeaway #2: The terminal error is too coarse to guide repair: 47% of rejections return EINVAL, and … view at source ↗
Figure 4
Figure 4. Figure 4: A real rejection from the aya project (issue 1002): (a) the rejected program, the verifier’s terminal line, and the bpfix diagnostic; (b) the developer’s fix. verifier rejects the write with the terminal line only read from bpf_array is supported. The line is correct, but it gives only the symptom: the verifier sees a write through the map object where a map value is required. From the same log, bpfix reco… view at source ↗
Figure 5
Figure 5. Figure 5: Two rejections that share the verifier message invalid mem access ‘scalar’ but need fixes in different layers: a source bug (a) and a compiler-lowering artifact (b). Each diagnostic is abridged to its error id, class, and the verifier line it explains. type before the load. The upstream fix steers the compiler and leaves the source logic unchanged, so the layer label holds independently of bpfix. bpfix rep… view at source ↗
Figure 6
Figure 6. Figure 6: bpfix-bench repair success across three models. Bars are grouped by prompt mode and colored by model; retry bars use one failure-informed retry. To locate the gain, we charge each failed one-shot candi￾date to the first stage it fails: returning a program, compiling, loading through the verifier, passing the functional test, or passing the source-semantics test. As [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

28 extracted references · 3 canonical work pages · 1 internal anchor

  1. [1]

    Cilium Authors. 2026. Cilium: eBPF-based Networking, Observability, and Security.https://github.com/cilium/cilium. Open-source project, accessed 2026

    2026

  2. [2]

    Cimatti, A

    A. Cimatti, A. Griggio, and R. Sebastiani. 2011. Computing Small Un- satisfiable Cores in Satisfiability Modulo Theories.Journal of Artificial Intelligence Research40 (April 2011), 701–728. doi:10.1613/jair.3196

    doi:10.1613/jair.3196 2011

  3. [3]

    Mugdha Deokar, Jingyang Men, Lucas Castanheira, Ayush Bhardwaj, and Theophilus A. Benson. 2024. An Empirical Study on the Chal- lenges of eBPF Application Development. InProceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions(Sydney, NSW, Australia)(eBPF ’24). Association for Computing Machinery, New York, NY, USA, 1–8. doi:10.1145/3672...

    work page doi:10.1145/3672197.3673429 2024

  4. [4]

    Bolaji Gbadamosi, Luigi Leonardi, Tobias Pulls, Toke Høiland- Jørgensen, Simone Ferlin-Reiter, Simo Sorce, and Anna Brunström

  5. [5]

    arXiv:2410.00026 [cs.OS] https://arxiv.org/abs/2410.00026

    The eBPF Runtime in the Linux Kernel. arXiv:2410.00026 [cs.OS] https://arxiv.org/abs/2410.00026

    Pith/arXiv arXiv

  6. [6]

    Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv

    Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv

  7. [7]

    InProceedings of the 40th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation(Phoenix, AZ, USA) (PLDI 2019)

    Simple and precise static analysis of untrusted Linux kernel extensions. InProceedings of the 40th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation(Phoenix, AZ, USA) (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 1069–1084. doi:10.1145/3314221.3314590

    doi:10.1145/3314221.3314590 2019

  8. [8]

    Le, Hubertus Franke, Hani Jamjoom, Tianyin Xu, and Dan Williams

    Jinghao Jia, Ruowen Qin, Milo Craun, Egor Lukiyanov, Ayush Bansal, Minh Phan, Michael V. Le, Hubertus Franke, Hani Jamjoom, Tianyin Xu, and Dan Williams. 2025. Rex: Closing the language-verifier gap with safe and usable kernel extensions. In2025 USENIX Annual Tech- nical Conference (USENIX ATC 25). USENIX Association, Boston, MA, 325–342.https://www.useni...

    2025

  9. [9]

    A game of alignment:collective behavior of multi-species

    James A. Jones and Mary Jean Harrold. 2005. Empirical evaluation of the tarantula automatic fault-localization technique. InProceedings of the 20th IEEE/ACM International Conference on Automated Software En- gineering(Long Beach, CA, USA)(ASE ’05). Association for Computing Machinery, New York, NY, USA, 273–282. doi:10.1145/1101908.1101949

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1145/1101908.1101949 2005

  10. [10]

    libbpf. 2025. bpfvv: BPF Verifier Visualizer.https://github.com/libbpf/ bpfvv. Accessed 2026-06-25

    2025

  11. [11]

    Soo Yee Lim, Xueyuan Han, and Thomas Pasquier. 2023. Unleashing Unprivileged eBPF Potential with Dynamic Sandboxing. InProceedings of the 1st Workshop on EBPF and Kernel Extensions(New York, NY, USA) (eBPF ’23). Association for Computing Machinery, New York, NY, USA, 42–48. doi:10.1145/3609021.3609301

    work page doi:10.1145/3609021.3609301 2023

  12. [12]

    Soo Yee Lim, Tanya Prasad, Xueyuan Han, and Thomas Pasquier. 2024. SafeBPF: Hardware-assisted Defense-in-depth for eBPF Kernel Exten- sions. InProceedings of the 2024 on Cloud Computing Security Workshop (Salt Lake City, UT, USA)(CCSW ’24). Association for Computing Ma- chinery, New York, NY, USA, 80–94. doi:10.1145/3689938.3694781

    doi:10.1145/3689938.3694781 2024

  13. [13]

    Linux kernel documentation. 2025. eBPF verifier.https://docs.kernel. org/bpf/verifier.html. The Linux Kernel documentation, Documenta- tion/bpf/verifier.rst

    2025

  14. [14]

    Hongyi Lu, Shuai Wang, Yechang Wu, Wanning He, and Feng- wei Zhang. 2024. MOAT: Towards Safe BPF Kernel Extension. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX As- sociation, Philadelphia, PA, 1153–1170.https://www.usenix.org/ conference/usenixsecurity24/presentation/lu-hongyi

    2024

  15. [15]

    Zvonimir Pavlinovic, Tim King, and Thomas Wies. 2014. Finding minimum type error sources.SIGPLAN Not.49, 10 (Oct. 2014), 525–542. 6 doi:10.1145/2714064.2660230

    doi:10.1145/2714064.2660230 2014

  16. [16]

    Rosario Rizza, Riccardo Sisto, and Fulvio Valenza. 2025. Design and implementation of a tool to improve error reporting for eBPF code. In2025 IEEE International Conference on Cyber Security and Resilience (CSR)(Chania, Crete, Greece). IEEE, Piscataway, NJ, USA, 214–219. doi:10.1109/CSR64739.2025.11130075

    doi:10.1109/csr64739.2025.11130075 2025

  17. [17]

    Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, and Ranjit Jhala

    Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, and Ranjit Jhala. 2017. Learning to blame: localizing novice type errors with data-driven diagnosis.Proc. ACM Program. Lang.1, OOPSLA, Article 60 (Oct. 2017), 27 pages. doi:10.1145/3138818

    doi:10.1145/3138818 2017

  18. [18]

    Hao Sun and Zhendong Su. 2024. Validating the eBPF verifier via state embedding. InProceedings of the 18th USENIX Conference on Operating Systems Design and Implementation(Santa Clara, CA, USA)(OSDI’24). USENIX Association, USA, Article 33, 14 pages

    2024

  19. [19]

    The XDP Project. 2026. xdp-tools: Utilities and Example Programs for Use with XDP.https://github.com/xdp-project/xdp-tools. Open- source project, accessed 2026

    2026

  20. [20]

    Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2022. Sound, precise, and fast abstract inter- pretation with tristate numbers. InProceedings of the 20th IEEE/ACM International Symposium on Code Generation and Optimization(Virtual Event, Republic of Korea)(CGO ’22). IEEE Press, Piscataway, NJ, USA, 254–265. doi:10.110...

    doi:10.1109/cgo53902.2022.9741267 2022

  21. [21]

    Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2023. Verifying the Verifier: eBPF Range Anal- ysis Verification. InComputer Aided Verification: 35th International Conference, CA V 2023, Paris, France, July 17–22, 2023, Proceedings, Part III(Paris, France). Springer-Verlag, Berlin, Heidelberg, 226–251. doi:10.1007/978...

    doi:10.1007/978-3-031-37709-9_12 2023

  22. [22]

    Mark Weiser. 1981. Program slicing. InProceedings of the 5th Interna- tional Conference on Software Engineering(San Diego, California, USA) (ICSE ’81). IEEE Press, Piscataway, NJ, USA, 439–449

    1981

  23. [23]

    Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, and Franz Wotawa

    W. Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, and Franz Wotawa

  24. [24]

    2016), 707–740

    A Survey on Software Fault Localization .IEEE Transactions on Software Engineering42, 08 (Aug. 2016), 707–740. doi:10.1109/TSE. 2016.2521368

    doi:10.1109/tse 2016

  25. [25]

    Danfeng Zhang and Andrew C. Myers. 2014. Toward general diagnosis of static errors.SIGPLAN Not.49, 1 (Jan. 2014), 569–581. doi:10.1145/ 2578855.2535870

    arXiv 2014

  26. [26]

    Peihua Zhang, Chenggang Wu, Xiangyu Meng, Yinqian Zhang, Ming- fan Peng, Shiyang Zhang, Bing Hu, Mengyao Xie, Yuanming Lai, Yan Kang, and Zhe Wang. 2024. HIVE: A Hardware-assisted Isolated Exe- cution Environment for eBPF on AArch64. In33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 163–180.https://www.usenix.org...

    2024

  27. [27]

    Yusheng Zheng, Yiwei Yang, Maolin Chen, and Andrew Quinn. 2024. Kgent: Kernel Extensions Large Language Model Agent. InProceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions (Sydney, NSW, Australia)(eBPF ’24). Association for Computing Ma- chinery, New York, NY, USA, 30–36. doi:10.1145/3672197.3673434

    doi:10.1145/3672197.3673434 2024

  28. [28]

    Yusheng Zheng, Tong Yu, Yiwei Yang, Yanpeng Hu, Xiaozheng Lai, Dan Williams, and Andi Quinn. 2025. Extending applications safely and efficiently. InProceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation(Boston, MA, USA)(OSDI ’25). USENIX Association, Boston, MA, USA, 557–574.https://www.usenix. org/conference/osdi25/presen...

    2025