Formal Specification of Linux eBPF Instruction Set Architecture in Sail

Abstract

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 all 153 sequential instructions in the Linux 7.1 eBPF interpreter. For the remaining 28 atomic instructions, it defines encodings, register effects, and memory-effect annotations, but not a concurrent memory semantics. From the same Sail source, we generate a human-readable formal specification document and Rocq definitions. We also provide a handwritten Rocq execution layer consisting of a Rocq driver and a CompCert-backed runtime to execute the generated definitions.