More Like this

1. BPF for Storage: an Exokernel-Inspired Approach

   https://doi.org/10.1145/3458336.3465290  

   Zhong, Yuhong; Wang, Hongyi; Wu, Yu Jian; Cidon, Asaf; Stutsman, Ryan; Tai, Amy; Yang, Junfeng (June 2021, Proceedings of the Workshop on Hot Topics in Operating Systems)
2. BeeBox: Hardening BPF against Transient Execution Attacks

   Jin, Di; Gaidis, Alexander J; Kemerlis, Vasileios P (August 2024, USENIX)
3. Unsafe kernel extension composition via BPF program nesting

   https://doi.org/10.1145/3672197.3673440  

   Chintamaneni, Siddharth; Somaraju, Sai Roop; Williams, Dan (August 2024, ACM)
4. BPF-oF: Storage Function Pushdown Over the Network

   Zarkadas, Ioannis; Zussman, Tal; Carin, Jeremy; Jiang, Sheng; Zhong, Yuhong; Pfefferle, Jonas; Franke, Hubertus; Yang, Junfeng; Kaffes, Kostis; Stutsman, Ryan; et al (September 2023, Arxiv)
5. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel

   Nelson, Luke; Van Geffen, Jacob; Torlak, Emina; Wang, Xi (January 2020, 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20))

   This paper describes our experience applying formal meth- ods to a critical component in the Linux kernel, the just-in-time compilers (“JITs”) for the Berkeley Packet Filter (BPF) virtual machine. We verify these JITs using Jitterbug, the first frame- work to provide a precise specification of JIT correctness that is capable of ruling out real-world bugs, and an automated proof strategy that scales to practical implementations. Using Jitterbug, we have designed, implemented, and verified a new BPF JIT for 32-bit RISC-V, found and fixed 16 previously unknown bugs in five other deployed JITs, and developed new JIT optimizations; all of these changes have been upstreamed to the Linux kernel. The results show that it is possible to build a verified component within a large, unverified system with careful design of specification and proof strategy. 

   more » « less