Rex: Closing the language-verifier gap with safe and usable kernel extensions

Safe kernel extensions like eBPF extensions have gained significant traction and practical adoption, evolving from simple packet filters to large, complex programs that customize storage, networking, and CPU and memory management. Existing kernel extension mechanisms like eBPF rely on in-kernel verifiers to ensure safety of kernel extensions by static verification using symbolic execution. However, this current approach introduces significant usability issues due to the language-verifier gap—a mismatch between the developer's expectation of program safety—provided by a contract with the programming language—and the verifier's expectation.

We present Rex, a new kernel extension framework that closes the language-verifier gap to effectively improve usability of kernel extensions. Rex builds on top of language-based safety to provide all the safety properties desired by kernel extensions. Rex employs a lightweight runtime for safety properties that are hard or costly to guarantee by static analysis, including safe exception handling, stack safety, and program termination. With Rex, kernel extensions are written in safe Rust and interact with the kernel via a safe interface provided by Rex's kernel crate. No separate verification is needed. We show that Rex addresses usability issues of eBPF kernel extensions without compromising performance.