The eBPF Foundation is committed to fostering innovation and expanding the boundaries of eBPF technology. In 2024, we granted $250,000 to five academic research projects aimed at improving eBPF’s performance, security, and usability. As we step into 2025, we are excited to share significant progress from each of these projects, along with their next steps.
1. Learned Virtual Memory with eBPF
Carried out by Dimitrios Skarlatos at Carnegie Mellon University, this project explores using eBPF to enhance virtual memory management by integrating learned page table structures for efficient address translation.
Key Progress:
- A preliminary learned virtual memory (LVM) design has been implemented, achieving performance within 1% of an ideal single-access page table design.
- A draft paper detailing the design and implementation has been prepared.
- Significant progress has been made on an eBPF interface for virtual memory, focusing on abstracting the Linux page table implementation.
- Plans are underway to explore potential eBPF hooks for deeper kernel integration.
Next Steps:
- Finalize eBPF hook exploration for virtual memory management.
- Begin a new related project on page table management with potential for an eBPF-based implementation.
- Work with the Linux community for potential upstream integration.
2. Efficient IO-Intensive µs-scale Applications using eBPF
This project, taking place at the Swiss Federal Institute of Technology Lausanne (EPFL) by Yueyang Pan, Kumar Kartikeya Dwivedi, Rishabh Iyer, and Sanidhya Kashyap, aims to optimize microsecond-scale applications by leveraging eBPF to construct efficient in-kernel data paths and computational runtimes.
Key Progress:
- Scoped two primary use cases: Dynamic Scaling of the Network Stack and Dataplane OS.
- Shifted to a more principled approach by designing composable building blocks for eBPF-based OS structuring, making solutions reusable across domains.
- Initial implementation of a coroutine runtime for dynamic scaling has begun.
Next Steps:
- Prototype the coroutine runtime using LLVM coroutine support.
- Deliver a working dynamic scaling solution as the first major milestone.
- Expand scope beyond networking to other system components.
3. Improving eBPF Complexity with a Hardware-backed Isolation Environment
A team at the Chinese Academy of Sciences Beijing under Zhe Wang is working to replace eBPF’s full-path verification with a hardware-backed isolation environment called HIVE, significantly reducing complexity and improving security.
Key Progress:
- Designed and implemented an initial version of HIVE, which enforces runtime isolation for BPF programs, eliminating the need for full-path analysis.
- Prototyped the approach on an Apple M1 chip and tested on workloads such as Memcached and Redis, showing efficiency comparable to standard eBPF.
- Replaced 10 in-tree kernel modules with HIVE-equipped eBPF programs, validating real-world feasibility.
Next Steps:
- Conduct further performance optimizations and security evaluations.
- Extend implementation to x86 using memory isolation techniques like PKS.
- Pitch to the Linux community for broader adoption.
4. Formally Verified eBPF Verifier for the Linux Kernel
The Rutgers University research team under Srinivas Narayana and Santosh Nagarakatte is formally verifying the path pruning algorithms in the eBPF verifier to ensure soundness and precision in static analysis.
Key Progress:
- Developed new techniques to synthesize more precise abstract operators for range analysis, improving program acceptance rates.
- Began formal verification of path pruning optimizations, ensuring that skipped paths do not introduce security vulnerabilities.
- Implemented directed black-box testing to validate verifier correctness against a comprehensive set of eBPF programs.
Next Steps:
- Extend verification to dataflow state abstractions (e.g., register liveness and pointer tracking).
- Implement soundness proofs for subsumption routines in the verifier.
- Continue upstream contributions to the Linux kernel.
5. Lazy Abstraction Refinement with Proof for an Enhanced Verifier
Zhendong Su and Hao Sun at ETH Zurich are developing a proof-based abstraction refinement mechanism to enhance eBPF verification by selectively refining abstractions with higher-precision techniques.
Key Progress:
- Implemented a proof-of-concept prototype where the verifier pauses execution to request a refinement proof from user space when encountering imprecise approximations.
- Developed an in-kernel proof checker and a new binary certificate format (BCF) to efficiently validate refinements.
- Collected a dataset of 339 eBPF programs from 15 projects to evaluate acceptance rates and overhead improvements.
Next Steps:
- Expand dataset coverage and analyze proof validation efficiency.
- Finalize refinements and submit findings to SOSP 2025.
- Release source code, datasets, and evaluation results to the community.
Looking Ahead
The eBPF Foundation is thrilled with the advancements made by these projects and looks forward to their continued development. As these research initiatives progress, we anticipate a significant impact on eBPF’s adoption and evolution, from improving memory management to enhancing verifier precision and security. We will continue to support and collaborate with the research community to push the boundaries of what’s possible with eBPF.