SoK: Challenges and Paths Toward Memory Safety for eBPF
Kaiming Huang, Mathias Payer, Zhiyun Qian, Jack Sampson, Gang Tan, Trent Jaeger
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper2
- 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
它引用的顶会 Paper34
- Where Does It Go?: Refining Indirect-Call Targets with Multi-Layer Type AnalysisKangjie Lu, Hong HuCCS 2019 · 被引用 142 次
- RedLeaf: Isolation and Communication in a Safe Operating SystemVikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel 等OSDI 2020 · 被引用 86 次
- PtrSplit: Supporting General Pointers in Automatic Program PartitioningShen Liu, Gang Tan, Trent JaegerCCS 2017 · 被引用 83 次
- BMC: Accelerating Memcached using Safe In-kernel Caching and Pre-stack ProcessingYoann Ghigoff, Julien Sopena, Kahina Lazri, Antoine Blin 等NSDI 2021 · 被引用 79 次
- 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 次
相关 Paper
- 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 等USENIX Security 2024 · 被引用 18 次
- Verifying the Verifier: eBPF Range Analysis VerificationHarishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, Santosh NagarakatteCAV 2023 · 被引用 37 次
- A Flow-Sensitive Refinement Type System for Verifying eBPF ProgramsAmeer Hamza, Lucas Zavalía, Arie Gurfinkel, Jorge A. Navas 等OOPSLA 2025 · 被引用 1 次
- VEP: A Two-stage Verification Toolchain for Full eBPF ProgrammabilityXiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu 等NSDI 2025 · 被引用 8 次
