一句话：提出流敏感精化类型系统，在用户态自动推断 eBPF 验证证明证书，缩小可信基并提升可调试性。
eBPF 允许用户态程序动态扩展内核功能，但出于安全风险，所有程序必须在内核部署前通过验证。现有 eBPF 验证方法呈单体化结构，整个分析都必须在安全环境中执行，导致可信代码库庞大且复杂。本文提出一种基于类型的验证方法，在用户态自动推断证明证书，从而只需将证明检查组件部署在安全环境中，显著缩小可信基。其核心是流敏感的精化类型系统，支持自动类型推断，并在验证失败时通过更符合使用习惯的类型标注提升程序可调试性。作者实现了类型推断工具 VeRefine，并与现有 eBPF 验证器 Prevail 在工业基准上进行比较；结果表明，VeRefine 在大多数基准上优于 Prevail。
The Extended Berkeley Packet Filter ( eBPF ) subsystem within an operating system’s kernel enables userspace programs to extend kernel functionality dynamically. Due to the security risks associated with runtime modification of the operating system, eBPF requires all programs to be verified before deploying them within the kernel. Existing approaches to eBPF verification are monolithic, requiring their entire analysis to be done in a secure environment, resulting in the need for extensive trusted codebases. We present a typebased verification approach that automatically infers proof certificates in userspace, thus reducing the size and complexity of the trusted codebase. At the same time, only the proof-checking component needs to be deployed in a secure environment. Moreover, compared to previous techniques, our type system enhances the debuggability of the programs for users through ergonomic type annotations when verification fails. We implemented our type inference algorithm in a tool called VeRefine and evaluated it against an existing eBPF verifier, Prevail . VeRefine outperformed Prevail on most of the industrial benchmarks.
@article{paperbot3018,
title = {A Flow-Sensitive Refinement Type System for Verifying eBPF Programs},
author = {Ameer Hamza and Lucas Zavalia and Arie Gurfinkel and Jorge A. Navas and Grigory Fedyukovich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763799}
}