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 have produced the first draft of eBPF ISA standard. However, eBPF still lacks a formal reference specification with rigorous semantics. This paper presents a Sail formalization of Linux eBPF ISA based on Linux 7.1. The model covers all sequential instructions in the Linux eBPF. From the same Sail source, we generate a human-readable formal specification document and Rocq definitions, while we provide a handwritten Rocq driver with a CompCert-based memory adapter to execute the generated semantics.