Jia, J., Qin, R., Craun, M., Lukiyanov, E., Bansal, A., Phan, M., Le, M. V., Franke, H., Jamjoom, H., Xu, T., & Williams, D. (2025, July). Rex: Closing the language-verifier gap with safe and usable kernel extensions. 2025 USENIX Annual Technical Conference (USENIX ATC 25). https://www.usenix.org/conference/atc25/presentation/jia
@inproceedings{rex-jinghao,
author = {Jia, Jinghao and Qin, Ruowen and Craun, Milo and Lukiyanov, Egor and Bansal, Ayush and Phan, Minh and Le, Michael V. and Franke, Hubertus and Jamjoom, Hani and Xu, Tianyin and Williams, Dan},
title = {Rex: Closing the language-verifier gap with safe and usable kernel extensions},
year = {2025},
booktitle = {2025 USENIX Annual Technical Conference (USENIX ATC 25)},
publisher = {USENIX Association},
url = {https://www.usenix.org/conference/atc25/presentation/jia},
month = jul,
file = {atc25-rex.pdf}
}
Chintamaneni, S., Somaraju, S. R., & Williams, D. (2024). Unsafe kernel extension composition via BPF program nesting. Proceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions, 65–67. https://doi.org/10.1145/3672197.3673440
@inproceedings{10.1145/3672197.3673440,
author = {Chintamaneni, Siddharth and Somaraju, Sai Roop and Williams, Dan},
title = {Unsafe kernel extension composition via BPF program nesting},
year = {2024},
isbn = {9798400707124},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3672197.3673440},
doi = {10.1145/3672197.3673440},
booktitle = {Proceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions},
pages = {65–67},
numpages = {3},
keywords = {callgraph, dynamic tracing, eBPF},
location = {Sydney, NSW, Australia},
series = {eBPF '24}
}
BPF programs provide the ability to extend the kernel while ensuring safety. The safety guarantees are provided by the in-kernel verifier. However, the verification guarantees may not hold when multiple BPF programs interact with each other through helper functions. This is because, while verifying a BPF program, the verifier considers each BPF program as an individual unit rather than part of a composite system. One aspect affected by this unsafe composition is the kernel stack. In this paper, we highlight how different possible nesting scenarios can affect the safety of the kernel stack. To address this problem, we propose a helper-rooted callgraph-based approach, which enables the verifier to have a global view of the system. By using the callgraph and maximum stack depth information during verification, the verifier will either accept or reject a program by considering all the possible nesting scenarios, which ensures runtime stack safety.
Craun, M., Hussain, K., Gautam, U., Ji, Z., Rao, T., & Williams, D. (2024). Eliminating eBPF Tracing Overhead on Untraced Processes. Proceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions, 16–22. https://doi.org/10.1145/3672197.3673431
@inproceedings{10.1145/3672197.3673431,
author = {Craun, Milo and Hussain, Khizar and Gautam, Uddhav and Ji, Zhengjie and Rao, Tanuj and Williams, Dan},
title = {Eliminating eBPF Tracing Overhead on Untraced Processes},
year = {2024},
isbn = {9798400707124},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3672197.3673431},
doi = {10.1145/3672197.3673431},
booktitle = {Proceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions},
pages = {16–22},
numpages = {7},
keywords = {copy-on-write, dynamic tracing, eBPF, tracing overhead},
location = {Sydney, NSW, Australia},
series = {eBPF '24}
}
Current eBPF-based kernel extensions affect entire systems, and are coarse-grained. For some use cases, like tracing, operators are more interested in tracing a subset of processes (e.g., belonging to a container) rather than all processes. While overhead from tracing is expected for targeted processes, we find untraced processes—those that are not the target of tracing—also incur performance overhead. To better understand this overhead, we identify and explore three techniques for per-process filtering for eBPF: post-eBPF, in-eBPF, and pre-eBPF filtering, finding that all three approaches result in excessive overhead on untraced processes. Finally, we propose a system that allows for zero-untraced-overhead per-process eBPF tracing by modifying kernel virtual memory mappings to present per-process kernel views, effectively enabling untraced processes to execute on the kernel as if no eBPF programs are attached.
Jia, J., Sahu, R., Oswald, A., Williams, D., Le, M. V., & Xu, T. (2023). Kernel Extension Verification is Untenable. Proceedings of the 19th Workshop on Hot Topics in Operating Systems, 150–157. https://doi.org/10.1145/3593856.3595892
@inproceedings{10.1145/3593856.3595892,
author = {Jia, Jinghao and Sahu, Raj and Oswald, Adam and Williams, Dan and Le, Michael V. and Xu, Tianyin},
title = {Kernel Extension Verification is Untenable},
year = {2023},
isbn = {9798400701955},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3593856.3595892},
doi = {10.1145/3593856.3595892},
booktitle = {Proceedings of the 19th Workshop on Hot Topics in Operating Systems},
pages = {150–157},
numpages = {8},
keywords = {eBPF, safety, operating system, kernel extension, verification},
location = {Providence, RI, USA},
series = {HOTOS '23}
}
The emergence of verified eBPF bytecode is ushering in a new era of safe kernel extensions. In this paper, we argue that eBPF’s verifier—the source of its safety guarantees—has become a liability. In addition to the well-known bugs and vulnerabilities stemming from the complexity and ad hoc nature of the in-kernel verifier, we highlight a concerning trend in which escape hatches to unsafe kernel functions (in the form of helper functions) are being introduced to bypass verifier-imposed limitations on expressiveness, unfortunately also bypassing its safety guarantees. We propose safe kernel extension frameworks using a balance of not just static but also lightweight runtime techniques. We describe a design centered around kernel extensions in safe Rust that will eliminate the need of the in-kernel verifier, improve expressiveness, allow for reduced escape hatches, and ultimately improve the safety of kernel extensions.
Craun, M., Oswald, A., & Williams, D. (2023). Enabling eBPF on Embedded Devices Through Decoupled Verification. Proceedings of ACM SIGCOMM Workshop on EBPF and Kernel Extensions (EBPF ’23). https://doi.org/10.1145/3609021.3609299
@inproceedings{ebpf23-decoupled-verification,
author = {Craun, Milo and Oswald, Adam and Williams, Dan},
title = {Enabling eBPF on Embedded Devices Through Decoupled Verification},
year = {2023},
booktitle = {Proceedings of ACM SIGCOMM Workshop on eBPF and Kernel Extensions (eBPF ’23)},
file = {ebpf23-decoupled.pdf},
url = {https://doi.org/10.1145/3609021.3609299},
doi = {10.1145/3609021.3609299}
}
Sahu, R., & Williams, D. (2023). Enabling BPF Runtime policies for better BPF management. Proceedings of ACM SIGCOMM Workshop on EBPF and Kernel Extensions (EBPF ’23). https://doi.org/10.1145/3609021.3609296
@inproceedings{ebpf23-runtime,
author = {Sahu, Raj and Williams, Dan},
title = {Enabling BPF Runtime policies for better BPF management},
year = {2023},
booktitle = {Proceedings of ACM SIGCOMM Workshop on eBPF and Kernel Extensions (eBPF ’23)},
file = {ebpf23-runtime.pdf},
url = {https://doi.org/10.1145/3609021.3609296},
doi = {10.1145/3609021.3609297}
}