一种用于验证eBPF程序的、对流程敏感的精化类型系统

《Proceedings of the ACM on Programming Languages》：A Flow-Sensitive Refinement Type System for Verifying eBPF Programs

扩展Berkeley数据包过滤器（eBPF）子系统需在内核中动态部署前验证用户态程序以保障安全。现有单一体验证方法依赖庞大可信代码库且全流程在安全环境执行。本文提出基于类型的安全验证框架，用户态自动生成证明证书，仅需安全环境部署验证组件，并引入类型注释增强调试性。实验表明工具VeRefine在工业基准测试中性能优于现有Prevail验证器。

　　

摘要

操作系统内核中的扩展伯克利数据包过滤器（eBPF）子系统允许用户空间程序动态扩展内核功能。由于在运行时修改操作系统存在安全风险，eBPF要求所有程序在部署到内核之前都必须经过验证。现有的eBPF验证方法都是整体性的，需要在整个安全环境中完成所有分析，这导致了对庞大可信代码库的需求。我们提出了一种基于类型的验证方法，该方法可以在用户空间自动生成证明证书，从而减少可信代码库的大小和复杂性。同时，只有证明检查组件需要部署在安全环境中。此外，与以往的技术相比，我们的类型系统在验证失败时通过符合人体工程学的类型注释提高了程序的可调试性。我们将这种类型推断算法实现在一个名为VeRefine的工具中，并将其与现有的eBPF验证器Prevail进行了对比测试。在大多数工业基准测试中，VeRefine的表现优于Prevail。