The eBPF verifier has repeatedly suffered from bugs in its verification algorithm which enable malicious applications to perform container escapes and privilege escalation. To improve upon this, existing work applies fuzzing (Chaignon'24) and formal methods (Agni) to the verifier in order to find and fix bugs. However, in the mid-term, these approaches are unlikely to result in a verifier that is fully bug-free. While academic works have proposed the use of hardware-based isolation (MOAT, Hive, SafeBPF) and software-fault isolation (BeeBox) to mitigate verifier bugs, these approaches suffer from portability issues, require significant design-changes with unclear consequences, or have runtime overheads.

Motivated by the shortcomings of the existing approaches, this talk discusses an alternative approach to prevent verifier-bugs from being exploited. By requiring eBPF bytecode to be compiled from safe Rust source code by a trusted systems service, program-safety would effectively be checked twice by two very different static analyzers (i.e., rustc's compiler passes and the eBPF verifier). Therefore, a bug in one of the analyzers will no longer directly result in a kernel exploit as the other analyzer is unlikely to exhibit the same buggy behavior and therefore still catch malicious programs. This approach is appealing as it is unlikely to result in runtime overheads and does not require significant changes to the kernel.

We analyze whether this is a viable approach to mitigate bugs in the eBPF verifier, taking runtime-overheads, expressiveness, and security into consideration. Specifically, we analyze whether past bugs in rustc and the eBPF verifier could have been chained together in order to exploit the proposed design as a whole.

We find that the fundamental flexibility of the Rust-IR-to-eBPF mapping allows attackers to still exploit the system as a whole. We also investigate whether using the alternative PREVAIL eBPF verifier would prevent a similar attack, but find that there exists a simple construction that allows attackers to combine exploits for the individual verifiers into an exploit that works for the verifiers when chained together.