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

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.