Assessing the Verifiability of Compiler Optimizations
In recent years, eBPF [1] has become a popular way to extend the Linux kernel with custom functionality [2]. Compared to kernel modules, eBPF programs are easier to write: The kernel provides a stable API that these programs can rely on, and verifies them to guarantee memory safety. But that does not mean that eBPF programs are particularly easy to write: eBPF verification is inaccurate and can reject safe programs.
A reason for this is an inherent mismatch between implementation and verification: While the developer implements eBPF programs in C (or other, higher-level languages), the kernel verifies the compiled binary. In between sits the compiler, which performs provably safe, but not always verifiable optimizations. Thus, even C can be too high-level, and developers regularly have to resort to assembly to avoid unverifiable optimization passes.
While this is a known problem [3], it remains unclear how to resolve it. Some suggest that the compiler should produce easier-to-verify binaries, while others advocate for more accurate eBPF verification. While both positions have merit, the debate lacks sufficient data to find a resolution.
The goal of this thesis is to address this knowledge gap. More specifically, this thesis aims at answering the following questions: Which optimization passes negatively impact eBPF verification? How big of a problem is this for day-to-day eBPF development? And how has this problem evolved over time?
Milestones
- Getting familiar with eBPF, its verification process, and the compiler optimizations
- Setup an infrastructure that links verification problems back to optimization passes
- Collect a test suite of eBPF programs and assess the status quo
Requirements
- Good understanding of C
- Experience with low-level programming and compiler design
- Critical and independent thinking
References
Supervisors
