Verifying the Verifier eBPF Range Analysis Verification
summary
Tool automatically extracts the verifier’s C semantics into SMT and checks a formal soundness spec for the eBPF range and bitwise analyses using Z3 and LLVM, reporting concrete violations and Agni extracts C semantics to SMT. It verifies 16 kernel versions, proves 5.13–5.19 sound, finds nine older kernels unsound with 27 new and 93 known violations, and synthesizes eBPF proofs-of-concept in ~97% of reported cases. Limits: excludes multiplication, verification can take a day and peaks around 16 GB RAM.
AI-written summary · about
chapters (14)
- 0:00Introduction to work
- 1:04Why verify the verifier
- 2:05Automating verification with AG
- 3:29Value tracking analysis
- 6:40Range tracking domain
- 8:49Modular vs non-modular soundness
- 10:14Combined abstract operators
- 11:38Automation in AG
- 12:20AG's strict constraints
- 13:01Generating proof of concept programs
- 14:26Demo of bug synthesis
- 16:12Summary of results
- 17:36Future plans for AG
- 18:18Q&A session
related talks
17mVEP: A Two-stage Verification Toolchain for Full eBPF Programmability
15mValidating the eBPF Verifier via State Embedding
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole
42mKernel Analysis Using eBPF
30mTools for eBPF DevSecOps
01h 18mTutorial: Getting Started with eBPF
51meBPF Warfare - Detecting Kernel & eBPF Rootkits with Tracee
42mA Deep Dive Into eBPF Program Loader