VEP - A Two-stage Verification Toolchain for Full eBPF Programmability

Learn about VEP, an innovative annotation-guided verification toolchain designed to overcome the strict constraints of existing eBPF verifiers in this 17-minute conference presentation from NSDI '25. Discover how researchers from Shanghai Jiao Tong University developed a comprehensive solution consisting of three key components: VEP-C for verifying annotated eBPF-C programs, VEP-compiler for targeting annotated eBPF bytecode, and VEP-eBPF as a lightweight bytecode-level proof checker. Explore how this toolchain enables full eBPF programmability by allowing developers to verify program correctness through appropriate annotations, eliminating the need for repeated program modifications to pass verification. Understand the technical approach that addresses limitations found in existing verifiers like the Linux verifier and PREVAIL, while examining experimental results that demonstrate VEP's effectiveness in providing a more flexible and automated approach to kernel security. Gain insights into how this technology advances the Extended Berkeley Packet Filter (eBPF) ecosystem, which has become revolutionary for safely and efficiently extending kernel capabilities across networking, tracing, security, and other domains.