Technical Summary: Heimdall

Problem Statement

Extended Berkeley Packet Filter (eBPF) programs are critical for Linux kernel extensions in networking, observability, and security. While the in-kernel eBPF verifier enforces low-level memory safety and termination, it fails to enforce higher-level source-level properties such as initialization discipline, schema consistency, and error handling. The authors document six classes of source-level bugs that compile and pass the kernel verifier but can silently corrupt data, leak sensitive information, or yield incorrect enforcement outcomes.

Key vulnerabilities identified include:

• Uninitialized State: Programs emitting stack-resident structs without zero-initialization leak per-CPU stack residue, including kernel pointers and return addresses sufficient to recover Kernel Address Space Layout Randomization (KASLR) slides.
• Unchecked Helper Returns: Helper functions (e.g., bpf_probe_read_user_str) that fail are often ignored, causing the emission of stale stack data instead of truncated strings.
• Buffer/Size Mismatches: Developers passing incorrect sizes to output helpers can leak adjacent private fields containing kernel pointers.
• Hook/Context Mismatches: Using incorrect context structures (e.g., __sk_buff in an XDP hook) leads to misinterpreted data.
• Map Type/Schema Confusion: Mismatches between declared map value sizes and actual data, or reinterpreting map lookup results as unrelated types.
• Signed/Unsigned Confusion: Storing signed helper return values (indicating errors) in unsigned fields creates spurious large positive values used as map keys.

Furthermore, the eBPF verifier itself has known vulnerabilities (e.g., unsound pruning, missing contract validation) that can be exploited. Migration to a memory-safe language like Rust could close these gaps, but manual rewriting is impractical at scale, and existing automated translation tools lack the rigor to ensure semantic equivalence or safety in the eBPF context.

Methodology: The Heimdall Pipeline

Heimdall is an automated pipeline that translates legacy libbpf C programs to idiomatic, safe Aya Rust. It employs a five-stage iterative process combining Large Language Models (LLMs), static analysis, and formal verification:

1. LLM Translation: An LLM translates the C source to Rust using Aya API mappings, hook macros, and working examples.
2. Compile and Kernel Verify: The generated Rust code is compiled to eBPF bytecode. Compiler lint guards (e.g., denying unused unsafe blocks) and the kernel verifier check for basic safety and correctness. Errors are fed back to the LLM for repair.
3. Safety Check (Static Analysis): A custom static analysis engine scans the Rust source for unsafe escape hatches that the compiler and verifier might miss. This includes banning untyped ring-buffer reservations, enforcing zero-initialization, and requiring explicit handling of Result types for helper returns.
4. Symbolic Execution: Both the original C binary and the compiled Rust binary are loaded into a custom eBPF backend for angr. This backend models eBPF helpers, maps, relocations, and atomic operations. It performs symbolic execution to explore all feasible paths, generating structured formulae for return values and map side effects.
5. Equivalence Checking: A Z3-based solver checks if the C and Rust programs are semantically equivalent. The authors introduce Conditional Semantic Equivalence, which requires equivalence only on inputs that satisfy declared safety conditions (e.g., helper calls succeeding). This allows the safer Rust translation (which handles errors or zero-fills memory) to be considered equivalent to the buggy C source on the paths where the bug is triggered, while still verifying that the logic is preserved on valid paths. If a counter-example is found, it is fed back to the LLM for targeted repair.

To support this, the authors built a complete eBPF backend for angr, including an ELF loader, architecture definition, VEX IR lifter, and helper stubs. They also developed a custom ITE-chain encoding to model map side effects under symbolic keys, capturing "last-write-wins" semantics.

Key Contributions

• Heimdall Pipeline: The first automated system to translate production eBPF programs from C to Rust with per-program formal guarantees of observable behavior preservation.
• Conditional Equivalence: A novel verification approach that validates safety-improving translations (which behave differently on bug-triggering paths) by restricting equivalence checks to safe execution paths.
• eBPF Symbolic Execution Backend: A full eBPF backend for angr that models kernel helpers, maps, and BPF-to-BPF calls, enabling formal reasoning at the bytecode level.
• Safe-Aya Static Analyzer: A policy engine that rejects unsafe Rust patterns (e.g., untyped ring buffers, ignored helper errors) that pass the kernel verifier.
• Security Findings: Discovery of previously unreported information leaks in ten open-source eBPF programs, including KASLR recovery via stack residue and cross-event content leaks in ring buffers.
• Benchmark and Evaluation: A public benchmark of 102 eBPF programs and a comprehensive evaluation of the translation pipeline.

Results

The system was evaluated on 102 real-world eBPF programs from various sources (libbpf-tools, libbpf-bootstrap, KEN, Suricata, etc.).

• Success Rate: Heimdall produced 96 formally verified-equivalent translations (94.1%). The remaining six were either partially verified (due to symbolic execution limits) or exceeded solver scalability limits.
• Bug Closure: In the 96 verified translations, Heimdall closed 100% of observed instances of uninitialized state, unchecked helper returns, and signed/unsigned confusion.
• Comparison to Baselines: Compared to baseline LLM agents without the Heimdall pipeline, Heimdall (Agentic) achieved a 98% triple-pass rate (Compile, Kernel Verify, Safety, Equivalence) versus 4–12% for baselines.
• Runtime Overhead: Runtime validation on 10 programs showed that Rust translations generally incurred modest overhead (geometric mean ranging from 0.44× to 3.60× compared to C), with most falling between 1.14× and 1.89×.
• Safety: The translations eliminated the specific unsafe patterns (uninitialized memory, unchecked errors) that caused the identified vulnerabilities.

Significance

The paper claims Heimdall is the first system to automate the memory-safe migration of production eBPF programs with per-program formal guarantees that the migration preserves observable behavior. It addresses the gap between the kernel verifier's low-level guarantees and the high-level safety requirements of modern eBPF applications. By combining LLMs with formal verification and static analysis, Heimdall demonstrates that automated translation can produce code that is not only syntactically correct but also semantically equivalent and free of specific classes of source-level safety bugs that the kernel verifier cannot detect. The work establishes a new benchmark for eBPF migration and provides a foundation for building more robust, memory-safe kernel extensions.