Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel
This talk presents our ongoing efforts of applying formal methods to a critical component in the Linux kernel, the just-in-time compilers (“JITs”) for the extended Berkeley Packet Filter (BPF). Building on our automated verification framework Serval, we have developed Jitterbug, a tool for writing JITs and proving them correct. We have used Jitterbug to find 30+ new bugs in the BPF JITs for the x86-32, x86-64, arm32, arm64, and riscv64 architectures, and to develop a new BPF JIT for riscv32, RISC-V compressed instruction support for riscv64, and new optimizations in existing JITs. All of these changes have been upstreamed to the Linux kernel.
Xi Wang is an associate professor in the Paul G. Allen School of Computer Science & Engineering at the University of Washington. He received his PhD from MIT, and B.E. and M.E. from Tsinghua. His research interests are in building secure and reliable systems. He contributed to the STACK tool for finding undefined behavior bugs in C programs, the Yggdrasil toolkit for writing file systems with push-button verification, and the Serval framework for automated verification of systems software.