eBPF Formal Semantics in Rocq

eBPF 形式语义构建

在 Rocq (Coq) 中实现 Linux 内核 eBPF 虚拟机指令集的形式化语义。

主要工作

• 通过官方测试及自动化验证工具验证与原实现语义一致性
• 为 Linux 内核 eBPF 提供形式语义支持，支撑后续安全验证研究
• CCF-A 类编程语言领域顶会论文在投

相关链接

• OpenSourceVerif Organization