SoK: Challenges and Paths Toward Memory Safety for eBPF
Kaiming Huang, Mathias Payer, Zhiyun Qian, Jack Sampson, Gang Tan, Trent Jaeger
Abstract
The extended Berkeley Packet Filter (eBPF) subsystem in Linux enables the extension of kernel functionality without modifying kernel code. In addition to its use in networking, eBPF provides the flexibility to perform tracing, add security checks, etc. To ensure that eBPF does not enable attackers to compromise the kernel, eBPF includes a verifier to validate every eBPF program before its execution, which includes checks that aim to prevent eBPF programs from modifying kernel memory due to memory errors. However, numerous vulnerabilities have been identified in the eBPF subsystem, including the verifier itself, which greatly violate expectations, leading to concerns about the threats of memory safety brought by eBPF. This paper presents the first systematic analysis of the memory safety risks inherent in the eBPF ecosystem, focusing on the challenges faced by the limitations of the eBPF verifier and current kernel defenses. We then evaluate proposed research mitigation strategies that apply isolation techniques, runtime checks, and static validation, highlighting their contributions and gaps. Our study finds that only 1.62-3.74% (37–85) of the memory operations in public eBPF programs cannot be proven memory safe comprehensively, motivating actionable insights towards enforcing comprehensive memory safety while accounting for performance and compatibility.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers2
- Approximation Enforced Execution of Untrusted Linux Kernel ExtensionsHao Sun, Zhendong SuUSENIX Security 2025
- KRAKENGUARD: Towards Fine-Grained eBPF IsolationJainil Patel, Lucas Graeff Buhl-Nielsen, Adrien Ghosn, Marios KogiasNSDI 2026
Builds on34
- Where Does It Go?: Refining Indirect-Call Targets with Multi-Layer Type AnalysisKangjie Lu, Hong HuCCS 2019 · 142 citations
- RedLeaf: Isolation and Communication in a Safe Operating SystemVikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel et al.OSDI 2020 · 86 citations
- PtrSplit: Supporting General Pointers in Automatic Program PartitioningShen Liu, Gang Tan, Trent JaegerCCS 2017 · 83 citations
- BMC: Accelerating Memcached using Safe In-kernel Caching and Pre-stack ProcessingYoann Ghigoff, Julien Sopena, Kahina Lazri, Antoine Blin et al.NSDI 2021 · 79 citations
- Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernelLuke Nelson, Jacob Van Geffen, Emina Torlak, Xi WangOSDI 2020 · 72 citations
Related papers
- Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction RefinementHao Sun, Zhendong SuSOSP 2025
- MOAT: Towards Safe BPF Kernel ExtensionHongyi Lu, Shuai Wang, Yechang Wu, Wanning He et al.USENIX Security 2024 · 18 citations
- Verifying the Verifier: eBPF Range Analysis VerificationHarishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, Santosh NagarakatteCAV 2023 · 37 citations
- A Flow-Sensitive Refinement Type System for Verifying eBPF ProgramsAmeer Hamza, Lucas Zavalía, Arie Gurfinkel, Jorge A. Navas et al.OOPSLA 2025 · 1 citation
- VEP: A Two-stage Verification Toolchain for Full eBPF ProgrammabilityXiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu et al.NSDI 2025 · 8 citations
