BeePL: Correct-by-Compilation Kernel Extensions

This conference talk presents BeePL, a new eBPF programming language designed to create correct-by-compilation kernel extensions. Explore how BeePL's type system encodes eBPF specifications and utilizes a formally verified compiler to preserve security properties through to BPF bytecode. Learn about the challenges with current eBPF verifiers and how this approach addresses safety concerns when extending kernel capabilities without modifying kernel source code or implementing kernel modules. Presented by researchers Swarn Priya, Tim Steenvoorden, Connor Sughrue, Frédéric Besson, and Freek Verbeek from Virginia Tech, Open Universiteit, and Inria, Rennes at the PriSC 2025 workshop sponsored by ACM SIGPLAN.