Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential(…)
summary
Presents a reproducible pipeline that lifts the 30,000-line eBPF verifier C code (about 6,000 lines of abstract-operator logic) into SMT via LLVM, checks precision relations between two sound abstract operators over reachable states, and uses SMT-based synthesis with depth-limited enumerative search to produce concrete witness programs that drive the verifier into differing abstract states. Produces a more precise multiplication operator and the bpf_mul upstreamed patch; the witnesses convince kernel developers and the checks run in kernel CI.
AI-written summary · about
chapters (8)
- 0:00eBPF and its verifier
- 3:10AGNI verification overview
- 6:21Soundness vs precision in operators
- 10:14Measuring operator precision
- 13:29Differential synthesis
- 16:21Case study: multiplication patch
- 17:03Conclusion and future work
- 17:47Q&A
related talks
43meBPF Superpowers for SRE
15mValidating the eBPF Verifier via State Embedding
33meBPF: exploring use case of BPF kernel infrastructure
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole
15mTowards a standardized eBPF ISA - Conformance testing
14mA Flow-Sensitive Refinement Type System for Verifying eBPF Programs
13mA complete formal semantics of eBPF instruction set architecture for Solana
01h 03mBPF and Spectre: Mitigating transient execution attacks