Dr. Grigory Fedyukovich has a paper accepted at OOPSLA

Dr. Grigory Fedyukovich has a paper accepted at OOPSLA

Dr. Grigory Fedyukovich has a paper accepted at the 2025 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Applications (OOPSLA). The paper, titled “A Flow-Sensitive Refinement Type System for Verifying eBPF Programs”, is co-authored by PhD students Ameer Hamza and Lucas Zavalia. The paper presents a new approach to automatic checking that eBPF programs do not harm the operating system while providing users with a user-friendly way of debugging eBPF programs.

eBPF is a kernel subsystem that allows an operating system to be modified while it is running. The paper focuses on how to check formal properties of eBPF code using a new type system. Every load/store operation is checked within certain fixed memory regions to ensure that kernel secrets are never exposed to user space. The presented approach separates the process of generating types for programs from the process that checks that types are correct. Type inference is handled in user space, while type checking is handled in kernel space, which minimizes the amount of code that has to be trusted. The paper also presents a tool, VeRefine, which infers types for eBPF programs. VeRefine outperforms state-of-the-art in eBPF verification on many benchmark instances.