Formal Specification of Linux eBPF Instruction Set Architecture in Sail
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...