Extended Berkeley Packet Filter (eBPF) programs are kernel extensions used for networking, observability, and security enforcement in the Linux kernel. The in-kernel eBPF verifier checks low-level memory safety and termination on eBPF programs, but it does not enforce many higher-level source-level properties, such as initialization discipline, schema consistency, or error handling. We document six classes of source-level bugs that compile, pass the kernel verifier, and can silently corrupt data, leak previously traced events to userspace, or yield incorrect enforcement outcomes. Among these, we identify previously unreported information leaks in ten open-source eBPF programs whose ring-buffer or stack-resident event records carry fully decodable prior traced events, including user-identifying paths and recurring kernel-text return addresses sufficient to recover the KASLR slide on every event, into userspace. To harden such verifier-accepted buggy programs and support safe migration, we present Heimdall, an automated pipeline that uses large language models to translate legacy libbpf C programs to Aya Rust. Heimdall iteratively repairs compilation and kernel-verifier failures, rejects unsafe escape hatches in Rust-Aya with a static analysis safety engine, and proves per-program equivalence to the original via symbolic execution and Z3-based equivalence checking. Across 102 eBPF programs, Heimdall produces 96 formally proven-equivalent translations (94.1%). Heimdall is the first system to automate memory-safe-language migration of production eBPF programs with per-program formal guarantees that the migration preserves observable behavior.

翻译：扩展的伯克利数据包过滤器（eBPF）程序是Linux内核中用于网络、可观测性与安全强制的内核扩展。内核中的eBPF验证器检查eBPF程序的低级内存安全性和终止性，但并未实施许多较高级别的源级性质，例如初始化规范、模式一致性或错误处理。我们记录了六类源级错误，这些错误能够编译通过、通过内核验证器，并可静默破坏数据、将先前追踪的事件泄露至用户空间，或产生错误的强制结果。其中，我们在十个开源eBPF程序中识别出先前未报告的信息泄露：这些程序的环形缓冲区或栈驻留事件记录将完全可解码的先前追踪事件（包括用户标识路径和足以恢复每次事件KASLR偏移量的重复内核文本返回地址）带入用户空间。为加固此类验证器可接受但有缺陷的程序并支持安全迁移，我们提出Heimdall——一个使用大语言模型将遗留libbpf C程序转换为Aya Rust的自动化流水线。Heimdall通过迭代修复编译与内核验证器失败、借助静态分析安全引擎拒绝Rust-Aya中的不安全逃逸机制、以及通过符号执行与基于Z3的等价性检查证明每程序与原程序的等价性。在102个eBPF程序上，Heimdall生成了96个经形式化证明等价的翻译（94.1%）。Heimdall是首个实现生产环境eBPF程序向内存安全语言自动化迁移的系统，能够为每个迁移程序提供迁移保留可观测行为的形式化保证。