Authors

Yanze Li, Reto Achermann, Ivan Beschastnikh and Alexander J. Summers

Venue

Proceedings of the 4th Workshop on EBPF and Kernel Extensions (eBPF'26)

Links

[ .doi ] [ .pdf ] [ .bib ]

Abstract

Bibtex

@inproceedings{Li:2026:UnifyingeBPF,
 abstract = {eBPF is no longer a single-platform technology. It runs in the Linux kernel, on Windows, in user space, on microcontrollers, and in blockchain virtual machines, on independently built runtimes. The IETF ISA standard, RFC 9669, pins down the core instructions but leaves out features that real programs depend on, such as helper functions and maps. We are building an executable formal semantics for eBPF in F* that explicitly distinguishes cross-platform and platform-specific behaviors. Our semantics passes the BPF conformance test suite on par with uBPF, bpftime, Linux, and Windows, and we are extending it beyond the core ISA to other shared features the RFC omits. Using Meta-F* metaprogramming, we can also generate prose specifications in structured English that provably match the model. We envision this semantics as a practical foundation for a uniform, trustworthy eBPF across platforms.},
 address = {New York, NY, USA},
 author = {Li, Yanze and Achermann, Reto and Beschastnikh, Ivan and Summers, Alexander J.},
 booktitle = {Proceedings of the 4th Workshop on EBPF and Kernel Extensions},
 doi = {10.1145/3837779.3838165},
 id = {Li:2026:UnifyingeBPF},
 isbn = {9798400729119},
 keywords = {eBPF, formal semantics, conformance testing},
 location = {Prague, Czech Republic},
 numpages = {3},
 pages = {97–99},
 publisher = {Association for Computing Machinery},
 series = {eBPF'26},
 title = {Unifying eBPF across Platforms: Formal Semantics, Conformance Testing, and Specifications},
 url = {https://doi.org/10.1145/3837779.3838165},
 year = {2026}
}