A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
summary
Type-based verifier infers proof certificates in userspace and pushes only a small checker into the kernel, reducing the trusted codebase. Implementation VeRefine lives as an abstract domain inside Prevail, uses flow-sensitive refinements (slack variables plus meta begin/end for packet bounds) and models pointer provenance (stack, context, packet, shared). Evaluation on 420 benchmarks shows VeRefine is faster and debuggable but slightly less precise than Prevail, and artifacts and reproduced results are available.
AI-written summary · about
chapters (10)
- 0:00Verifying eBPF programs
- 1:25eBPF verification today
- 4:13Limitations of verifiers
- 5:15Type-based verification architecture
- 6:41Pointer provenance and flow safety
- 8:07Flow sensitivity and refinements
- 9:10Packet pointers with refinements
- 10:53Type inference algorithm
- 11:55Evaluation and future work
- 12:17Q&A
related talks
17mVEP: A Two-stage Verification Toolchain for Full eBPF Programmability
15mValidating the eBPF Verifier via State Embedding
43meBPF Superpowers for SRE
01h 03mBPF and Spectre: Mitigating transient execution attacks
19mComparing the Precision of Abstract Operators in the eBPF Verifier using Differential(…)
15mEnhancing the RISC-V Trace Encoder to Verify the Control-Flow and More
29meBPF on the Rise - Getting Started
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole