A Flow-Sensitive Refinement Type System for Verifying eBPF Programs

doi:10.1145/3763799

A Flow-Sensitive Refinement Type System for Verifying eBPF Programs

2025-10-01

0

PRE

AI

DOI：10.1145/3763799

原文求助

摘要

En 中文

操作系统内核中的扩展伯克利包过滤器（EBPF）子系统使用户空间程序能够动态扩展内核功能。由于与操作系统运行时修改相关的安全风险，EBPF要求所有程序在部署到内核之前进行验证。现有的EBPF验证方法都是一体化的，要求其整个分析过程在安全环境中完成，从而导致需要庞大的可信代码库。我们提出了一种基于类型的验证方法，可在用户空间自动推断证明证书，从而减少可信代码库的规模和复杂性。同时，只有证明检查组件需要部署在安全环境中。此外，与以往技术相比，我们的类型系统在验证失败时通过人机工程学类型注解增强了用户程序的调试能力。我们将类型推断算法实现于一个名为VEREFINE的工具中，并将其与现有的EBPF验证器PREVAIL进行了比较评估。VEREFINE在大多数工业基准测试中表现优于PREVAIL。

Keyword:

Flow-Sensitivity

Refinement Types

Type Inference

Memory Safety

Information Flow Safety

Automated Reasoning about Low-Level Code

A Flow-Sensitive Refinement Type System for Verifying eBPF Programs

摘要

期刊

机构