Sep 2026· Proceedings of the 4th Workshop on eBPF and Kernel Extensions· pp. 97-99· 0 citations· 4 references
TL;DR
This work is building an executable formal semantics for eBPF in F* that explicitly distinguishes cross-platform and platform-specific behaviors and envision this semantics as a practical foundation for a uniform, trustworthy eBPF across platforms.
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.
eBPF has become a widely used mechanism for extending the Linux kernel, and recent standardization efforts resulted in RFC 9669, the first eBPF ISA standard. However, eBPF still lacks a formal ISA reference that is both executable and presented as an ISA-style document. This paper presents a Sail formalization covering...
Ya-Zhou Tang, Sheng-Hao Yuan, J. Talpin et al.· Proceedings of the 4th Works...· 0 citations
Janus is presented, an LLM-assisted framework that synthe-sizes custom instructions integrated into the Ibex RISC-V core while keeping correctness outside the agent, demonstrating a practical path for using LLMs to explore ISA specialization without making the agent part of the trusted correctness boundary.
This work develops a new methodology for verifying cryptographic software and extends SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code.
Ho Son, C. Fournet, Jonathan Protzenko et al.· 0 citations
eBPF allows user-defined programs to safely extend Linux kernel functionality at runtime, but its final machine code comes from a compilation pipeline that differs from native targets, and how efficient that pipeline is has no clear reference point. Our work constructs one: using the standard LLVM x86 backend as an app...
Hoang Duong, Hao Sun, Zhendong Su· Proceedings of the 4th Works...· 0 citations
Trusted execution environments (TEEs) have become a key building block for privacy-preserving and confidential computing because they protect sensitive code and data through hardware-assisted isolation. However, the current TEE ecosystem remains highly fragmented. Different platforms expose different execution abstract...
Di Lu, Qing-Wen Zhang, Yujia Liu et al.· Journal of networking and ne...· 0 citations
The Signal protocol is a prominent messaging protocol that secures communication for billions of users. It powers WhatsApp, the most widely used messaging application worldwide, and the Signal app, popular among privacy-conscious users. Extensive research in the computational and Dolev-Yao settings provides strong form...
Moustafa Said, Aurora Naska, Kevin Morio et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
