eBPF

Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications

This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA). We develop a small-step …

Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, Mingshuai Chen