The Good, Bad, and Ugly of Verified Safe Kernel Extensions

Dan Williams
Virginia Tech
03.13.2023 14:15 to 15:15

IRB 3137

eBPF has been described as a superpower for the kernel, in partbecause of its promise to run verified safe extensions anywhere in thekernel. However, verification comes at a cost of both expressivenessand performance. In this talk, I will give an overview of my recentresearch on eBPF at Virginia Tech. First, I will describe KFUSE (inEurosys '21), a system that decouples the execution of BPF extensionsfrom their verification requirements, allowing chains of BPF extensionprograms to be collectively optimized after each BPF extension programis individually verified and loaded into the shared kernel. Then, I
will describe ongoing work exploring the verifier's constraints onexpressiveness and the unfortunate effects of those constraints onsafety.