BeePL: Correct-by-compilation kernel extensions
summary
BeePL is a new source language whose type system encodes eBPF specs (effects, substructural and refinement types) and whose goal is a Coq-verified compiler that preserves safety down to BPF bytecode. Plan uses CompCert extended to emit BPF and machine-checked proofs of functional correctness and preservation; current work is early-stage with paper proofs and a prototype pipeline planned. Targets concrete limits like the 512-byte stack bound and verifier quirks (e.g. 1,000,000 instruction verifier limit) rather than vague safety claims.
AI-written summary · about
chapters (5)
- 0:00BeePL introduction
- 2:30eBPF verifier limits
- 7:03BeePL design goals
- 11:21Type system verification
- 14:30Q&A on BeePL
related talks
24mCompiling for verified targets BPF
15mTowards a standardized eBPF ISA - Conformance testing
46mWhat is PL Research?
45mSupporting BPF in the GNU Toolchain
15mMy Journey in Secure Compilation
31mPfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagr...
24mGenerating BPF Verifier Friendly Code with Clang
50mCompCert: a journey through the landscape of mechanized semantics for verified co...