The Good, Bad, and Ugly of Verified Safe Kernel Extensions
Dan Williams - Virginia Tech
Monday, March 13, 2023, 2:15-3:15 pm 
Abstract
eBPF has been described as a superpower for the kernel, in part
because of its promise to run verified safe extensions anywhere in the
kernel. However, verification comes at a cost of both expressiveness
and performance. In this talk, I will give an overview of my recent
research on eBPF at Virginia Tech. First, I will describe KFUSE (in
Eurosys '21), a system that decouples the execution of BPF extensions
from their verification requirements, allowing chains of BPF extension
programs to be collectively optimized after each BPF extension program
is individually verified and loaded into the shared kernel. Then, I
because of its promise to run verified safe extensions anywhere in the
kernel. However, verification comes at a cost of both expressiveness
and performance. In this talk, I will give an overview of my recent
research on eBPF at Virginia Tech. First, I will describe KFUSE (in
Eurosys '21), a system that decouples the execution of BPF extensions
from their verification requirements, allowing chains of BPF extension
programs to be collectively optimized after each BPF extension program
is individually verified and loaded into the shared kernel. Then, I
will describe ongoing work exploring the verifier's constraints on
expressiveness and the unfortunate effects of those constraints on
safety.
expressiveness and the unfortunate effects of those constraints on
safety.
Bio
Dan Williams has been an Assistant Professor at Virginia Tech since
Fall '21, after a decade as a Research Staff Member at IBM
Research. His research interests center around operating systems and
virtualization usually in a cloud security context. He is best known
for his work on unikernels as the original author of Solo5 and a
co-creator of IBM Nabla Containers. He is active in the research
community, having co-authored over 30 peer-reviewed papers for top
USENIX and ACM conferences, and has served on numerous program
committees, most recently co-chairing USENIX ATC '23.
Fall '21, after a decade as a Research Staff Member at IBM
Research. His research interests center around operating systems and
virtualization usually in a cloud security context. He is best known
for his work on unikernels as the original author of Solo5 and a
co-creator of IBM Nabla Containers. He is active in the research
community, having co-authored over 30 peer-reviewed papers for top
USENIX and ACM conferences, and has served on numerous program
committees, most recently co-chairing USENIX ATC '23.
This talk is organized by Todd Holden