Seminars

View all Seminars  |  Download ICal for this event

Proof Carrying BPF Programs

Series: Department Seminar

Speaker: Prof. Santosh Nagarakatte, Professor and Undergraduate Program Director, Computer Science, Rutgers University

Date/Time: Aug 10 11:00:00

Location: CSA Auditorium, (Room No. 104, Ground Floor)

Abstract:
This talk will describe our Proof-Carrying BPF framework. We envision
proof-carrying-BPF programs as a mechanism to increase the class of
programs accepted by the Linux eBPF verifier without increasing its
complexity. To accomplish this vision, we develop a userspace version
of the kernel verifier and append it to the BPF backend. The BPF
backend generates proofs with symbolic evaluation where the kernel
verifier is not able to prove safety. The kernel verifier checks
proofs with an in-kernel proof checker and accepts the program when the
proof is valid. This coupling of the userspace BPF verifier to the BPF
backend addresses the limitations of the recent BCF framework, such as
latency due to multiple kernel-to-userspace transitions and the
dormant verifier state during userspace verification. Our prototype
can successfully verify 189 programs from Calico/Cilium suites that
the kernel verifier previously rejected.

Speaker Bio:
Santosh Nagarakatte is a Professor and Undergraduate Program Director of Computer Science at Rutgers University. He obtained his PhD from the University of Pennsylvania in 2012. His research interests are in Hardware-Software Interfaces spanning Programming Languages, Compilers, Software Engineering, and Computer Architecture. His papers have been selected as IEEE MICRO Top Picks papers in 2010 and 2013. He received the NSF CAREER Award in 2015, PLDI and ICSE 2016 Distinguished Paper Awards for his research on LLVM compiler verification. His PhD student David Menendezs dissertation on LLVM verification was awarded the 2018 ACM SIGPLAN John C Reynolds Outstanding Dissertation Award. His papers on correctly rounded elementary functions have been recognized with the PLDI 2021 and POPL 2022 Distinguished Paper Awards. His PhD student Jay Lims dissertation on correctly rounded elementary functions was awarded the 2022 ACM SIGPLAN John C Reynolds Outstanding Dissertation Award. He was selected as an ACM Distinguished Member in 2023.

Host Faculty: Prof. Vinod Ganapathy