A Mechanized Semantics For eBPF And Its Applications In Program Verification
Resumo
The absence of a formally verified semantics for eBPF hampers the development of verified analysis tools and leaves JIT compilers and static analyzers without an authoritative reference. This paper presents a mechanized formalization of eBPF in Lean 4, comprising: (i) a small-step operational semantics over 64-bit machinewords and flat byte-addressed memory; (ii) a separation logic whose assertions are predicates over register files and partial heaps; (iii) a fully proved sound frame rule, with a semantic soundness theorem connecting the syntactic derivation system to the operational model; and (iv) a machine-checked, end-to-end correctness proof for an IPv4/TCP packet-filter program.
Palavras-chave:
eBPF, Separation Logic, Hoare Logic, Operational Semantics, Lean 4
Referências
Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17). Association for Computing Machinery, New York, NY, USA, 666–679. DOI: 10.1145/3009837.3009866
Anonymous. 2025. Executable Formal Specification of eBPF in Lean 4. OMITTED. Accessed on: July 20, 2025.
Cilium Authors. 2024. BPF and XDP Reference Guide. [link]. BPF and XDP Reference Guide - Cilium 1.16.0-dev documentation.
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K Rajamani, and Abdullah Ustuner. 2006. Thorough static analysis of device drivers. ACM SIGOPS Operating Systems Review 40, 4 (2006), 73–85.
Gilberto Bertin. 2017. XDP in practice: integrating XDP into our DDoS mitigation pipeline. In Netdev 2.1 - Technical Conference on Linux Networking. 1–5.
Facebook. 2025. Katran source code repository. [link].
Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, AndreiS, tefănescu, and Grigore Ros, u. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). DOI: 10.1109/CSF.2018.00022
Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576–580.
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. A Formally-Verified C Static Analyzer. In POPL 2015: 42nd symposium Principles of Programming Languages. ACM Press, 247–259. [link]
Alan Jowett. 2025. eBPF conformance tests. [link].
Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. In ERTS 2018: Embedded Real Time Software and Systems. SEE. [link]
Steven McCanne and Van Jacobson. 1993. The BSD packet filter: a new architecture for user-level packet capture. In Proceedings of the USENIX Winter 1993 Conference Proceedings on USENIX Winter 1993 Conference Proceedings (San Diego, California) (USENIX’93). USENIX Association, USA, 2.
Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15 , 2021, Proceedings. Springer-Verlag, Berlin, Heidelberg, 625–635. DOI: 10.1007/978-3-030-79876-5_37
Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 41–61.
Peter O’Hearn, John Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In InternationalWorkshop on Computer Science Logic. Springer, 1–19.
IOVisor Project. 2025. uBPF: A Userspace Virtual Machine for eBPF. [link]. Accessed on 2026-05-12.
David Pym, Jonathan M Spring, and Peter O’Hearn. 2019. Why separation logic works. Philosophy & Technology 32, 3 (2019), 483–516.
Liz Rice. 2023. Learning eBPF: Programming the Linux Kernel for Enhanced Observability, Networking, and Security. O’Reilly Media, Inc.
Jay Schulist, Daniel Borkmann, and Alexei Starovoitov. 2025. Linux Socket Filtering aka Berkeley Packet Filter (BPF). [link]. Accessed on 12/05/2026.
Gang Tan and Andrew W Appel. 2006. A compositional logic for control flow. In InternationalWorkshop on Verification, Model Checking, and Abstract Interpretation. Springer, 80–94.
Dave Thaler. 2024. BPF Instruction Set Architecture (ISA). RFC 9669. Internet Engineering Task Force. Standards Track.
The Linux Kernel Community. 2024. Berkeley Packet Filter (BPF) Documentation. [link]. Accessed on 05/12/2026.
Sebastian Ullrich and Leonardo de Moura. 2020. Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-5, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12166). Springer International Publishing, 167–182. DOI: 10.1007/978-3-030-51054-1_10
Marcos A. M. Vieira, Matheus S. Castanho, Racyus D. G. Pací fico, Elerson R. S. Santos, Eduardo P. M. Câmara Júnior, and Luiz F. M. Vieira. 2020. Fast Packet Processing with eBPF and XDP: Concepts, Code, Challenges, and Applications. ACM Comput. Surv. 53, 1, Article 16 (Feb. 2020), 36 pages. DOI: 10.1145/3371038
Shenghao Yuan, Frédéric Besson, and Jean-Pierre Talpin. 2024. End-to-end mechanized proof of a JIT-accelerated eBPF virtual machine for IoT. In International Conference on Computer Aided Verification. Springer, 325–347.
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, and Emmanuel Baccelli. 2022. End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. In International Conference on Computer Aided Verification. Springer, 293–316.
Anonymous. 2025. Executable Formal Specification of eBPF in Lean 4. OMITTED. Accessed on: July 20, 2025.
Cilium Authors. 2024. BPF and XDP Reference Guide. [link]. BPF and XDP Reference Guide - Cilium 1.16.0-dev documentation.
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K Rajamani, and Abdullah Ustuner. 2006. Thorough static analysis of device drivers. ACM SIGOPS Operating Systems Review 40, 4 (2006), 73–85.
Gilberto Bertin. 2017. XDP in practice: integrating XDP into our DDoS mitigation pipeline. In Netdev 2.1 - Technical Conference on Linux Networking. 1–5.
Facebook. 2025. Katran source code repository. [link].
Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, AndreiS, tefănescu, and Grigore Ros, u. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). DOI: 10.1109/CSF.2018.00022
Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576–580.
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. A Formally-Verified C Static Analyzer. In POPL 2015: 42nd symposium Principles of Programming Languages. ACM Press, 247–259. [link]
Alan Jowett. 2025. eBPF conformance tests. [link].
Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. In ERTS 2018: Embedded Real Time Software and Systems. SEE. [link]
Steven McCanne and Van Jacobson. 1993. The BSD packet filter: a new architecture for user-level packet capture. In Proceedings of the USENIX Winter 1993 Conference Proceedings on USENIX Winter 1993 Conference Proceedings (San Diego, California) (USENIX’93). USENIX Association, USA, 2.
Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15 , 2021, Proceedings. Springer-Verlag, Berlin, Heidelberg, 625–635. DOI: 10.1007/978-3-030-79876-5_37
Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 41–61.
Peter O’Hearn, John Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In InternationalWorkshop on Computer Science Logic. Springer, 1–19.
IOVisor Project. 2025. uBPF: A Userspace Virtual Machine for eBPF. [link]. Accessed on 2026-05-12.
David Pym, Jonathan M Spring, and Peter O’Hearn. 2019. Why separation logic works. Philosophy & Technology 32, 3 (2019), 483–516.
Liz Rice. 2023. Learning eBPF: Programming the Linux Kernel for Enhanced Observability, Networking, and Security. O’Reilly Media, Inc.
Jay Schulist, Daniel Borkmann, and Alexei Starovoitov. 2025. Linux Socket Filtering aka Berkeley Packet Filter (BPF). [link]. Accessed on 12/05/2026.
Gang Tan and Andrew W Appel. 2006. A compositional logic for control flow. In InternationalWorkshop on Verification, Model Checking, and Abstract Interpretation. Springer, 80–94.
Dave Thaler. 2024. BPF Instruction Set Architecture (ISA). RFC 9669. Internet Engineering Task Force. Standards Track.
The Linux Kernel Community. 2024. Berkeley Packet Filter (BPF) Documentation. [link]. Accessed on 05/12/2026.
Sebastian Ullrich and Leonardo de Moura. 2020. Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-5, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12166). Springer International Publishing, 167–182. DOI: 10.1007/978-3-030-51054-1_10
Marcos A. M. Vieira, Matheus S. Castanho, Racyus D. G. Pací fico, Elerson R. S. Santos, Eduardo P. M. Câmara Júnior, and Luiz F. M. Vieira. 2020. Fast Packet Processing with eBPF and XDP: Concepts, Code, Challenges, and Applications. ACM Comput. Surv. 53, 1, Article 16 (Feb. 2020), 36 pages. DOI: 10.1145/3371038
Shenghao Yuan, Frédéric Besson, and Jean-Pierre Talpin. 2024. End-to-end mechanized proof of a JIT-accelerated eBPF virtual machine for IoT. In International Conference on Computer Aided Verification. Springer, 325–347.
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, and Emmanuel Baccelli. 2022. End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. In International Conference on Computer Aided Verification. Springer, 293–316.
Publicado
08/09/2026
Como Citar
EMILIANO, Marcos Geraldo Braga; RIBEIRO, Rodrigo.
A Mechanized Semantics For eBPF And Its Applications In Program Verification. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 30. , 2026, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 37-45.
DOI: https://doi.org/10.5753/sblp.2026.27719.
