Exploring Static and Dynamic Safety for Safe, Expressive, and Fast Kernel Extensions

Abstract

Kernel extensions allow for flexibility in operating systems. The expressiveness of extensions that can be written is limited by requirements of safety and performance. In eBPF, a Linux kernel extension framework, an in-kernel verifier statically upholds extension safety, while a dynamically checked kernel interface enables expressiveness otherwise prohibited by the verifier. In this work, we explore the benefits and limitations of this hybrid safety model. We find that the eBPF interface has gaps in its safety and a lack of expressiveness. To address these limitations, we introduce termination to eBPF to guarantee a bound on program runtime safety, and we identify a fundamental language-verifier gap which compromises eBPF expressiveness. We evaluate the proposed termination mechanism and Rex's approach to closing the language-verifier gap, finding that both reflect different tradeoffs in safety, performance, and expressiveness while improving over the original eBPF framework.