Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Safe and usable kernel extensions with Rex

Jinghao Jia, Ruowen Qin, Milo Craun, Egor Lukiyanov, Ayush Bansal, Michael V. Le, Hubertus Franke, Hani Jamjoom, Tianyin Xu, Dan Williams

TL;DR

Rex tackles the usability and maintainability problems of eBPF kernel extensions by removing the in-kernel verifier and enforcing safety through a safe Rust-based framework. It provides a safe kernel interface via a Rex kernel crate, and complements static safety with a lightweight in-kernel runtime for properties like termination and stack safety. The approach yields cleaner, more scalable extension code with comparable performance to eBPF, demonstrated by the Rex-BMC case study and macro/micro benchmarks. Rex introduces a practical path for large, complex kernel extensions while acknowledging trade-offs such as Rust toolchain trust and current lack of dynamic allocation support.

Abstract

Safe kernel extensions have gained significant traction, evolving from simple packet filters to large, complex programs that customize storage, networking, and scheduling. Existing kernel extension mechanisms like eBPF rely on in-kernel verifiers to ensure safety of kernel extensions by static verification using symbolic execution. We identify significant usability issues -- safe extensions being rejected by the verifier -- due to the language-verifier gap, a mismatch between developers' 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 and improves the usability of kernel extensions in terms of programming experience and maintainability. Rex builds upon language-based safety to provide safety properties desired by kernel extensions, along with a lightweight extralingual runtime for properties that are unsuitable for static analysis, including safe exception handling, stack safety, and 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 static verification is needed. Rex addresses usability issues of eBPF kernel extensions without compromising performance.

Safe and usable kernel extensions with Rex

TL;DR

Rex tackles the usability and maintainability problems of eBPF kernel extensions by removing the in-kernel verifier and enforcing safety through a safe Rust-based framework. It provides a safe kernel interface via a Rex kernel crate, and complements static safety with a lightweight in-kernel runtime for properties like termination and stack safety. The approach yields cleaner, more scalable extension code with comparable performance to eBPF, demonstrated by the Rex-BMC case study and macro/micro benchmarks. Rex introduces a practical path for large, complex kernel extensions while acknowledging trade-offs such as Rust toolchain trust and current lack of dynamic allocation support.

Abstract

Safe kernel extensions have gained significant traction, evolving from simple packet filters to large, complex programs that customize storage, networking, and scheduling. Existing kernel extension mechanisms like eBPF rely on in-kernel verifiers to ensure safety of kernel extensions by static verification using symbolic execution. We identify significant usability issues -- safe extensions being rejected by the verifier -- due to the language-verifier gap, a mismatch between developers' 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 and improves the usability of kernel extensions in terms of programming experience and maintainability. Rex builds upon language-based safety to provide safety properties desired by kernel extensions, along with a lightweight extralingual runtime for properties that are unsuitable for static analysis, including safe exception handling, stack safety, and 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 static verification is needed. Rex addresses usability issues of eBPF kernel extensions without compromising performance.

Paper Structure

This paper contains 22 sections, 9 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Safety of Kernel Extensions
  3. The Language-Verifier Gap
  4. Verifier Workarounds
  5. Implications
  6. Key Idea and Safety Model
  7. Rex Design
  8. Safe Rust in Rex
  9. Memory safety
  10. Extended type safety
  11. Safe resource management
  12. Safe exception handling
  13. Kernel stack safety
  14. Termination
  15. Implementation
  16. ...and 7 more sections

Figures (9)

  • Figure 1: The language-verifier gap
  • Figure 2: An example of the language-verifier gap from Cilium chaignon-847014aa62f9, where a safe eBPF extension is incorrectly rejected by the verifier (\ref{['fig:inline-error']}) and developers had to work around the problem by creating inline assembly code (\ref{['fig:inline-asm']}).
  • Figure 3: Examples that developers had to work around the language-verifier gap by refactoring already safe extensions
  • Figure 4: Overview of the Rex kernel extension framework. The gray boxes are Rex components.
  • Figure 5: Exception handling control flow in Rex
  • ...and 4 more figures