一句话：在 Rocq 中形式化 eBPF 核心 ISA 的全部 153 条指令，并据此验证 eBPF 验证器抽象域的可靠性、发现内核缺陷。
本文为 Linux eBPF 指令集架构（ISA）建立了机器化的形式语义。作者在 Rocq 中以小步语义刻画了全部 153 条内核顺序指令，该语义完全可执行，并用 Linux 官方 eBPF 测试套件加以验证；这一大规模测试暴露出原始形式化中的不一致之处。基于该语义，作者设计、实现并证明了 Linux eBPF 验证器所采用的位级抽象域（bit-level abstract domain）的可靠性。该工作还为现有 eBPF 文档提供了严格的形式规约补充。在形式化过程中，作者发现了内核实现中此前未知的缺陷，并提出新的验证器优化，相应的内核补丁已被上游合并。
This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA). We develop a small-step semantics in Rocq that faithfully formalizes all 153 sequential in-kernel instructions of the eBPF ISA. The semantics is fully executable and has been validated against the official Linux eBPF test suite. This extensive testing revealed inconsistencies in our original formalization. Using this semantics, we have designed, implemented, and verified the soundness of the bit-level abstract domain employed by the Linux eBPF verifier. Our semantics also complements the existing Linux eBPF documentation by providing a rigorous formal specification. During the formalization process, we have discovered previously unknown bugs in the Linux eBPF implementation, and developed new verifier optimizations; the corresponding kernel patches have been upstreamed.
@article{paperbot12074,
title = {Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications},
author = {Shenghao Yuan and Yazhou Tang and Tianci Cao and Frédéric Besson and Jean-Pierre Talpin and Mingshuai Chen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839449}
}