VEP: A Two-stage Verification Toolchain for Full eBPF Programmability
summary
VEP is a two-stage verifier: VEP-C (annotation-guided C verifier), a VEP-compiler that preserves annotations through compilation, and VEP-eBPF, a lightweight bytecode proof checker in the kernel. Claim: annotated programs achieve both zero false positives and zero false negatives in their evaluation. Example: a 618‑line Linux sample needs 16 high‑level annotations that expand to 64,840 proof obligations; VEP-C uses most CPU time, VEP-eBPF uses minimal kernel resources. Compared to Linux verifier and PREVAIL, VEP accepts string-library cases that those reject.
AI-written summary · about
chapters (11)
- 0:00VEP verification toolchain intro
- 2:48Current eBPF verifier challenges
- 4:11VEP design goals
- 4:55VEP three-stage workflow
- 7:04XTP packet handling example
- 10:54Annotated C to eBPF bytecode
- 12:21User feedback and verifier choices
- 13:26Zero false positives and negatives
- 14:10Evaluation results and accuracy
- 15:40Annotation requirements
- 16:24Summary and future
related talks
26mVerifying the Verifier eBPF Range Analysis Verification
15mValidating the eBPF Verifier via State Embedding
14mA Flow-Sensitive Refinement Type System for Verifying eBPF Programs
29meBPF on the Rise - Getting Started
01h 18mTutorial: Getting Started with eBPF
38mAlice in Kernel Land: Lessons Learned From the eBPF Rabbit Hole
43meBPF Superpowers for SRE
01h 03mBPF and Spectre: Mitigating transient execution attacks