A Flow-Sensitive Refinement Type System for Verifying eBPF Programs

The Extended Berkeley Packet Filter (eBPF) subsystem within an operating system’s kernel enables userspace programs to extend kernel functionality dynamically. Due to the security risks associated with runtime modification of the operating system, eBPF requires all programs to be verified before deploying them within the kernel. Existing approaches to eBPF verification are monolithic, requiring their entire analysis to be done in a secure environment, resulting in the need for extensive trusted codebases. We present a type- based verification approach that automatically infers proof certificates in userspace, thus reducing the size and complexity of the trusted codebase. At the same time, only the proof-checking component needs to be deployed in a secure environment. Moreover, compared to previous techniques, our type system enhances the debuggability of the programs for users through ergonomic type annotations when verification fails. We implemented our type inference algorithm in a tool called VeRefine and evaluated it against an existing eBPF verifier, Prevail. VeRefine outperformed Prevail on most of the industrial benchmarks.