Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
2026-05-25 • Cryptography and Security
Cryptography and SecuritySymbolic Computation
AI summaryⓘ
The authors study eBPF programs, which run inside the Linux kernel to help with networking and security. They find that while the kernel checks some safety rules, it misses higher-level issues that can cause data leaks or bugs. They discover real leaks in popular eBPF software that expose sensitive information. To fix these problems, the authors created Heimdall, a tool that automatically converts old C eBPF programs into safer Rust code, making sure the new code behaves the same as the old. Heimdall succeeds in safely translating most tested programs and provides formal proof that the new versions work correctly.
eBPFLinux kernelkernel verifiermemory safetyRust programming languageformal verificationsymbolic executionZ3 solvercode migrationstatic analysis
Authors
Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari, Gang Tan
Abstract
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.