Verified programs can party: optimizing kernel extensions via post-verification merging
Hsuan-Chi Kuo, Kai-Hsun Chen, Yicheng Lu, Dan Williams, Sibin Mohan, Tianyin Xu
Abstract
Operating system (OS) extensions are more popular than ever. For example, Linux BPF is marketed as a "superpower" that allows user programs to be downloaded into the kernel, verified to be safe and executed at kernel hook points. So, BPF extensions have high performance and are often placed at performance-critical paths for tracing and filtering.
However, although BPF extension programs execute in a shared kernel environment and are already individually verified, they are often executed independently in chains. We observe that the chain pattern has large performance overhead, due to indirect jumps penalized by security mitigations (e.g., Spectre), loops, and memory accesses.
In this paper, we argue for a separation of concerns. We propose to decouple the execution of BPF extensions from their verification requirements-BPF extension programs can be collectively optimized, after each BPF extension program is individually verified and loaded into the shared kernel.
We present KFuse, a framework that dynamically and automatically merges chains of BPF programs by transforming indirect jumps into direct jumps, unrolling loops, and saving memory accesses, without loss of security or flexibility. KFuse can merge BPF programs that are (1) installed by multiple principals, (2) maintained to be modular and
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 papers9
- Finding Correctness Bugs in eBPF Verifier with Structured and Sanitized ProgramHao Sun, Yiru Xu, Jianzhong Liu, Yuheng Shen et al.EuroSys 2024 · 24 citations
- Merlin: Multi-tier Optimization of eBPF Code for Performance and CompactnessJinsong Mao, Hailun Ding, Juan Zhai, Shiqing MaASPLOS 2024 · 15 citations
- NetEdit: An Orchestration Platform for eBPF Network Functions at ScaleTheophilus A. Benson, Prashanth Kannan, Prankur Gupta, Balasubramanian Madhavan et al.SIGCOMM 2024 · 11 citations
- eNetSTL: Towards an In-kernel Library for High-Performance eBPF-based Network FunctionsBin Yang, Dian Shen, Junxue Zhang, Hanlin Yang et al.EuroSys 2025 · 9 citations
- Revealing the Unstable Foundations of eBPF-Based Kernel ExtensionsShawn Wanxiang Zhong, Jing Liu, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-DusseauEuroSys 2025 · 4 citations
Builds on11
- Spectre Attacks: Exploiting Speculative ExecutionPaul Kocher, Jann Horn, Anders Fogh, Daniel Genkin et al.S&P 2019 · 2,435 citations
- Meltdown: Reading Kernel Memory from User SpaceMoritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher et al.USENIX Security 2018 · 1,456 citations
- Twine: A Unified Cluster Management System for Shared InfrastructureChunqiang Tang, Kenny Yu, Kaushik Veeraraghavan, Jonathan Kaldor et al.OSDI 2020 · 107 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
- SANRAZOR: Reducing Redundant Sanitizer Checks in C/C++ ProgramsJiang Zhang, Shuai Wang, Manuel Rigger, Pinjia He et al.OSDI 2021 · 38 citations
Related papers
- Fast, Flexible, and Practical Kernel ExtensionsKumar Kartikeya Dwivedi, Rishabh R. Iyer, Sanidhya KashyapSOSP 2024 · 7 citations
- Synthesizing safe and efficient kernel extensions for packet processingQiongwen Xu, Michael D. Wong, Tanvi Wagle, Srinivas Narayana et al.SIGCOMM 2021 · 30 citations
- VEP: A Two-stage Verification Toolchain for Full eBPF ProgrammabilityXiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu et al.NSDI 2025 · 8 citations
- Approximation Enforced Execution of Untrusted Linux Kernel ExtensionsHao Sun, Zhendong SuUSENIX Security 2025
- BeeBox: Hardening BPF against Transient Execution AttacksDi Jin, Alexander J. Gaidis, Vasileios P. KemerlisUSENIX Security 2024 · 10 citations
