Heimdall：为迁移到 Rust 而形式化验证的自动化遗留 eBPF 程序
密码学与安全
2026-05-26 v1 符号计算
摘要
扩展伯克莱包过滤器 (eBPF) 程序是 Linux 内核中用于网络、可观察性和安全强制的内核扩展。内核 eBPF 验证器检查 eBPF 程序的低级内存安全和终止性，但不强制执行许多更高级别的源级属性，如初始化规范、模式一致性或错误处理。我们记录了六类源级错误，这些错误可编译、通过内核验证器，并可能在数据方面静默地损坏数据、泄露先前被追踪的事件到用户空间，或产生不正确的强制结果。在这些错误中，我们识别了十个开源 eBPF 程序中此前未报告的信息泄露，其环形缓冲区或堆栈居留的事件记录包含可完全解码的先前被追踪的事件，包括足以在每一次事件中恢复 KASLR 位移的用户标识路径和内核文本返回地址。为加固这些验证器接受的有缺陷程序并支持安全迁移，我们提出了 Heimdall，一个自动化管道，使用大语言模型将遗留 libbpf C 程序翻译为 Aya Rust。Heimdell 迭代修复编译和内核验证器失败，拒绝 Rust-Aya 中不安全的逃逸路径，并通过符号执行和 Z3 基于等效性检查证明每个程序与原始程序的等效性。在 102 个 eBPF 程序中，Heimdall 生成 96 个形式化证明等效的翻译 (94.1%)。Heimdell 是第一个自动化迁移生产级 eBPF 程序的系统，具有每个程序形式化保证，确保迁移保留可观察行为。
引用
@article{arxiv.2605.25411,
title = {Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust},
author = {Vishnu Asutosh Dasu and Monika Santra and Md Rafi Ur Rashid and Ashish Kumar and Saeid Tizpaz-Niari and Gang Tan},
journal= {arXiv preprint arXiv:2605.25411},
year = {2026}
}