Thesis Proposal: Generating Safety Proofs for eBPF in LLVM

 - 2 mins read

Details

Type: BA/MA/GR/IDP
Timeframe: WS24/25, SS25
Keywords: eBPF, PCC, Z3, static analysis
A PDF version of this proposal can be found here.

Introduction

eBPF1 programs run inside the kernel without user–kernel boundaries, which means any mistake can corrupt kernel memory or break isolation. Current verifiers run entirely on generated eBPF code and are limited1 2: They reject many safe programs and still fail to catch certain bugs. To address this, we propose a two stage verification approach, based on Proof-Carrying Code (PCC)3. The eBPF compiler generates safety proofs during compilation and the kernel only checks these proofs after JIT compilation, which provides end to end safety while reducing false rejections.

Objective of the Thesis

In this thesis you will implement the LLVM side of the system. You will integrate Z34 into LLVM, derive safety properties during IR lowering, and emit compact proof artifacts that the kernel level verifier can check.

Required Skills

  • C++ knowledge
  • Experience with LLVM
  • Basic understanding of compilers and static analysis

  1. “eBPF Verifier. The Linux Kernel Documentation.” https://docs.kernel.org/bpf/verifier.html. Accessed November 12, 2025. ↩︎ ↩︎

  2. Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv. 2019. “Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions.” In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1069 to 1084. PLDI 2019. New York NY USA. Association for Computing Machinery. https://doi.org/10.1145/3314221.3314590. ↩︎

  3. George C. Necula. 1997. “Proof Carrying Code.” In Proceedings of the ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, pages 106 to 119. POPL 1997. New York NY USA. Association for Computing Machinery. https://doi.org/10.1145/263699.263712. ↩︎

  4. Leonardo de Moura and Nikolaj Bjørner. 2008. “Z3: An Efficient SMT Solver.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by C. R. Ramakrishnan and Jakob Rehof, pages 337 to 340. Berlin Heidelberg. Springer. https://doi.org/10.1007/978-3-540-78800-3_24. ↩︎