A complete formal semantics of eBPF instruction set architecture for Solana
summary
First complete formal semantics for Solana eBPF, mechanized as a small‑step operational model that covers 116 opcodes and is extracted to executable Isabelle/HOL‑generated OCaml; validation runs the Solana test suite (including 114 normal cases and 32 exception cases, 14 excluded) and exhaustive per‑instruction comparisons against the Rust interpreter with all tested results matching. Includes glue code to bridge extracted types, finds real issues (missing version checks, assembler register‑range bug), and proves assembler/disassembler and JIT x86_64 arithmetic correctness.
AI-written summary · about
chapters (9)
- 0:00Formalizing Solana eBPF semantics
- 1:28Solana eBPF challenges
- 2:53Contributions and approach
- 4:17Syntax and semantics of Solana eBPF
- 5:17Validating against Rust
- 7:06Code extraction issues
- 8:11Formal semantics in Solana
- 9:38Conclusion and future
- 10:26Q&A
related talks
15mTowards a standardized eBPF ISA - Conformance testing
19mComparing the Precision of Abstract Operators in the eBPF Verifier using Differential(…)
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
36mTowards a Formally-verified Software Toolchain for open ISAs
40mFormal semantics for multi-language programs
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
13mWTF Is the SVM?
36mFlexible Instruction-Set Semantics via Abstract Monads