arXiv:2605.25411v1 [cs.CR] 25 May 2026
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust Vishnu Asutosh Dasu
Monika Santra
Md Rafi Ur Rashid
Pennsylvania State University State College, USA [email protected]
Pennsylvania State University State College, USA [email protected]
Pennsylvania State University State College, USA [email protected]
Ashish Kumar
Saeid Tizpaz-Niari
Gang Tan
Pennsylvania State University State College, USA [email protected]
University of Illinois Chicago, USA [email protected]
Pennsylvania State University State College, USA [email protected]
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.
CCS Concepts • Security and privacy → Operating systems security; • Software and its engineering → Software verification and validation.
Keywords large language models, eBPF, Rust, program translation, symbolic execution, equivalence verification, angr, Z3
1
Introduction
The extended Berkeley Packet Filter (eBPF) lets developers extend the Linux kernel without modifying its source: a small program is compiled, loaded into the kernel via the bpf() syscall, vetted
by an in-kernel verifier that enforces memory safety and bounded execution, and then runs in response to events such as system calls, network packets, or function entries. eBPF programs are now the backbone for high-performance networking [23], continuous profiling [48], security policy enforcement [15], and system observability [9, 29] across virtually every modern Linux deployment, and the verifier is widely treated as the trust boundary that makes loading untrusted code into the kernel safe at scale. However, the eBPF verifier’s guarantees have gaps. Certain classes of safety and correctness bugs compile, load, and run without complaint, such as memory left uninitialized before being sent to userspace and helper return values that are silently discarded (Section 2 details a list of such issues). Consider bashreadline, a libbpf-tools [9] utility that traces interactive bash command lines via a uretprobe on readline. The handler declares an 84-byte stack-resident struct str_t without zero-initialization, calls bpf_probe_read_user_str to copy the returned string into one of its fields (writing only up to the string’s terminating \0), and emits the full struct via bpf_perf_event_output. The trailing bytes per event are never written by any source-level code path. They hold per-CPU BPF stack residue, including helper return values spilled by other recently-executed BPF programs on the same CPU. We loaded the program and ran it under a stock workload of short typed commands. We observe that all the perf-buffer events expose kernel-pointer-shaped trailing bytes. Across two independent 50-event runs, two distinct kernel-text return addresses (do_fault+0xf0 and mtree_load+0x271) recur identically. Cross-checked against /proc/kallsyms and /boot/System.map, both yield the same Kernel Address Space Layout Randomization (KASLR) slide of 0x0e600000, fully recovering the live kernel-text base and defeating KASLR. The same uninitialized-state gap also leaks prior event content rather than kernel pointers. mountsnoop, a mount-syscall tracer in the same libbpf-tools collection that backs commercial observability platforms, reserves a kernel ring-buffer slot for each traced event and writes only the active arm of an anonymous union before submitting the slot to userspace. On every umount, fsopen, fsconfig, fsmount, or move_mount syscall, which account for five of the six paths the program traces, the trailing kilobytes of the slot are never written by any source-level code path. We loaded the program on the same kernel and ran it under a stock workload. The kernel verifier accepts the program without warning. Once the ring
Conference’17, July 2017, Washington, DC, USA
buffer cycles, subsequent UMOUNT-class events leak fully decodable previous traced records into userspace—the kernel’s internal ring-buffer header followed by the previous record’s PID, command name, mount filesystem type, and source and destination paths. In our run those paths carried numeric UIDs from per-user systemd credential paths, exposing which users had triggered earlier mount operations. The verifier was not designed to catch issues of this kind, and yet, increasingly, eBPF is the vehicle through which such bugs reach the kernel. Migration of eBPF programs to a memory-safe language can help close source-level safety gaps, but toolchain complexity, instruction-limit constraints, and ecosystem inertia have kept this path largely unrealized [27]. Aya is the natural memory-safe target: an eBPF library built from the ground up purely in Rust without relying on libbpf or bcc, providing safe and idiomatic Rust wrappers to the BPF ABI, supporting the BPF Type Format (BTF), and requiring no C toolchain. Manually rewriting the existing libbpf C ecosystem in Aya Rust is impractical at scale, but large language model (LLM)-assisted translation is a promising direction. LLMs have shown strong general-purpose code-translation capability, and Aya’s typed surface gives the Rust type checker substantial leverage to reject ill-formed translations at compile time. However, automated translation of eBPF programs with perprogram equivalence raises several challenges. First, validating equivalence in eBPF is structurally hard. eBPF programs execute inside the kernel on opaque input structures such as packet buffers and tracepoint arguments, and the important observable outputs are side effects — map operations and data emitted to userspace — rather than return values which are usually constants. Even with the kernel’s BPF_PROG_TEST_RUN facility, comparing side effects across two program versions requires custom per-program harnesses, and subtle semantic divergences (endianness conversions, sign extension, map-access patterns) escape any finite test suite by construction. Furthermore, formally reasoning about these side effects is also non-trivial. Hash maps take dynamic, possibly symbolic keys, so a single write may alias any prior entry. Array maps utilize fixed integer-keyed accesses but still require modeling per-index updates across paths. Output sinks such as perf_event_array and ringbuf leave the kernel altogether, so equivalence has to compare the sequence of emissions rather than any in-kernel state. Second, unconstrained LLMs often resort to unsafe Rust and unidiomatic usage of Aya. Aya’s typed API is itself a partial defense — map-schema mismatches, and unchecked helper-returns become compile-time errors — but a residual class of unsafe patterns slips past the compiler and the kernel verifier alike. For example, Opus 4.6 faithfully reproduced mountsnoop’s uninitialized ring-buffer leak through untyped RingBufEntry<[u8; N]> and raw-pointer field writes. Catching this residual class requires an explicit safety policy that goes beyond what the Rust type system and Aya’s compiletime guards encode. Third, comparing two translations at their respective source levels would force reconciliation of Rust and C idiosyncrasies (ownership moves, integer promotion, panic semantics, trait resolution) that do not survive compilation. It is imperative to perform analysis on the eBPF bytecode for both the C and Rust programs, while faithfully modeling maps and helper functions. However, no existing symbolic-execution framework supported realistic eBPF programs at the bytecode level.
Dasu et. al
We present Heimdall, an automated pipeline that addresses these challenges end-to-end. Given a libbpf C program, Heimdall translates it to idiomatic safe Aya Rust via an LLM and iteratively fixes compilation and kernel-verifier errors. A safe-Aya static analysis engine rejects unsafe escape hatches (transmute, uninitialized output buffers, unsafe-extern helper trampolines) that LLMs often resort to and enforces safety properties the Rust compiler misses. We prove per-program equivalence to the original C program at the bytecode level, by comparing formulae produced by symbolic execution using angr [51] and Z3 [13]. To facilitate eBPF bytecode analysis, we built a complete eBPF backend for angr that faithfully models kernel helpers and symbolic maps. For last-writewins map updates under symbolic keys, we develop an ITE-chain encoding over per-path write sequences that captures both value and presence. Across 102 real-world eBPF programs, Heimdall produces 96 formally-verified-equivalent translations (94.1%). Of the remaining six, three are partially verified (a subset of entry points proven equivalent, with the rest exceeding symbolic execution time or memory limits) and three exceed solver scalability limits before reaching a verdict. Contributions. This paper makes the following contributions: • An automated C-to-Rust pipeline for eBPF. We present Heimdall, an automated translation approach for eBPF programs that combines LLM-based translation, compiler and kernel-verifier repair, safe-Aya static analysis, symbolic equivalence checking, and counterexample-guided repair in a single autonomous loop. • Conditional equivalence for safety- improving translation. Heimdall proves equivalence on executions that do not trigger declared C safety failures, while separate safety checks validate the repaired Rust behavior on excluded bugtriggering paths. • An eBPF symbolic-execution backend for angr. We model eBPF helpers, maps, relocations, atomic operations, and BPF-to-BPF calls, and introduce a custom if-then-elsechain encoding for comparing map side effects under symbolic keys. • A safe-Aya static analyzer. The analyzer rejects verifieraccepted Rust translations that bypass Aya’s typed surface, including unsafe helper, map, ring-buffer, and signed-errorhandling patterns. • New security findings in production eBPF tools. We report a bashreadline stack-residue leak that discloses kerneltext addresses sufficient to recover the KASLR slide, and 9 cross-event content leaks in ringbuffer programs. • A full-scale evaluation and public benchmark. We evaluate Heimdall on 102 eBPF programs. Heimdall generates 96 formally verified translations, substantially outperforms compile-only LLM baselines, and closes observed uninitialized-state, unchecked-helper, and signed/unsigned bug instances in the verified corpus. We release the benchmark, translations, scripts, and verification artifacts.
2
Motivation
Two kinds of problems in the eBPF verifier motivate Heimdall. First, there are safety gaps outside verifier scope: properties such
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Conference’17, July 2017, Washington, DC, USA
Table 1: Overview of six bug classes that cause safety and correctness issues due to the eBPF verifier gaps. Heimdall prevents these issues by translating to idiomatic Aya Rust.
into bpf_perf_event_output unchecked. The verifier treats this as acceptable since a root loader is considered part of the Trusted Computing Base (TCB). However, deployed BPF programs run continuously on attacker-influenced runtime inputs (syscall arguments, packets), so the load-time privilege check does not match the runtime trust boundary, which is the gap Heimdall closes at the source level. Heimdall prevents this because Rust requires that all struct fields be initialized before use (error[E0381], or error[E0063] for missing-field struct literals). We observed the same uninitialized-emit pattern in nine additional eBPF programs across libbpf-tools, libbpf-bootstrap, and the KEN tracing dataset: filelife.bpf.c, mountsnoop.bpf.c, opensnoop.bpf.c, oomkill.bpf.c, and tcpktlat.bpf.c from libbpf-tools [9]; bootstrap.bpf.c, profile.bpf.c, and sockfilter.bpf.c from libbpf-bootstrap [35]; and exitsnoop.bpf.c from KEN. Each reserves a ring-buffer slot and submits it with only a subset of fields written, so trailing bytes leak the previous record’s contents on every event. The cross-record ring-buffer residue leak in mountsnoop is described in Section 1. Public reports such as BCC issues #919 and #2623 confirm that verifier enforcement for stack initialization is incomplete and sensitive to code generation details [2, 4].
Bug Class
Tag
Heimdall Prevention
Listing
Uninitialized state Unchecked helper returns Buffer/Size mismatch Hook/context mismatch Map type/schema confusion Signed/unsigned confusion
Security Security Security Correctness Correctness Correctness
Compile-time Compile-time & API-level API-level Compile-time Compile-time Compile-time & API-level
Listing 1 Listing 1 Listing 2 Listing 5 Listing 6 Listing 7
as struct initialization discipline, output schema correctness, map key/value type consistency, or hook/context coherence that the verifier does not enforce. The verifier operates on compiled bytecode and reasons about byte ranges and pointer kinds, not the programmer’s intended source-level types, initialization discipline, or error-handling conventions. As a result, even a perfect, bugfree verifier would still not close these gaps, which motivates the case for moving such checks into the source language. Second, the verifier has bugs: CVEs arising from unsound pruning, missing helper-contract validation, and other logic errors [47, 54, 57]. We next present examples of those two categories of problems and discuss how Heimdall complements rather than replaces the eBPF verifier, thereby creating more robust eBPF systems that do not rely on the verifier as the sole arbitrator of safety.
2.1
Limitations of the eBPF Kernel Verifier
We present a non-exhaustive set of six classes of bugs that bypass the verifier. All the unsafe examples were run on kernel 6.8.0-106generic (Ubuntu) with clang 21.1.8 and bpftool v7.4.0. We confirm that the verifier accepts every program without error. Table 1 summarizes the bug classes discussed. Due to space constraints, we provide some of the listings in the appendix (Section A). Uninitialized state. Listing 1 shows bashreadline from libbpftools, which traces interactive bash command lines via a uretprobe on readline. The handler declares an 84-byte struct str_t on the stack with no zero-initialization, populates only the pid field plus the string prefix written by bpf_probe_read_user_str (which stops at the user string’s terminating \0), and emits the full struct via bpf_perf_event_output. On a stock workload of short typed commands, the trailing bytes per event are per-CPU BPF stack residue, and 100 % of perf-buffer events expose kernel-pointershaped values in those bytes. Across two independent 50-event runs, two distinct kernel-text return addresses (do_fault+0xf0 and mtree_load+0x271) recur identically. Cross-checked against /proc/kallsyms and /boot/System.map, both yield the same KASLR slide of 0x0e600000, recovering the kernel-text base. The verifier normally rejects helper reads of uninitialized stack bytes with an “invalid read from stack” error on any STACK_INVALID slot. However, for privileged programs like kprobes and uretprobes with CAP_PERFMON permissions, this check is silently bypassed via an internal allow_uninit_stack flag. Additionally, the destination of bpf_probe_read_user_str is additionally tagged MEM_UNINIT (helper-fills-buffer contract), suppressing any caller-side initialization check. Uninitialized bytes, therefore, flow
Unchecked helper returns. In Listing 1, the return value of bpf_probe_read_user_str is silently discarded. When the helper fails—e.g., if the process exits between the uretprobe trigger and the read—no bytes are written to data.str but the event is still emitted. Because the destination is uninitialized, helper failure means the entire 80 bytes of data.str are stale per-CPU stack residue rather than truncated string bytes. The verifier does not enforce that helper return values are checked before subsequent operations. Heimdall prevents this through two independent defenses. First, Rust’s definite initialization requirement (E0381) eliminates stale stack data even when the helper fails. Second, Aya helpers return a value of type Result<T, E>, which includes a normal case and an error case. Idiomatic Rust handles the error case explicitly — either by propagating with the ? operator or by branching on Ok/Err — rather than silently dropping it. Public issue reports show that these helper failures do arise in production. Tetragon issue #3728 reports unchecked probe_read failures in its argument-extraction path producing events with inaccurate argument values, and BCC issues #3175, #622, and #2245 report bpf_probe_read returning -EFAULT at runtime in production tracing programs [1, 3, 5, 6]. 1
struct str_t { __u32 pid; char str[80]; };
2
SEC("uretprobe/readline") int BPF_URETPROBE(printret, const void *ret) { 5 struct str_t data; /* BUG 1: not zero-initialized */ 6 if (!ret) return 0; 7 data.pid = bpf_get_current_pid_tgid() >> 32; 8 bpf_probe_read_user_str( &data.str, sizeof(data.str), ret); /* BUG 2: return ignored */ 9 bpf_perf_event_output(ctx, &events, 10 BPF_F_CURRENT_CPU, &data, sizeof(data)); /* emits 84 B */ 11 return 0; 3 4
Conference’17, July 2017, Washington, DC, USA
12
}
Listing 1: bashreadline.bpf.c (libbpf-tools) exhibits two safety bug classes simultaneously: an uninitialized stackresident struct (BUG 1) and a discarded helper return value (BUG 2). Buffer/Size mismatch. Listing 2 shows a kprobe that builds a full_event containing a small public header and adjacent private fields (a task_struct pointer and a kernel instruction pointer). The private fields are explicitly populated with bpf_get_current_task() and PT_REGS_IP_CORE(ctx), so they hold real kernel addresses rather than stale stack bytes. The developer intends to emit only the header but passes sizeof(evt) instead of sizeof(evt.pub), so the helper copies the entire enclosing object and leaks a kernel code pointer on every event, sufficient to recover the KASLR offset in our tests. The same root cause, a caller-supplied size argument decoupled from the logical extent of a typed buffer, arises on the input side. In a PoC, bpf_probe_read_user_str is called with a size that covers both filename[16] and an adjacent verdict field, so attacker-supplied paths longer than 16 characters overwrite verdict, flipping 5 of 60 policy decisions from deny to allow. In every variant the verifier validates the buffer as a raw byte range paired with a constant-size argument, with no notion of which fields lie within that range. Safe Aya wrappers prevent every case because output APIs such as PerfEventArray<T>::output derive the byte count from the type parameter T, and input helpers derive the writable length from the destination buffer type. There is no separate caller-controlled size that can accidentally be larger than the buffer type. struct public_event { __u32 pid, reserved; __u64 timestamp; }; 2 struct full_event { 3 struct public_event pub; 4 __u64 task_ptr, ip_ptr; /* private addresses */ 5 }; 1
6
SEC("kprobe/do_sys_openat2") int output_size_leak(struct pt_regs *ctx) { 9 struct full_event evt = {}; 10 ... /* init evt.pub.*, evt.task_ptr, evt.ip_ptr */ 11 bpf_perf_event_output(ctx, &events, 12 BPF_F_CURRENT_CPU, &evt.pub, sizeof(evt)); /* BUG: sizeof(evt) instead of sizeof(evt.pub) */ 13 return 0; 14 } 7 8
Listing 2: Wrong output size: the developer intends to emit only the public header, but sizeof(evt) copies adjacent private fields including kernel pointers. Hook/context mismatch. Listing 5 shows a program declared as an XDP hook (SEC("xdp")) whose function signature uses struct __sk_buff, the TC context type. The source reads skb->protocol (byte offset 16), but under XDP, offset 16 maps to xdp_md->rx_queue_index. A network monitoring tool deploying this program would receive queue indices labeled as protocol numbers, silently corrupting downstream packet classification
Dasu et. al
or security filtering decisions. The verifier accepts this because it checks byte offset validity against the program type, not the C-level struct name. Heimdall prevents this because Aya’s typed #[xdp] macro generates code expecting XdpContext. Passing SkBuffContext produces error[E0308]: mismatched types. A related variant appears in the BMC in-kernel cache [22], where error paths in the TC-attached tx_filter and update_cache programs return XDP_PASS (value 2) instead of TC_ACT_OK (value 0); in the TC action namespace, value 2 is TC_ACT_SHOT, so these paths silently drop packets instead of passing them. Map type/schema confusion. This bug class has two variants. The first writes a struct larger than a map’s declared value size. The second reinterprets a map lookup result as an unrelated struct type. Listing 6 shows both in one program. The array map declares struct conn (8 bytes) as its value type. The program then updates the map with a pointer to the larger struct big (16 bytes), and the kernel copies only value_size (8) bytes, silently discarding the rest. A bpf_map_lookup_elem result is then cast to the unrelated struct stats, so two 32-bit IP addresses are reinterpreted as a single 64-bit byte counter. The verifier permits both because bpf_map_update_elem takes an untyped void* and bpf_map_lookup_elem returns void*, since validation is by byte width, not C type. Heimdall prevents all three variants because Aya maps are generic: Array<A>::set requires impl Borrow<A>, HashMap<K,V>::get returns Option<&V>, and passing the wrong key or value type produces error[E0277] or error[E0308]. Signed/unsigned confusion. Listing 7 shows the Linux kernel’s offwaketime sample, which stores the return value of bpf_get_stackid in u32 struct fields. This helper returns a signed long and negative values such as -EEXIST (−17) or -ENOMEM (−12) indicate failure. Stored in a u32, these become large positive values (e.g., 232 − 17 = 4,294,967,279) that are subsequently used as map keys, silently creating spurious entries in the counts hash map. The verifier does not track the signedness of helper return values or detect implicit signed-to-unsigned conversions. Heimdall addresses this because Aya’s StackTrace::get_stackid returns Result<i64, i64>: the error sits in a typed Err variant rather than a sentinel integer encoded in the success channel, giving the translation a typed handle on the failure path (error[E0308]).
2.2
Vulnerabilities of the eBPF Kernel Verifier
Beyond design-level gaps, the verifier itself has been a recurring source of exploitable vulnerabilities. Huang et al. [27] classify recent CVEs into unsound state pruning, incomplete helpercontract validation, and helper-side trust failures. Heimdall does not eliminate these kernel-side bugs since it compiles to the same bytecode and passes through the same verifier pipeline. However, typed and ownership-oriented APIs can remove some concrete exploit-enabling source patterns from legacy libbpf code, narrowing the attack surface. For example, CVE-2021-4204 exploits a missing bounds check in the ring-buffer helper. The attacker calls bpf_ringbuf_submit(sample + 128, 0), passing a shifted pointer past the reserved region, to corrupt adjacent kernel memory. Similarly, CVE-2023-2163 exploits incorrect branch pruning in the verifier’s state-comparison logic to enable
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
C libbpf (.c)
Stage 1
LLM Translation
Rust Aya (.rs)
Stage 2
Compile → Kernel Verify
Stage 3
Safety Check
LLM + error/safety feedback
pass?
fail
pass
Rust eBPF Binary (.o)
C eBPF Binary (.o)
Stage 4
Symbolic Execution (angr)
Stage 5
Z3 Equivalence Check
result?
SAT
LLM + counter-example
UNSAT
✓ VERIFIED
Figure 1: Heimdall’s five-stage pipeline with retry loops. Orange boxes are LLM-driven steps and blue boxes are deterministic tool steps.
arbitrary kernel memory access using the ring-buffer helper. Heimdall prevents certain exploit patterns with safe and idiomatic Aya Rust. For example, Aya represents a reserved ring-buffer slot as an owned RingBufEntry<T> whose submit(self, flags) and discard(self, flags) methods consume the entry and internally use the original reserved pointer, thereby preventing safe Aya code from submitting or discarding an attacker-shifted pointer.
3
Methodology
We present Heimdall, an automated pipeline that translates C eBPF programs to Rust and formally verifies semantic equivalence.
3.1
Heimdall Translation Pipeline
Figure 1 presents the five stages of Heimdall. Heimdall can be instantiated in two ways: a deterministic approach that explicitly follows each stage sequentially via a scripted pipeline, and an agentic approach where an LLM agent implicitly follows the same stages via tool-mediated reasoning. More details about the two approaches are provided in Section 4.2. Stage 1: LLM Translation. The pipeline takes as input a C eBPF source file, the entry point symbol name, and a list of map names with their types. An LLM translates the C source to Rust using a
Conference’17, July 2017, Washington, DC, USA
prompt that includes Aya API mappings, hook macro tables, map access patterns, and a complete working example. Stage 2: Compile and Kernel Verify. The Rust source is compiled to eBPF bytecode with a set of compiler-supported lint guards. These guards deny multiple unsafe operations within one block, undocumented unsafe blocks, unnecessary unsafe, and unused must_use results. For example, #![deny(unused_unsafe)] is added at the top of the produced Rust code to deny unnecessary uses of unsafe blocks. These guards force the translation toward small, scoped unsafe regions and prevent silently ignored API outcomes. Compiler errors are fed back to the LLM in an inner retry loop. On successful compilation, the binary is loaded into the kernel verifier, which ensures the translated program satisfies eBPF safety requirements (bounded loops, memory safety, restricted helpers). Stage 2 rejects translations that are not accepted by the Rust toolchain or by the eBPF verifier. This stage handles the part of the LLM-unsafety challenge (Section 1) that Aya’s typed API and the kernel verifier already encode (e.g., hook/context mismatches and map-schema mismatches surface as error[E0308] or verifier rejections). Stage 3: Safety Check via Static Analysis. This stage determines whether the translation used the safest available Aya abstraction and idiomatic Rust. While the Rust compiler with lint guards helps isolate unsafe code and prevent unsafe blocks with overly broad scope, it cannot automatically derive safe or idiomatic alternatives needed to replace the remaining unsafe blocks. Identifying such gratuitous unsafe usage is challenging since unsafe code is inherent to Aya eBPF programs, such as HashMap::get() and bpf_probe_read_kernel(). On the other hand, safe interfaces also exist, such as HashMap::insert()/remove(), and helper wrappers like bpf_get_current_comm(). We therefore create a source-level safety engine that strips comments and applies bannedpattern checks, regex bans, and file-level invariants on the Rust source. The two empirically dominant bug classes from Section 2.1 drive the strictest rules. For uninitialized state, the engine bans untyped ringbuf reservations (RingBuf::reserve::<[u8; N]>, RingBufEntry<[u8; N]>) that would force raw-pointer field arithmetic and instead requires a pre-population zero-fill on typed reservations. Additionally, Rust’s error[E0063] catches any missing field at struct-literal construction. For unchecked helper returns, the engine rejects let _ = . . . and .ok() discards on failable Aya helper returns, forcing ?-propagation or explicit Ok/Err matching. The full set of safety policies is listed in the appendix (Section D). This stage closes the residual portion of the LLM-unsafety challenge (Section 1) by preventing unsafe and unidiomatic Aya patterns that compile and pass the kernel verifier but circumvent our safety policy. Stage 4: Symbolic Execution. Both the original C eBPF binary and the compiled Rust binary are loaded into angr using the symbolic execution backend described in Section 3.2. Our symbolic execution explores all paths, producing structured formulae that capture return values and map side effects of the two input programs. Operating on eBPF bytecode rather than on Rust or C source addresses the source-level-mismatch challenge (Section 1), since ownership moves, integer promotion, and trait resolution do not survive compilation.
Conference’17, July 2017, Washington, DC, USA
Stage 5: Equivalence Checking. The equivalence checker (Section 3.3) submits the generated formulae to Z3 to determine whether the C eBPF and Rust programs are equivalent for all inputs. If they are equivalent, the translation is verified. If it finds a counterexample, the example is formatted with divergence classification and fed back to the LLM for targeted repair. The repaired Rust source re-enters the pipeline at Stage 2, after which Stages 3–5 are re-run on the rebuilt binary. This stage addresses the structurally-hard eBPF equivalence challenge (Section 1) by checking equivalence of side effects (map state, output sinks) and return values jointly, rather than relying on test-input harnesses.
Dasu et. al
Core angr Framework
CLE Loader
Archinfo DB
VEX Engine
SimOS Dispatch
Simulation Manager
1
2
3
4
5
eBPF ELF Backend
eBPF Architecture
Instruction Lifter
eBPF Helper SimProcs
Formula Generator
relocations + contexts
11 registers + call stack
82 instruction classes
56 helper models
maps + path outcomes
Our eBPF Backend Extension Extension hook
3.2
angr lifecycle
Symbolic Execution
One stage of Heimdall performs symbolic execution on eBPF bytecode. No existing symbolic execution framework supported realistic eBPF programs at the bytecode level1 , so we built a full eBPF backend for angr [51]. Figure 2 shows how our eBPF support extends angr across five layers of its execution stack: (1) CLE delegates object loading to an eBPF ELF backend, (2) archinfo resolves bpf binaries to our eBPF architecture definition, (3) the VEX engine delegates instruction lifting to an eBPF lifter, (4) SimOS dispatch invokes eBPF helper and runtime models, and (5) the simulation manager hands terminated states to a formula generator. We provide a concrete end-to-end example of symbolic execution of eBPF bytecode in the Appendix (Figure 5). eBPF ELF backend. We extend angr’s loader with an eBPF ELF backend that resolves the eBPF-specific relocations needed to make a compiled program symbolically executable: map references become handles consumed by the runtime model, BPF-to-BPF call targets become reachable addresses, and remaining external references (read-only constants, mutable globals, kernel functions) are bound to memory regions or stubs. The loader auto-detects the program type (kprobe, tracepoint, XDP, etc.) from ELF section names, and the symbolic program context is sized appropriately for each program type. Architecture definition. We register a 64-bit eBPF architecture with angr so every downstream component treats the binary as native eBPF. The architecture declares the eBPF general-purpose registers along with the auxiliary state the lifter needs to track instruction flow and BPF-to-BPF call depth. Instruction lifter. We implement a VEX IR lifter that decodes the eBPF instruction format and lifts it into VEX IR for angr’s symbolic engine. The lifter covers the eBPF instruction set in both 32-bit and 64-bit variants: arithmetic and bitwise ALU operations, conditional and unconditional control flow (including helper and BPF-to-BPF calls), load/store at all standard widths, and atomic memory operations. eBPF helper stubs. We extend angr’s SimOS dispatch with an environment that initializes the symbolic execution state according to the eBPF calling convention and registers a model for every BPF helper a program may call. Helpers that read kernel state return symbolic bitvectors under a stable naming convention shared 1 The existing angr-platforms eBPF backend supports bare-bones ALU/jump/load-
store lifting with 2 helper stubs, with no map modeling, no atomic instructions, no BPF-to-BPF call support, and no relocation handling.
Figure 2: Our eBPF support in angr. Five numbered hooks pair each angr component (top) with its eBPF extension (bottom). Horizontal arrows show the angr lifecycle from bytecode to formula generation.
between the C and Rust binaries, so the equivalence checker (Section 3.3) can unify reads across the two programs and ensure both are evaluated under identical kernel state. Formula generator. We extend angr’s simulation manager with a formula generator that drives a fully symbolic initial state, explores all feasible paths, and emits, for each terminated path, the structured outputs the equivalence checker consumes: a path predicate, the return value in R0, and the final state of each map. Mutable ELF globals are tracked alongside maps and included in the same perpath summary, so any divergence between the C and Rust binaries in either map state or globals surfaces during equivalence checking.
3.3
Equivalence Checking
The equivalence checking stage in Heimdall asserts if the Rust translation is formally equivalent to the C program. In case of mismatches, it guides the LLM in repairing the translation using concrete counterexamples. Definition 3.1 (eBPF Program). An eBPF program P is a function P : C × M −→ R × M ′
(1)
where C is the symbolic program context (dependent on program type: xdp_md, pt_regs, sk_buff, etc.), M = {𝑚 1, . . . , 𝑚𝑘 } is the initial map state, R ∈ B64 is the return value (register R0), and M ′ is the final map state. Definition 3.2 (Symbolic Execution Paths). Symbolic execution of program P yields a set of paths Π = {𝜋1, . . . , 𝜋𝑛 } where each path 𝜋𝑖 = (𝜙𝑖 , 𝑟𝑖 , M𝑖′ ) consists of: • 𝜙𝑖 : the path predicate, a conjunction of branch conditions constraining the symbolic inputs • 𝑟𝑖 ∈ B64 : the symbolic return value along this path, which is the content of register R0 • M𝑖′ : the map state at the end of this path, represented as a sequence of map entry snapshots per map where the path predicates are mutually exclusive and collectively Ô exhaustive i.e., 𝑖 𝜙𝑖 = true and 𝜙𝑖 ∧ 𝜙 𝑗 = false for 𝑖 ≠ 𝑗.
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Definition 3.3 (Program Output). The output of program P on input 𝑥® ∈ C × M is encoded as a predicate out P (𝑥) ® over the return value R, built in three layers: (1) Per-path Binding. Along each path 𝜋𝑖 , the expression R = 𝑟𝑖 asserts that the program’s return value matches the symbolic register R0 value generated along 𝜋𝑖 . (2) Path Guard. The binding is conjoined with the path predicate, 𝜙𝑖 (𝑥) ® ∧ R = 𝑟𝑖 , so that the equality R = 𝑟𝑖 is valid only on inputs that traverse 𝜋𝑖 . (3) Path Enumeration. Disjunction of the guarded bindings yields the full output predicate and covers the entire input space: out P (𝑥) ® ≜
𝑛 Ü
𝜙𝑖 (𝑥) ® ∧ R = 𝑟𝑖 .
(2)
𝑖=1
Definition 3.4 (Map Output). map𝑚 ® 𝑘𝑞 ) ≜ 𝑃𝑚 (𝑘𝑞 ), 𝑉𝑚 (𝑘𝑞 ) P (𝑥, denotes the final (presence, value) pair of map 𝑚 at query key 𝑘𝑞 ∈ K after executing program P on input 𝑥, ® where each component is encoded as an If-Then-Else (ITE) chain. Given a query key 𝑘𝑞 , the map𝑚 P tuple answers the following questions: “would the lookup succeed?” (𝑃𝑚 ) and “if the lookup succeeds, what value would I read back?” (𝑉𝑚 ). Both are encoded as ITE chains that walk the program’s writes in newest-first order, mirroring the kernel’s last-write-wins semantics. ITE-chain map encoding. A natural approach to represent maps is to use Z3’s Theory of Arrays directly. However, angr’s constraint backend (Claripy) represents all symbolic values as fixed-width bitvectors that cannot be directly combined with Z3 Arrays2 . Instead, we post-process the symbolic execution output into ITE (if-then-else) chains over bitvectors. The encoding is two-level: an inner chain captures the ordered write trace on a single path, and an outer chain selects the trace whose path predicate 𝜙 𝑗 is satisfied. On a single path 𝜋 𝑗 , the entries ⟨𝑘 1, 𝑣 1, 𝑒 1 ⟩, . . . , ⟨𝑘𝑛 , 𝑣𝑛 , 𝑒𝑛 ⟩ are sorted by temporal write sequence (𝑒𝑖 is 1 after update_elem, 0 after delete_elem). The per-path value chain walks the trace newest-first and returns the first write whose key matches and whose post-state still exists, falling through to the shared initial map 𝑣 init : 𝜋 𝑉𝑚 𝑗 (𝑘𝑞 ) ≜ Ite 𝑘𝑞 = 𝑘𝑛 ∧ 𝑒𝑛 = 1, 𝑣𝑛 , Ite 𝑘𝑞 = 𝑘𝑛−1 ∧ 𝑒𝑛−1 = 1, 𝑣𝑛−1, . . . , 𝑣 init . 𝜋
(3)
The presence chain 𝑃𝑚𝑗 (𝑘𝑞 ) has the same structure but branches on 𝑘𝑞 = 𝑘𝑖 alone (without conjoining 𝑒𝑖 = 1) and returns 𝑒𝑖 directly, so a delete clears presence at 𝑘𝑖 while still letting the value chain fall through to the prior write at the same key. This encoding yields last-write-wins under symbolic key aliasing and is equivalent to the read-over-write axioms of the Theory of Arrays [38]. Across all paths, we create per-program ITE chains for value (𝑉𝑚 (𝑘𝑞 )) and presence (𝑃𝑚 (𝑘𝑞 )) that are ITE chains over individual path chains combined with the respective path predicates: 2 https://github.com/angr/claripy/issues/171
Conference’17, July 2017, Washington, DC, USA
𝑉𝑚 (𝑘𝑞 ) ≜ Ite 𝜙𝑛 (𝑥), ® 𝑉𝑚𝜋𝑛 (𝑘𝑞 ), Ite 𝜙𝑛−1 (𝑥), ® 𝑉𝑚𝜋𝑛−1 (𝑘𝑞 ), . . . , 𝑉𝑖𝑛𝑖𝑡 .
(4)
where 𝑉𝑖𝑛𝑖𝑡 is the shared initial value for the program. We provide a concrete example of the ITE chain construction in the appendix (Section C). Several eBPF programs mutate map values through pointers returned by bpf_map_lookup_elem rather than via bpf_map_update_elem (e.g. __sync_fetch_and_add on a hashmap slot). To account for such pointer updates, we model map values as memory-backed regions in angr. All pointer-level updates are recorded in the same write sequence as helper-mediated updates and flow through the same ITE chain. The bug classes from Section 2.1 (unchecked helper returns, uninitialized state, etc.) are precisely the source-level patterns we do not wish to translate faithfully into Rust. By construction, our pipeline produces Rust translations that close such patterns: a Rust translation that handles the error return value of a helper call, or that zero-fills a ringbuf slot before population, behaves differently from the buggy C source on the inputs that trigger the underlying bug. Strict equivalence checking between C and Rust would therefore reject the safer translation precisely on the inputs where we want it to behave better. We resolve this tension by adopting conditional equivalence: we require the Rust and C programs to agree only on inputs that satisfy a declared set of safety conditions. Definition 3.5 (Conditional Semantic Equivalence). Let Φsafe : C × M → {true, false} be a safety condition on inputs. Programs P𝐶 (C original) and P𝑅 (Rust translation) are equivalent modulo Φsafe iff for all inputs 𝑥® ∈ C × M and all query keys 𝑘𝑞 ∈ K: Φsafe (𝑥) ® =⇒ out P𝐶 (𝑥) ® = out P𝑅 (𝑥) ® ∧ ∀𝑚 ∈ M : map𝑚 ® 𝑘𝑞 ) = map𝑚 ® 𝑘𝑞 ). P𝐶 (𝑥, P𝑅 (𝑥,
(5)
In our pipeline, Φsafe is the conjunction of two concrete safety conditions, each of which is a deliberate scoping choice that lets safety-improving Rust translations (error-aware helper handling, zero-filled ringbuf slots) coexist with bytecode-level equivalence to legacy C source that does not perform those safety checks: (i) Helper(𝑖 ) success (Φsafe ). Equivalence is required only on inputs that drive every helper call to success. On the success paths, the typed Err arm is unreachable during symbolic execution, so a Rust translation that short-circuits on Err (e.g., Err(_) => return) produces the same state as a C source that ignores the helper-failure return on every (𝑖 ) input that Φsafe admits. To analyze failure paths, our equivalence checker provides a helper failure mode where helpers can fail. (𝑖𝑖 ) (ii) Output-sink Opacity (Φsafe ). Equivalence does not require per-event bytes emitted to perf events or ringbuf output sinks to match between C and Rust. A Rust translation that safely zero-fills uninitialized memory (closing the mountsnoop-style cross-record leak) does not diverge from a C source that emits stale data, since the (𝑖𝑖 ) divergent bytes are exactly the ones Φsafe leaves out of comparison. To analyze sink content, our equivalence checker provides a stricter sink-tracking mode that also tracks bytes emitted from events.
Conference’17, July 2017, Washington, DC, USA
Verification of equivalence reduces to checking unsatisfiability. We negate Equation (5) and ask Z3 whether there exists an input 𝑥® and a query key 𝑘𝑞 such that: out P𝐶 (𝑥) ® ≠ out P𝑅 (𝑥) ® ∨ ∃𝑚 ∈ M : map𝑚 ® 𝑘𝑞 ) ≠ map𝑚 ® 𝑘𝑞 ). P𝐶 (𝑥, P𝑅 (𝑥, (6) If the formula is UNSAT, the programs are equivalent. If SAT, the satisfying assignment is a concrete counter-example. Unless otherwise specified, “equivalent” and “verified” refer to conditional equivalence in Definition 3.5. Variable unification. Our equivalence checker renames symbolic variables into a unified namespace with two categories: shared variables (kernel state such as input_pid_tgid and input_ktime, initial map contents, and key-existence conditions) are mapped to the same Z3 variable for both programs and distinct variables (return values, final map state) are given per-program suffixes (e.g., output_r0_c vs. output_r0_rust). This ensures both programs are evaluated under identical kernel state while allowing their outputs to possibly diverge. Map type support. Our engine supports 20 eBPF map types across four categories. Hash-like maps (8 types: hash, lru_hash, percpu_hash, lru_percpu_hash, stack_trace, devmap_hash, lpm_trie, sockhash) take symbolic keys, so each lookup must reason about aliasing against every prior entry. Array-like maps (8 types: array, percpu_array, cgroup_array, xskmap, devmap, cpumap, sockmap, prog_array) are the integer-keyed special case, so a lookup is just a bounds check against the array length. Output sinks (2 types: perf_event_array, ringbuf) record the sequence of emitted events for equivalence comparison even though the data leaves the kernel. Map-of-maps (2 types: array_of_maps, hash_of_maps) resolve outer lookups to a canonical inner map, which subsequent helper calls then index using the inner key. Counterexample feedback. When Z3 returns SAT, the satisfying assignment provides concrete values for all shared input variables (program context, initial map contents, helper return values). The checker evaluates both programs’ outputs under these concrete inputs, classifies the divergence type (e.g., sign extension, truncation, missing write, extra write), and formats a structured counterexample with both programs’ outputs at each diverging point. The counterexample is fed back to the LLM for targeted repair, forming a loop analogous to counter-example-guided inductive synthesis (CEGIS) [8, 52]. The LLM acts as the synthesizer proposing candidate translations, and Z3 acts as the verifier producing counter-examples that guide the next candidate [7, 31]. Supplementary checks. Beyond the core Z3 equivalence checking, we enforce several additional structural invariants. During Atomic operation equivalence, symbolic execution treats atomic and non-atomic memory operations identically on a single path, so a translation that drops atomicity guarantees would appear equivalent under Z3. To detect this, we augment the checker with a static bytecode scan that counts atomic opcodes in each binary’s entry symbol section. If the C program uses atomic operations but the Rust translation does not (or uses fewer), the UNSAT result is overridden and reported as a mismatch with concrete feedback on the missing atomic operations and their Aya equivalents. The checker
Dasu et. al
also pairs mutable globals across the two binaries (matching by name where possible, by size otherwise) and includes their final values in the equivalence query alongside map state and return values. Finally, to ensure entry-point type compatibility, the checker extracts the BPF program type from each entry point’s ELF section name and rejects pairs with incompatible types before symbolic execution begins, preventing false equivalence results from comparing programs with different context layouts.
4 Evaluation 4.1 Experimental Setup Hardware. All experiments were conducted on an x86_64 server equipped with 24 physical cores and 335 GB of RAM. The system runs Ubuntu 22.04.3 LTS with Linux Kernel 6.8.0. The environment is hosted on a KVM-based virtual machine with hardware acceleration. Software. We use Python 3.12, angr 9.2 for symbolic execution, Z3 4.13 as the SMT solver, and the Aya3 eBPF framework with rustc 1.93.1. The C libbpf programs were compiled with clang 14.0.0, bpftool v7.4.0, and libbpf v1.4. In our experiments with commandline agents, we use claude code 2.1.112, codex 0.116.0, and gemini-cli 0.36.0. The C libbpf programs were compiled at the -O2 optimization level. The Rust programs were compiled with the –release flag.
4.2
Translation Approaches
We experiment with the following fully autonomous translation approaches: (1) Baseline. For the baseline approach, we consider code agents with state-of-the-art LLMs inside a coding harness e.g., Claude Code. The agent is given instructions to translate the C libbpf to Rust Aya, along with the source .c file. The agent is completely unrestricted and runs with full-tool reasoning, i.e., file browsing, creating bash/.py scripts, etc. The agent iterates until it produces a compilable Rust Aya program that it believes is equivalent to the C program. Our baseline setup mimics the setup of software engineering benchmarks [33, 39, 40], and our experiments serve as a benchmark of agentic capability in producing equivalent eBPF translations from C to Rust. (2) Heimdall (Deterministic). In this setting, we instantiate Heimdall (Figure 1) in a scripted pipeline that explicitly follows the 5-stage approach. The LLM is invoked as a stateless translator: on the first attempt it receives the C source and is asked to produce a Rust Aya translation; on subsequent attempts it additionally receives the previous rust code along with structured feedback from the failing stage (compiler errors, kernel verifier diagnostics, safety-policy violations, or Z3 counter-examples). No tool-mediated reasoning is permitted. Transitions between stages are driven by an automaton-style controller in our pipeline rather than by the model itself, so the LLM never decides what to do next. It only produces the next candidate translation given the current stage’s feedback. 3 Upstream was at commit: a7144b9a6efc963e1fdcc0716990846a9d407ae1
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Conference’17, July 2017, Washington, DC, USA
Table 2: Dataset of eBPF programs. “Total” is the number of programs in each source; “Valid” is the subset supported by the Rust/Aya target.
instantiate the pipeline with opus-4.6 and sonnet-4.64 . Lastly, we instantiate Heimdall (Agentic) with the same agents as the baseline. We evaluate these settings against 44 libbpf-tools programs and 7 randomly picked programs (DAE, Fluvia, Hercules, CRAB, and XDP-FW). This gives us 510 translations across all settings. Of these, the ksnoop program from libbpf-tools is the only translation that cannot be verified since it exceeds symbolic execution limits. We consider this a de facto failure since it is a limitation of our verification framework. Table 3 highlights the results for the 510 translations in our benchmark study. Compile, Kernel Verified (KV), Safety, Equivalent (Equiv.), and the KV ∩ Safety ∩ Equiv. triple-pass columns report counts and percentages over the 51-program comparison set, while Time, Bytecode (BC) Overhead, Unsafe Ops, Tokens In/Out, and Cost are per-program averages. We measure Bytecode (BC) Overhead as the ratio of Rust to C verifier-loaded .text/prog_* bytecode sections and exclude debug and symbol sections. Unsafe Ops is the per-program count of unsafe operations (raw pointer dereferences, function/method calls inside an unsafe context, inline-assembly invocations, and mutable-static reads), counted via tree-sitter-rust on the produced Rust source. The first trend is that compilation is not a meaningful proxy for translation success. Every setting produces 51/51 compiled Rust artifacts, but the baseline agents only fully verify 2–6/51 (4–12%) translations. Heimdall’s staged repair loop closes most of this gap on the same underlying models. Heimdall (Deterministic) reaches 24–32/51 (47–63%) triple-pass translations, and Heimdall (Agentic) reaches 37–50/51 (73–98%) — a ∼90 percentage-point absolute improvement over the strongest baseline. Additionally, kernel verification is a poor signal of equivalence. Baseline KV pass rates of 71–96% drop to 4–12% triple-pass once safety policy and symbolic equivalence are layered in, confirming that the three downstream checks catch disjoint failure classes (471/510 pass KV, 373/510 pass safety, 273/510 pass equivalence, but only 248/510 pass all three). Since every setting compiles all 51 programs, none of the 262 translations that fail at least one downstream check fail for syntactic reasons; i.e., they fail in eBPF-specific semantics or safety policy. Of these 262, 114 (43.5%) are safety violations, 109 (41.6%) are equivalence failures, and 39 (14.9%) are KV rejections. We charge each failing translation to its earliest failing stage in the order KV → safety → equivalence, so these three sub-counts are disjoint and sum to 262. Table 3’s per-stage columns count failures independently and therefore overlap (e.g., a program that fails both KV and safety is counted in both columns but charged only to KV in the 39/114/109 split). Within safety violations, 80.7% of failing translations declare read-only configuration globals (e.g., target_pid, targ_tgid) as static mut and read them via read_volatile — Aya emits static mut as a writable BPF map rather than read-only .rodata, exposing what the C source intends as immutable configuration to userspace writes. Within equivalence failures, the top two categories are both map-related and account for 77.1% of the total: 43.1% are wrong map values for the same key (the LLM emits an incorrect update or skips one), and 33.9% are state-representation mismatches between .data globals and BPF-map slots (e.g., the C
Source
Total
Valid
Entries
Avg LoC
Avg Maps
libbpf-tools [9] libbpf-bootstrap [9] KEN samples [62] DAE [12] Fluvia [45] Hercules [43] Suricata [46] CRAB [34] XDP-FW [53] BMC [22] cache_ext [65]
57 15 26 1 1 1 6 1 3 1 7
44 13 25 1 1 1 5 1 3 1 7
322 21 38 6 1 1 5 1 3 7 42
175 45 40 206 162 193 216 370 111 526 325
2.2 0.5 1.0 2.0 1.0 3.0 2.6 4.0 1.3 6.0 3.0
Total
119
102
447
—
—
(3) Heimdall (Agentic). In this setting, we instantiate Heimdall (Figure 1) as an agentic harness layered on top of the same code agents used in the baseline, so the 5-stage approach is followed implicitly rather than enforced by an external controller. The agent retains full freedom to perform tool-mediated reasoning—reading files, inspecting C and Rust bytecode, browsing the Aya source tree, spawning subagents, and writing helper scripts—while being directed to follow the stages of our approach to produce an equivalent and idiomatic Rust Aya translation. At each stage, the agent has access to the same structured signals as the deterministic pipeline (compiler output, kernel verifier diagnostics, safety analyzer reports, and equivalence-checker counterexamples), but it can also act on them with arbitrary tool calls.
4.3
Dataset
Table 2 summarizes our evaluation dataset, which is diverse in both source and eBPF subsystem coverage. It includes production tracing tools, tutorial programs, benchmark samples, network functions, research systems, and network-IDS filters, spanning kprobes, tracepoints, fentry/fexit, uprobes, LSM, XDP, TC, and socket-filter programs. Of the 119 collected programs, 17 are excluded because Aya does not support BPF_MAP_TYPE_CGROUP_ARRAY, USDT arguments, and legacy BPF_LD_ABS/BPF_LD_IND socket-filter instructions. Thirteen libbpf-tools programs use cgroup_array maps, two libbpf-bootstrap programs require an iterator or USDT-argument support, one KEN sample uses bpf_usdt_arg, and one Suricata program depends on legacy socket-filter instructions. This leaves 102 valid programs for translation and verification. The data sources are of varying complexity, measured using average LoC and number of eBPF maps (shown in the last two columns of Table 2).
4.4
Benchmarks
To benchmark the three translation approaches, we create 10 experimental settings. For the baseline, we use Claude Code (sonnet-4.6 and opus-4.6), Codex (gpt-5.4), and Gemini-CLI (gemini-3-flash-preview). For Heimdall (Deterministic), we
4We only use two LLMs here due to resource constraints and limited API credits.
Conference’17, July 2017, Washington, DC, USA
Dasu et. al
Table 3: Evaluation results of the three translation approaches across 10 experiment settings and 51 eBPF programs. Heimdall (Agentic) with opus-4.6 is the most successful with 98% formally verified and equivalent translations. KV ∩ Safety ∩ Equiv. Time (min) Bytecode Overhead
Translation Approach
Model
Compile
Kernel Verified (KV)
Safety
Equivalent
Unsafe Ops
Tokens In/Out
Cost
Baseline
sonnet-4.6 opus-4.6 gpt-5.4 gemini-3-flash-preview
51/51 (100%) 51/51 (100%) 51/51 (100%) 51/51 (100%)
39/51 (76%) 49/51 (96%) 47/51 (92%) 36/51 (71%)
24/51 (47%) 22/51 (43%) 27/51 (53%) 21/51 (41%)
10/51 (20%) 11/51 (22%) 6/51 (12%) 8/51 (16%)
5/51 (10%) 6/51 (12%) 4/51 (8%) 2/51 (4%)
6.7 4.6 3.6 2.7
2.62× 2.41× 2.46× 2.33×
18.0 19.7 6.3 26.4
594K / 24K 800K / 16K 861K / 9K 597K / 11K
$0.78 $1.23 $0.48 $0.13
Heimdall (Deterministic)
sonnet-4.6 opus-4.6
51/51 (100%) 51/51 (100%)
49/51 (96%) 47/51 (92%)
43/51 (84%) 43/51 (84%)
24/51 (47%) 34/51 (67%)
24/51 (47%) 32/51 (63%)
16.5 18.7
2.62× 2.12×
30.3 29.5
164K / 66K 286K / 79K
$1.42 $3.26
Heimdall (Agentic)
sonnet-4.6 opus-4.6 gpt-5.4 gemini-3-flash-preview
51/51 (100%) 51/51 (100%) 51/51 (100%) 51/51 (100%)
51/51 (100%) 51/51 (100%) 51/51 (100%) 51/51 (100%)
51/51 (100%) 51/51 (100%) 47/51 (92%) 44/51 (86%)
48/51 (94%) 50/51 (98%) 37/51 (73%) 45/51 (88%)
48/51 (94%) 50/51 (98%) 37/51 (73%) 40/51 (78%)
25.7 23.3 7.9 11.1
2.82× 2.63× 2.62× 2.68×
19.8 18.1 9.2 26.7
2721K / 77K 2646K / 65K 2882K / 16K 3782K / 25K
$2.58 $4.05 $1.21 $0.62
version uses a global and the translation uses a map, or vice-versa). Of the KV failures, 26/39 (≈ 67%) are a heterogeneous mix of helpercall and pointer-tracking errors. The remaining KV failures are split across pointer-bounds violations, unreleased reference-counted resources, invalid memory accesses, and out-of-range branches. Heimdall (Agentic) excels at the expense of higher running time and tokens consumption. Opus-4.6 agentic averages 23.3 min and $4.05 per program vs. 18.1 min and $3.26 for opus-4.6 deterministic. Gemini-3-flash-preview agentic finishes in 11.1 min at $0.62 per program. Agentic input-token use is roughly an order of magnitude higher than deterministic (2.6–3.8M vs. 164–286K) because the agent reads files, inspects bytecode, and invokes subagents to ground each fix. We observe Heimdall (Agentic) with gpt-5.4 has a much lower runtime and output token consumption since the agent tends to give up early without attempting to fix the errors. The Unsafe Ops column tracks translation style, not policy compliance. The operations counted here are sanctioned escapes (helper invocations, packet-pointer arithmetic, ctx-pointer reads) rather than safety violations. The 3× gap between gpt-5.4 (6.3–9.2 ops) and the other models (18.1–30.3) is driven by translation choices. For example, gpt-5.4 abstracts the unsafe bpf_probe_read_kernel function into a safe wrapper function whose body holds the only unsafe block. Every kernel read at a call-site is a plain safe-Rust call. The other models inline unsafe bpf_probe_read_kernel(. . . ) at each read instead. So if a program performs ten kernel reads, gpt-5.4 contributes one unsafe op (the wrapper body) while the other models contribute ten, even though the runtime behavior is the same.
4.5
Full-scale Evaluation
We evaluate Heimdall (Agentic) with opus-4.6, the most successful approach in the benchmarks, across all 102 valid programs in our dataset. Of these, Heimdall produces 96/102 (94.1%) fully verified translations. Of the remaining six, none are true failures. Three are partially verified (bmc_kern, cache_ext_lhd, cache_ext_mglru) with some entry points verified and the others timing out due to symbolic execution time and memory limits. The other three (ksnoop, suricata_xdp_filter, suricata_xdp_lb) are unverified since all entry points exceed solver limits. Across all 102 attempted translations, the agent averages 27.3 min/program and consumes 2.0M input / 47K output tokens on average. This yields an average translation cost of $2.94 per program and $297 in total across all. The average is lower than the $4.05 cost from Table 3 since the 51-program subset in the
benchmarks is considerably harder to translate. The bytecode overhead of the produced Rust .o averages 2.89× over the C counterpart, and each translation contains 18.3 unsafe operations on average. To assess the effectiveness of Heimdall (Agentic), we investigate the operations the agent performs. Figure 3 groups the agent’s tool calls by purpose, separating main-agent and subagent contributions. The two largest categories are Code search with 769 calls (locating where a symbol or pattern lives across many files, via shell grep/find or the agent’s native search primitives) and file reading with 723 calls (loading the contents of a known file: C source under translation, the Aya framework source tree, and prior verified translations consumed as in-context examples). Together, these two exploration activities account for roughly 38 % of all 3,966 tool calls. The agent locates and ingests far more than it generates (code editing: 467 calls). The next-largest categories cover the four deterministic gates each translation must clear: compilation runs (463), equivalence checking (395), binary inspection (428) via llvm-objdump, and kernel verification (150). Another advantage of the agentic approach is subagent delegation. A subagent is invoked 68 times while translating 48/96 programs. The subagent makes 421 of the 3,966 combined tool calls (10.6%). Figure 4 breaks the subagent invocations down by purpose: 43 resolve Aya framework-API questions, 12 resolve C-side BPF headers (bits.bpf.h, maps.bpf.h, helper-macro definitions), and the remainder read documentation, prior verified translations, or inspect binaries. Heimdall (Agentic) thus exploits tool-mediated reasoning with test-time scaling — searching widely, ingesting and learning in-context from verified outputs, and delegating focused lookups to subagents — along with the five-stage pipeline to generate formally verified and idiomatic translations.
4.6
Verifier Gaps Closed in Dataset
To ensure that Heimdall adequately addresses the bug classes outlined in Section 2.1, we scan the C source of the 96 verified translations to identify instances of each bug class. Table 4 summarizes the result. Every observed bug class — uninitialized state, unchecked helper returns, and signed/unsigned confusion — is closed at 100 % on the in-dataset C instances. The uninitialized-state cases are the most consequential since they include both the KASLR-defeat finding from Section 1 and four cross-event content leaks. In bashreadline, the unchecked bpf_probe_read_user_str return combines with an 84-byte stack-resident struct str_t declared without zero-initialization.
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Code search
769
File reading
Conference’17, July 2017, Washington, DC, USA
Table 5: Runtime overhead and pass rate of Rust translations over 𝑁 =100 paired trials across 10 programs.
723
Runtime Overhead
695
Logging/file ops Code editing
467
Compilation
463
Binary inspection
Program bootstrap execsnoop exitsnoop opensnoop sigsnoop solisten statsnoop syncsnoop tcpconnlat tcplife
428
Equivalence checking
395
Kernel verification
150
Subagent delegation
Main agent Subagents
68
0
100
200
300
400
500
600
700
800
Tool calls (96 programs)
Pass 100/100 100/100 100/100 100/100 100/100 100/100 100/100 100/100 100/100 100/100
mean
95% CI
1.47× 1.33× 3.60× 1.86× 1.24× 1.14× 1.89× 1.17× 0.44× 1.09×
[1.33, 1.62] [1.17, 1.51] [3.14, 4.12] [1.44, 2.42] [1.17, 1.30] [1.01, 1.29] [1.55, 2.31] [1.08, 1.27] [0.39, 0.48] [0.96, 1.24]
1 Figure 3: Tool-call distribution across the 96-program verified evaluation, separated into main-agent and subagent contributions.
6% 6%
Framework API lookup (43) Header/helper lookup (12) Read documentation (4)
18% 63%
Read verified examples (4) Binary inspection (3) Misc. file read (2)
ringbuf-residue leaks of the same shape with smaller per-event leak surfaces. The unchecked-helper sites across 44 programs are handled with the ? operator, an Ok/Err match, or .map_err on the Result<T, E> that Aya helpers return. The six signed/unsigned confusion bugs are bpf_get_stackid sites translated to StackTrace::get_stackid() returning Result<i64, i64>, with an early-return on the Err arm and an i32 receiving field on the Ok side.
4.7 1 of 68 subagent invocations Figure 4: Purpose distribution across 48 programs in the verified set.
Table 4: Empirical analysis of bug classes from Table 1 addressed by Heimdall across the 96 verified translations. Bug Class Uninitialized state Unchecked helper returns Signed/unsigned confusion
C instances
Closed with Heimdall
10 44 6
10 (100%) 44 (100%) 6 (100%)
The Rust translation builds StrT via a struct literal (any missing field triggers error[E0063]) and propagates the helper return with the ? operator, closing both bug classes at the same site. opensnoop, mountsnoop, filelife, and bootstrap all use ring buffers without zero-filling the reserved slot in C; the Rust translations insert core::ptr::write_bytes(.., 0, size_of::<Event>()) immediately after RingBuf::reserve::<T>(0), eliminating the cross-record residue described in Section 1. bootstrap additionally reserves two distinct slots in its exec and exit branches with different field subsets written on each path; both are zeroed before population. The remaining five uninitialized state cases are
Runtime Validation
To ensure that the formally equivalent programs actually behave similarly to their C counterparts, we built common userspace loaders for 10 verified Heimdall (Agentic) opus 4.6 translations (bootstrap, opensnoop, sigsnoop, statsnoop, tcplife, exitsnoop, tcpconnlat, solisten, execsnoop, syncsnoop) and ran each of C and Rust under the same controlled workload (file opens, signals, forking children, loopback connections). We repeat each program 𝑁 =100 times (1,000 paired trials total). We restrict our comparison to our trigger-induced events only since certain fields always change across runs; for example, timestamps, PIDs, and ephemeral ports. We read per-program ns/invocation from kernel.bpf_stats_enabled. All 1,000/1,000 trials match exactly with identical filtered record counts. Since the equivalence side is uniform, we report runtime overhead as the geometric mean of the per-trial Rust/C ratio with a Student’s 𝑡 95% confidence interval computed on log-ratios (Table 5). Seven of ten per-program CIs lie strictly above 1×, tcplife’s CI overlaps 1× ([0.96, 1.24]), and tcpconnlat’s CI lies strictly below ([0.39, 0.48]). Our runtime validation experiments also validate the safety gaps Heimdall closes. In opensnoop, the C side leaves the ts field unwritten and emits stack residue, while the Rust translation emits ts=0. We ignore this field on both sides since the divergence is intentional and confirms the safety pass enforces zeroing on a production program.
Conference’17, July 2017, Washington, DC, USA
5 Related Work 5.1 eBPF Analysis A substantial body of work has tackled the soundness and analysis of the eBPF substrate itself, rather than its migration to safer languages. Huang et al. [27] survey complementary paths toward eBPF memory safety such as verifier hardening, runtime checks, language-based approaches and identify languagebased migration to Rust/Aya as a promising but underexplored direction that Heimdall concretizes with formal per-program equivalence. PREVAIL [21] replaces the in-kernel verifier with an abstract-interpretation-based static analyzer. Complementary work formally models the verifier to find soundness bugs or improve its precision via proof-guided abstraction refinement [56, 57], or fuzzes it with differential, state-embedding, and specification-based oracles [37, 47, 54]. Other axes add runtime checks [14, 55] that confine or augment extension execution beyond what the verifier proves, hardware isolation via Intel MPK [36], or proof-carrying code via an annotation-guided toolchain [59]. Jitterbug [42] verifies the eBPF JIT compilers themselves. For language-based security and symbolic execution specifically, Rex [32] sidesteps the in-kernel verifier entirely by running Rust eBPF programs directly with type-system and runtime-check-based safety, but does not address the legacy migration problem. eBPFSE [30] extends KLEE [10] at the C source level (requiring C-side annotations and not supporting Rust), and Serval [41] lifts an interpreter into a Rosette-based BPF verifier used to check JIT-compiler correctness on individual BPF instructions. Both target verifier- or JIT-side properties. Neither models BPF maps, the broader helper set, ELF relocations, or BPF-to-BPF subprogram calls. On the synthesis side, K2 [62] generates safe and efficient packet-processing eBPF programs from high-level specifications, and KEN/KGent [63] drives natural-language-to-eBPF code generation with an LLM agent. None of these systems translate between the C and Rust eBPF dialects or check semantic equivalence between two eBPF objects.
5.2
C-to-Rust Translation
Rule-based approaches. C2Rust [19] produces a faithful AST-level transliteration from C that is functionally correct but pervasively unsafe. A series of static-analysis post-processors — Laertes [16], Crown [61], Concrat [24], Forcrat [26], and PR2 [20] — apply ownership inference, pointer lifting, or API-specific rewrites (locks, I/O) on top of C2Rust output to reduce unsafe usage, but retain unsafe in the general case and provide no semantic equivalence guarantee. LLM-based and hybrid approaches. A growing line of work translates C to safer Rust with LLMs, either end-to-end [11, 17, 18, 25, 50, 58] or by combining LLMs with static analysis or differential testing on top of a C2Rust skeleton [44, 49, 64]. ReCodeAgent [28] proposes a multi-agent coding workflow for language-agnostic translation. Most closely related on the verification axis is VERT [60], which lifts the C source through Wasm into an oracle Rust program and checks bounded equivalence between the oracle and LLM-produced Rust. However, VERT’s Wasm path does not exist for eBPF (which compiles to a distinct bytecode with its own helpers, maps, and
Dasu et. al
verifier constraints), and its bounded model checking does not scale to programs with complex data structures. With the exception of VERT, the systems above establish equivalence through differential fuzzing or generated test cases rather than a formal proof, so silent semantic divergences that aren’t surfaced by the test workload escape detection. Crucially, none of them target eBPF: their toolchains assume libc, std, and a hosted runtime, none of which are available to in-kernel eBPF programs. Heimdall closes both gaps — formal symbolic equivalence as the success criterion, and a translation pipeline that produces eBPF-valid Aya Rust — within a single autonomous loop.
6
Discussion
Limitations. We rely on monolithic symbolic execution over the full eBPF bytecode to discharge equivalence. This times out on large programs: six of our 102 attempted translations hit our 𝑛=50,000 path-exploration cap on at least one entry point. We hypothesize this is due to path explosion in programs with deeply nested branching, large constant tables, or long write traces against tracked map state. Additionally, our static safety policy is a hand-curated set of pattern-based rules. While it strictly enforces every rule it covers, it cannot anticipate idiomaticity issues we have not yet encountered, and bug classes whose runtime effect lands on the helper-success path and inside tracked map state (i.e., outside our safety condition Φsafe ) remain out of scope for an equivalence-preserving pipeline. Another limitation of our approach is that we detect dropped atomicity via a static bytecode scan that compares atomic-opcode totals between the C and Rust binaries, which is a coarse heuristic rather than a per-site atomicity proof.
Threats to Validity. Symbolic execution and equivalence checking are only as faithful as their modeling; our angr backend caps path exploration at 𝑛=50,000, models 56 helper stubs, eBPF maps, and output sinks to the best of our ability, and limits ringbuf reservations to 512 bytes for tractable equivalence checking. A program that exercises behavior beyond these caps may be incorrectly admitted or rejected. To make safety-improving Rust translations pass equivalence against legacy C source, we adopt two explicit modeling exceptions, both enforced uniformly across the dataset. First, helpers are modeled along the success path and helper-failure behavior is audited separately under a stricter helper-failure mode, so a Rust translation that short-circuits on the typed Err variant remains equivalent to a C source that ignores the helper-failure return. Second, ringbuf and perf-event output content is treated as a write-only sink in the default equivalence check (so the Rust safety policy to zero-out uninitialized memory does not diverge from the C program’s residual stale data), and is audited separately under a stricter output-sink tracking mode that records the per-event emitted bytes for cross-binary comparison. Generalization to arbitrary eBPF programs beyond our dataset is bound by our modeling scope: the kernel exposes 100+ eBPF helpers, but we model 56, and our safety policy targets a subset of unsafe patterns rather than every possible hazard.
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
7
Conclusion
We presented Heimdall, the first system for formally verified automated migration of eBPF programs from C to Rust. Heimdall combines LLM-driven translation with bytecode-level symbolic equivalence checking and a static safe-Aya analyzer, producing translations that are formally equivalent to the original C program across all inputs and free of the residual unsafe-Rust patterns. Across 102 real-world eBPF programs, Heimdall generates 96 (94.1 %) verified translations. For future work, one may explore strategies to incorporate performance optimization techniques like bytecode size and execution time into the feedback loop. Additionally, compositional reasoning over individual functions or basic blocks would enable scaling up to much larger and more complicated eBPF programs. Lastly, since our eBPF symbolic execution and equivalence engine is frontendagnostic, one may explore translation strategies across other languages like Go, Python, and Java.
References [1] 2016. Can’t read in struct fields even with bpf_probe_read: -EFAULT. https: //github.com/iovisor/bcc/issues/622. [2] 2017. invalid indirect read from stack with uninitialized struct. https: //github.com/iovisor/bcc/issues/919. [3] 2019. bpf_probe_read() returned -14. https://github.com/iovisor/bcc/issues/ 2245. [4] 2019. invalid indirect read from stack off -16+4 size 16 when tracing spinlocks. https://github.com/iovisor/bcc/issues/2623. [5] 2020. bpf_probe_read_user returns error ( −14) and opensnoop emits empty filenames. https://github.com/iovisor/bcc/issues/3175. [6] 2025. Tetragon does not raise an event when the resolved value is null. https: //github.com/cilium/tetragon/issues/3728. [7] Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. 2018. Counterexample guided inductive synthesis modulo theories. In International Conference on Computer Aided Verification. Springer, 270–288. [8] Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. IEEE, 1–8. [9] BCC Contributors. 2024. libbpf-tools: BPF CO-RE Tools. https://github.com/iov isor/bcc/tree/master/libbpf-tools. [10] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (OSDI’08). USENIX Association, USA, 209–224. [11] Xuemeng Cai, Jiakun Liu, Xiping Huang, Yijun Yu, Haitao Wu, Chunmiao Li, Bo Wang, Imam Nur Bani Yusuf, and Lingxiao Jiang. 2025. RustMap: Towards Project-Scale C-to-Rust Migration via Program Analysis and LLM. arXiv:2503.17741 [cs.SE] https://arxiv.org/abs/2503.17741 [12] daeuniverse. 2023. dae: A Linux High-Performance Transparent Proxy Based on eBPF. https://github.com/daeuniverse/dae. [13] Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 4963). Springer, 337–340. [14] Kumar Kartikeya Dwivedi, Rishabh Iyer, and Sanidhya Kashyap. 2024. Fast, Flexible, and Practical Kernel Extensions. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (Austin, TX, USA) (SOSP ’24). Association for Computing Machinery, New York, NY, USA, 249–264. doi:10.114 5/3694715.3695950 [15] eBPF Foundation. 2024. eBPF: Extended Berkeley Packet Filter. https://ebpf.io/. [16] Mehmet Emre, Ryan Schroeder, Kyle Dewey, and Ben Hardekopf. 2021. Translating C to safer Rust. Proc. ACM Program. Lang. 5, OOPSLA, Article 121 (Oct. 2021), 29 pages. doi:10.1145/3485498 [17] Hasan Ferit Eniser, Hanliang Zhang, Cristina David, Meng Wang, Maria Christakis, Brandon Paulsen, Joey Dodds, and Daniel Kroening. 2024. Towards Translating Real-World Code with LLMs: A Study of Translating to Rust. arXiv:2405.11514 [cs.SE] https://arxiv.org/abs/2405.11514 [18] Muhammad Farrukh, Smeet Shah, Baris Coskun, and Michalis Polychronakis. 2025. SafeTrans: LLM-assisted Transpilation from C to Rust.
Conference’17, July 2017, Washington, DC, USA
arXiv:2505.10708 [cs.CR] https://arxiv.org/abs/2505.10708 [19] Galois. 2018. C2Rust. https://galois.com/blog/2018/08/c2rust/ [20] Yifei Gao, Chengpeng Wang, Pengxiang Huang, Xuwei Liu, Mingwei Zheng, and Xiangyu Zhang. 2025. PR2: Peephole Raw Pointer Rewriting with LLMs for Translating C to Safer Rust. arXiv:2505.04852 [cs.SE] https://arxiv.org/abs/2505 .04852 [21] Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv. 2019. Simple and precise static analysis of untrusted Linux kernel extensions. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (Phoenix, AZ, USA) (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 1069–1084. doi:10.1145/3314221.3314590 [22] Yoann Ghigoff, Julien Sopena, Kahina Lazri, Antoine Blin, and Gilles Muller. 2021. BMC: Accelerating Memcached using Safe In-kernel Caching and Prestack Processing. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 487–501. https://www.usenix.o rg/conference/nsdi21/presentation/ghigoff [23] Toke Høiland-Jørgensen, Jesper Dangaard Brouer, Daniel Borkmann, John Fastabend, Tom Herbert, David Ahern, and David Miller. 2018. The eXpress data path: fast programmable packet processing in the operating system kernel. In Proceedings of the 14th International Conference on Emerging Networking EXperiments and Technologies (Heraklion, Greece) (CoNEXT ’18). Association for Computing Machinery, New York, NY, USA, 54–66. doi:10.1145/3281411.3281443 [24] Jaemin Hong and Sukyoung Ryu. 2023. Concrat: An Automatic C-to-Rust Lock API Translator for Concurrent Programs. arXiv:2301.10943 [cs.SE] https://arxiv. org/abs/2301.10943 [25] Jaemin Hong and Sukyoung Ryu. 2024. To Tag, or Not to Tag: Translating C’s Unions to Rust’s Tagged Unions. arXiv:2408.11418 [cs.SE] https://arxiv.org/abs/ 2408.11418 [26] Jaemin Hong and Sukyoung Ryu. 2025. Forcrat: Automatic I/O API Translation from C to Rust via Origin and Capability Analysis. arXiv:2506.01427 [cs.SE] https://arxiv.org/abs/2506.01427 [27] Kaiming Huang, Mathias Payer, Zhiyun Qian, Jack Sampson, Gang Tan, and Trent Jaeger. 2025. SoK: Challenges and Paths Toward Memory Safety for eBPF. In Proceedings of the 2025 IEEE Symposium on Security and Privacy (SP). IEEE, 848–866. [28] Ali Reza Ibrahimzada, Brandon Paulsen, Daniel Kroening, and Reyhaneh Jabbarvand. 2026. ReCodeAgent: A Multi-Agent Workflow for Language-agnostic Translation and Validation of Large-scale Repositories. arXiv:2604.07341 [cs.SE] https://arxiv.org/abs/2604.07341 [29] IO Visor Project. 2024. BCC: Tools for BPF-based Linux IO Analysis, Networking, Monitoring, and More. https://github.com/iovisor/bcc. [30] Rishabh Iyer, Katerina Argyraki, and George Candea. 2022. Performance Interfaces for Network Functions. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Renton, WA, 567–584. https://www.usenix.org/conference/nsdi22/presentation/iyer [31] Susmit Jha and Sanjit A Seshia. 2017. A theory of formal synthesis via inductive learning. Acta Informatica 54, 7 (2017), 693–726. [32] Jinghao Jia, Ruowen Qin, Milo Craun, Egor Lukiyanov, Ayush Bansal, Minh Phan, Michael V. Le, Hubertus Franke, Hani Jamjoom, Tianyin Xu, and Dan Williams. 2025. Rex: closing the language-verifier gap with safe and usable kernel extensions. In Proceedings of the 2025 USENIX Conference on Usenix Annual Technical Conference (Boston, MA, USA) (USENIX ATC ’25). USENIX Association, USA, Article 20, 18 pages. [33] Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2024. SWE-bench: Can Language Models Resolve RealWorld GitHub Issues? arXiv:2310.06770 [cs.CL] https://arxiv.org/abs/2310.06770 [34] Marios Kogias, Rishabh Iyer, and Edouard Bugnion. 2020. Bypassing the Load Balancer Without Regrets. In Proceedings of the 11th ACM Symposium on Cloud Computing (Virtual Event, USA) (SoCC ’20). Association for Computing Machinery, New York, NY, USA, 193–207. doi:10.1145/3419111.3421304 [35] libbpf Contributors. 2024. libbpf-bootstrap: Scaffolding for BPF CO-RE applications. https://github.com/libbpf/libbpf-bootstrap. [36] Hongyi Lu, Shuai Wang, Yechang Wu, Wanning He, and Fengwei Zhang. 2024. MOAT: Towards Safe BPF Kernel Extension. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 1153–1170. https: //www.usenix.org/conference/usenixsecurity24/presentation/lu-hongyi [37] Tao Lyu, Kumar Kartikeya Dwivedi, Thomas Bourgeat, Mathias Payer, Meng Xu, and Sanidhya Kashyap. 2025. eBPF Misbehavior Detection: Fuzzing with a Specification-Based Oracle. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles (Lotte Hotel World, Seoul, Republic of Korea) (SOSP ’25). Association for Computing Machinery, New York, NY, USA, 701–718. doi:10.1145/3731569.3764797 [38] John McCarthy. 1993. Towards a mathematical science of computation. In Program verification: Fundamental issues in computer science. Springer, 35–56. [39] Mike A. Merrill, Alexander G. Shaw, Nicholas Carlini, Boxuan Li, Harsh Raj, Ivan Bercovich, Lin Shi, Jeong Yeon Shin, Thomas Walshe, E. Kelly Buchanan,
Conference’17, July 2017, Washington, DC, USA
Junhong Shen, Guanghao Ye, Haowei Lin, Jason Poulos, Maoyu Wang, Marianna Nezhurina, Jenia Jitsev, Di Lu, Orfeas Menis Mastromichalakis, Zhiwei Xu, Zizhao Chen, Yue Liu, Robert Zhang, Leon Liangyu Chen, Anurag Kashyap, JanLucas Uslu, Jeffrey Li, Jianbo Wu, Minghao Yan, Song Bian, Vedang Sharma, Ke Sun, Steven Dillmann, Akshay Anand, Andrew Lanpouthakoun, Bardia Koopah, Changran Hu, Etash Guha, Gabriel H. S. Dreiman, Jiacheng Zhu, Karl Krauth, Li Zhong, Niklas Muennighoff, Robert Amanfu, Shangyin Tan, Shreyas Pimpalgaonkar, Tushar Aggarwal, Xiangning Lin, Xin Lan, Xuandong Zhao, Yiqing Liang, Yuanli Wang, Zilong Wang, Changzhi Zhou, David Heineman, Hange Liu, Harsh Trivedi, John Yang, Junhong Lin, Manish Shetty, Michael Yang, Nabil Omi, Negin Raoof, Shanda Li, Terry Yue Zhuo, Wuwei Lin, Yiwei Dai, Yuxin Wang, Wenhao Chai, Shang Zhou, Dariush Wahdany, Ziyu She, Jiaming Hu, Zhikang Dong, Yuxuan Zhu, Sasha Cui, Ahson Saiyed, Arinbjörn Kolbeinsson, Jesse Hu, Christopher Michael Rytting, Ryan Marten, Yixin Wang, Alex Dimakis, Andy Konwinski, and Ludwig Schmidt. 2026. Terminal-Bench: Benchmarking Agents on Hard, Realistic Tasks in Command Line Interfaces. arXiv:2601.11868 [cs.SE] https://arxiv.org/abs/2601.11868 [40] Samuel Miserendino, Michele Wang, Tejal Patwardhan, and Johannes Heidecke. 2025. SWE-Lancer: Can Frontier LLMs Earn $1 Million from Real-World Freelance Software Engineering? arXiv:2502.12115 [cs.LG] https://arxiv.org/abs/2502.12115 [41] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (Huntsville, Ontario, Canada) (SOSP ’19). Association for Computing Machinery, New York, NY, USA, 225–242. doi:10.1145/3341301.3359641 [42] Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and verification in the field: Applying formal methods to BPF just-intime compilers in the Linux kernel. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 41–61. https://www.usenix.org/conference/osdi20/presentation/nelson [43] Network Security Group, ETH Zürich. 2023. Hercules: High-Speed Bulk Data Transfer Using XDP. https://github.com/netsec-ethz/hercules. [44] Vikram Nitin, Rahul Krishna, Luiz Lemos do Valle, and Baishakhi Ray. 2025. C2SaferRust: Transforming C Projects into Safer Rust with NeuroSymbolic Techniques. arXiv:2501.14257 [cs.SE] https://arxiv.org/abs/2501.14257 [45] NTT Communications. 2023. Fluvia: IPFIX Exporter Using XDP. https://github.c om/nttcom/fluvia. [46] Open Information Security Foundation. 2024. Suricata: Open Source IDS/IPS/NSM Engine. https://suricata.io/. [47] Chaoyuan Peng, Muhui Jiang, Lei Wu, and Yajin Zhou. 2024. Toss a Fault to BpfChecker: Revealing Implementation Flaws for eBPF runtimes with Differential Fuzzing. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security (Salt Lake City, UT, USA) (CCS ’24). Association for Computing Machinery, New York, NY, USA, 3928–3942. doi:10.1145/3658644.36 90237 [48] Polar Signals. 2024. Parca Agent: eBPF-based Always-On Continuous Profiler. https://github.com/parca-dev/parca-agent. [49] Manish Shetty, Naman Jain, Adwait Godbole, Sanjit A. Seshia, and Koushik Sen. 2024. Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis. arXiv:2412.14234 [cs.SE] https://arxiv.org/abs/2412.14234 [50] Momoko Shiraishi, Yinzhi Cao, and Takahiro Shinagawa. 2026. SmartC2Rust: Iterative, Feedback-Driven C-to-Rust Translation via Large Language Models for Safety and Equivalence. [51] Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. 2016. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In 2016 IEEE Symposium on Security and Privacy (SP). 138–157. doi:10.1109/SP.2016.17 [52] Armando Solar-Lezama. 2013. Program sketching. International Journal on Software Tools for Technology Transfer 15, 5 (2013), 475–495. [53] Marco Spaziani Brunella, Giacomo Belocchi, Marco Bonola, Salvatore Pontarelli, Giuseppe Siracusano, Giuseppe Bianchi, Aniello Cammarano, Alessandro Palumbo, Luca Petrucci, and Roberto Bifulco. 2020. hXDP: Efficient Software Packet Processing on FPGA NICs. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 973–990. https://www.usenix.org/conference/osdi20/presentation/brunella [54] Hao Sun and Zhendong Su. 2024. Validating the eBPF Verifier via State Embedding. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, 615–628. [55] Hao Sun and Zhendong Su. 2025. Approximation Enforced Execution of Untrusted Linux Kernel Extensions. In 34th USENIX Security Symposium (USENIX Security 25). USENIX Association, Seattle, WA, 7467–7485. https://www.usenix.org/con ference/usenixsecurity25/presentation/sun-hao [56] Hao Sun and Zhendong Su. 2025. Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction Refinement. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles (Lotte Hotel World, Seoul, Republic of Korea) (SOSP ’25). Association for Computing Machinery, New York, NY, USA, 736–751. doi:10.1145/3731569.3764796
Dasu et. al
[57] Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2023. Verifying the Verifier: eBPF Range Analysis Verification. In Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III (Paris, France). Springer-Verlag, Berlin, Heidelberg, 226–251. doi:10.1007/978-3-031-37709-9_12 [58] Chaofan Wang, Tingrui Yu, Jie Wang, Dong Chen, Wenrui Zhang, Yuling Shi, Xiaodong Gu, and Beijun Shen. 2025. EVOC2RUST: A Skeleton-guided Framework for Project-Level C-to-Rust Translation. arXiv:2508.04295 [cs.SE] https://arxiv.org/abs/2508.04295 [59] Xiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu, Shengkai Lin, Lihan Xie, Shizhen Zhao, and Qinxiang Cao. 2025. VEP: A Two-stage Verification Toolchain for Full eBPF Programmability. In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25). USENIX Association, Philadelphia, PA, 277–299. https://www.usenix.org/conference/nsdi25/presentation/wu-xiwei [60] Aidan Z. H. Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, and Daniel Kroening. 2024. VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners. arXiv:2404.18852 [cs.PL] https: //arxiv.org/abs/2404.18852 [61] Hanliang Zhang, Cristina David, Yijun Yu, and Meng Wang. 2023. Ownership guided C to Rust translation. arXiv:2303.10515 [cs.PL] https://arxiv.org/abs/2303 .10515 [62] Yusheng Zheng, Yiwei Yang, Maolin Chen, and Andrew Quinn. 2024. Kgent: Kernel Extensions Large Language Model Agent. In Proceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions (Sydney, NSW, Australia) (eBPF ’24). Association for Computing Machinery, New York, NY, USA, 30–36. doi:10.1145/3672197.3673434 [63] Yusheng Zheng, Yiwei Yang, Maolin Chen, and Andrew Quinn. 2024. Kgent: Kernel Extensions Large Language Model Agent. In Proceedings of the ACM SIGCOMM 2024 Workshop on EBPF and Kernel Extensions (Sydney, NSW, Australia) (eBPF ’24). Association for Computing Machinery, New York, NY, USA, 30–36. doi:10.1145/3672197.3673434 [64] Tianyang Zhou, Haowen Lin, Somesh Jha, Mihai Christodorescu, Kirill Levchenko, and Varun Chandrasekaran. 2025. LLM-Driven Multi-step Translation from C to Rust using Static Analysis. arXiv:2503.12511 [cs.SE] https://arxiv.org/abs/2503.1 2511 [65] Tal Zussman, Ioannis Zarkadas, Jeremy Carin, Andrew Cheng, Hubertus Franke, Jonas Pfefferle, and Asaf Cidon. 2025. cache_ext: Customizing the Page Cache with eBPF. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles (Lotte Hotel World, Seoul, Republic of Korea) (SOSP ’25). Association for Computing Machinery, New York, NY, USA, 462–478. doi:10.1145/3731569.3764820
A
C Listings for Bug Classes
This appendix contains listings for the six bug classes in Section 2.1. #include "vmlinux.h" #include <bpf/bpf_helpers.h> 3 #include <bpf/bpf_tracing.h> 1 2
4 5 6
#define TASK_COMM_LEN 16 #define MAX_LINE_SIZE 80
7
struct str_t { __u32 pid; 10 char str[MAX_LINE_SIZE]; 11 }; 8 9
12
struct { __uint(type, BPF_MAP_TYPE_PERF_EVENT_ARRAY); 15 __uint(key_size, sizeof(__u32)); 16 __uint(value_size, sizeof(__u32)); 17 } events SEC(".maps"); 13 14
18
SEC("uretprobe/readline") int BPF_URETPROBE(printret, const void *ret) { 21 struct str_t data; /* BUG: not zero-initialized */ 22 char comm[TASK_COMM_LEN]; 23 u32 pid; 19 20
24 25
if (!ret)
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
return 0;
26 27
bpf_get_current_comm(&comm, sizeof(comm)); if (comm[0] != 'b' || comm[1] != 'a' || comm[2] != 's' || comm[3] != 'h' || comm[4] != 0) return 0;
29 30 31 32
pid = bpf_get_current_pid_tgid() >> 32; data.pid = pid; bpf_probe_read_user_str( /* BUG: return IGNORED */ &data.str, sizeof(data.str), ret);
33 34 35 36 37 38 39
41
}
39
1
return 0;
5
char LICENSE[] SEC("license") = "GPL";
Listing 3: Full listing for Listing 1 (uninitialized state & unchecked helper return): libbpf-tools bashreadline.bpf.c verbatim. struct str_t is declared on the stack with no zero-initialization, and the return value of bpf_probe_read_user_str is never inspected.
return 0;
char LICENSE[] SEC("license") = "GPL";
Listing 4: Full listing for Listing 2 (buffer/size mismatch). The intended header pointer is &evt.pub, but the size argument is sizeof(evt), so the helper also copies the private task_ptr and ip_ptr fields.
bpf_perf_event_output(ctx, &events, BPF_F_CURRENT_CPU, &data, sizeof(data));
43
}
38
2
40
44
36 37
28
42
Conference’17, July 2017, Washington, DC, USA
#include "vmlinux.h" #include <bpf/bpf_helpers.h>
3
struct event { __u32 protocol; /* will contain rx_queue_index */ 6 __u32 queue_mapping; /* will contain ingress_ifindex */ 7 }; 4
8
struct { __uint(type, BPF_MAP_TYPE_PERF_EVENT_ARRAY); 11 __uint(key_size, sizeof(__u32)); 12 __uint(value_size, sizeof(__u32)); 13 } events SEC(".maps"); 9
10
14
SEC("xdp") int monitor_packets(struct __sk_buff *skb) /* BUG: wrong ctx type */ 17 { 18 struct event evt = {}; 19 evt.protocol = skb->protocol; /* actually rx_queue_index */ 20 evt.queue_mapping = skb->queue_mapping; /* actually ingress_ifindex */ 21 bpf_perf_event_output(skb, &events, 22 BPF_F_CURRENT_CPU, &evt, sizeof(evt)); 23 return XDP_PASS; 24 } 15
#include "vmlinux.h" 2 #include <bpf/bpf_helpers.h> 3 #include <bpf/bpf_tracing.h> 4 #include <bpf/bpf_core_read.h> 1
5
struct public_event { __u32 pid; 8 __u32 reserved; 9 __u64 timestamp; 10 }; 6 7
11
struct full_event { struct public_event pub; 14 __u64 task_ptr; /* private: kernel address */ 15 __u64 ip_ptr; /* private: kernel address */ 16 }; 12 13
17
struct { __uint(type, BPF_MAP_TYPE_PERF_EVENT_ARRAY); 20 __uint(key_size, sizeof(__u32)); 21 __uint(value_size, sizeof(__u32)); 22 } events SEC(".maps"); 18
16
25 26
char LICENSE[] SEC("license") = "GPL";
Listing 5: Hook/context mismatch: XDP program declares its parameter as struct __sk_buff, the TC context type. Under XDP, offset 16 is rx_queue_index, not protocol.
19
23
27
29 30 31
evt.pub.pid = bpf_get_current_pid_tgid() >> 32; evt.pub.timestamp = bpf_ktime_get_ns(); evt.task_ptr = (__u64)bpf_get_current_task(); evt.ip_ptr = PT_REGS_IP_CORE(ctx);
32 33
34 35
2
#include "vmlinux.h" #include <bpf/bpf_helpers.h>
3
struct conn { __u32 src_ip, dst_ip; }; /* map value: 8 B */ 5 struct stats { __u64 bytes; }; /* wrong type: 8 B */ 6 struct big { __u32 a, b, c, d; }; /* wrong type: 16 B */ 4
SEC("kprobe/do_sys_openat2") 25 int output_size_leak(struct pt_regs *ctx) { 26 struct full_event evt = {}; 24
28
1
/* BUG: pointer to public header, size of the enclosing object */ bpf_perf_event_output(ctx, &events, BPF_F_CURRENT_CPU, &evt.pub, sizeof(evt));
7
struct { __uint(type, BPF_MAP_TYPE_ARRAY); 10 __type(key, __u32); 11 __type(value, struct conn); /* value_size = 8 */ 12 __uint(max_entries, 1); 13 } data SEC(".maps"); 8 9
14
Conference’17, July 2017, Washington, DC, USA
SEC("xdp") int map_schema_bug(struct xdp_md *ctx) { 17 __u32 key = 0; 18 struct big val = { 1, 2, 3, 4 };
Dasu et. al
15
34
16
35
19
37
/* BUG 1: 16B payload written into 8B slot; truncated silently. */ bpf_map_update_elem(&data, &key, &val, BPF_ANY);
20
21 22
24 25 26 27
28 29 30
}
/* BUG 2: void* result cast to wrong struct type. */ struct stats *s = (struct stats *) bpf_map_lookup_elem(&data, &key); if (s) { __u64 b = s->bytes; /* reinterprets (src_ip|dst_ip ) as u64 */ bpf_printk("bytes=%llu", b); } return XDP_PASS;
32 33
38 39 40
}
41
23
31
36
val = bpf_map_lookup_elem(&counts, key); if (!val) bpf_map_update_elem(&counts, key, &zero, BPF_NOEXIST); val = bpf_map_lookup_elem(&counts, key); if (val) __sync_fetch_and_add(val, 1);
char LICENSE[] SEC("license") = "GPL";
Listing 6: Map type/schema confusion in one program: a 16byte struct is written into an 8-byte slot, and the void* result of bpf_map_lookup_elem is cast to an unrelated struct type.
42
Listing 7: Signed/unsigned confusion in the kernel’s offwaketime sample: bpf_get_stackid returns a signed long, but the stack-id fields are declared u32, so negative error codes become large positive map keys.
B
End-to-End Symbolic Execution Example
Figure 5 traces two eBPF instructions through the full symbolic execution pipeline, from raw bytecode to symbolic formula. The pattern bpf_get_current_pid_tgid() » 32 (extracting the thread group ID) is ubiquitous in tracing programs, so it serves as a compact example of lifting, helper dispatch, and symbolic state construction.
C #include "vmlinux.h" #include <bpf/bpf_helpers.h> 3 #include <bpf/bpf_tracing.h>
char LICENSE[] SEC("license") = "GPL";
End-to-End ITE-Chains and Formula Generation Example
1 2
4 5
#define TASK_COMM_LEN 16
6
struct key_t { char waker[TASK_COMM_LEN]; 9 char target[TASK_COMM_LEN]; 10 u32 wret; /* BUG: should be s32 or int */ 11 u32 tret; /* BUG: should be s32 or int */ 12 }; 7 8
13
1 2
#include "vmlinux.h" #include <bpf/bpf_helpers.h>
3
struct { __uint(type, BPF_MAP_TYPE_HASH); 6 __type(key, __u32); 7 __type(value, __u32); 8 __uint(max_entries, 256); 9 } counters SEC(".maps"); 4 5
struct { __uint(type, BPF_MAP_TYPE_STACK_TRACE); 16 __uint(key_size, sizeof(u32)); 17 __uint(value_size, PERF_MAX_STACK_DEPTH * sizeof(u64) ); 18 __uint(max_entries, 10000); 19 } stackmap SEC(".maps"); 14 15
20
struct { __uint(type, BPF_MAP_TYPE_HASH); 23 __type(key, struct key_t); 24 __type(value, u64); 25 __uint(max_entries, 10000); 26 } counts SEC(".maps"); 21 22
27
static inline void update_counts(void *ctx, struct key_t *key, u32 flags) 29 { 30 /* BUG: negative errno (-EEXIST, -ENOMEM, ...) stored as u32 */ 31 key->tret = bpf_get_stackid(ctx, &stackmap, flags); 28
32 33
We illustrate the complete symbolic execution and equivalence checking pipeline on a minimal eBPF program, instantiating the encoding of Section 3.3 (Equation (3)) on a concrete two-path program. Listing 8 shows a kprobe that maintains a per-PID hit counter in a hash map: if the PID’s entry exists, it increments the value; otherwise, it inserts 1.
u64 zero = 0, *val;
10
SEC("kprobe/__x64_sys_read") int count_reads(struct pt_regs *ctx) { 13 __u32 pid = bpf_get_current_pid_tgid() >> 32; 14 __u32 *val = bpf_map_lookup_elem( 15 &counters, &pid); 16 if (val) 17 *val += 1; 18 else { 19 __u32 one = 1; 20 bpf_map_update_elem( 21 &counters, &pid, &one, 0); 22 } 23 return 0; 24 } 11 12
Listing 8: Minimal eBPF program: per-PID counter in a hash map.
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Raw eBPF bytecode (16 bytes, little-endian)
Conference’17, July 2017, Washington, DC, USA
Path 0 (lookup hit → in-place increment via pointer):
85 00 00 00 0e 00 00 00
call 14
𝜙 0 = (𝑒 0 = 1)
77 00 00 00 20 00 00 00
r0 >>= 32
𝑟0 = 0 write trace :
Lifter decode
Insn 1: opcode 0x85 = 1000 0 101 , imm = 14 |{z} |{z} |{z} call
K
Path 1 (lookup miss → update_elem insert): 𝜙 1 = (𝑒 0 = 0)
JMP64
Insn 2: opcode 0x77 = 0111 0 111 , dst = R0, imm = 32 |{z} |{z} |{z} rsh
K
⟨𝑘 1 =𝑘, 𝑣 1 =𝑣 0 [31:0] + 1, 𝑒 1 =1⟩
𝑟1 = 0 write trace :
ALU64
VEX IR generation
Insn 1 → VEX IR: PUT(syscall) = 0x0e exit Ijk_Sys_syscall Insn 2 → VEX IR: t0 = GET(R0) t1 = Shr64(t0, 0x20) PUT(R0) = t1 Helper dispatch class BpfGetCurrentPidTgid(SimProcedure): def run(self): pid_tgid = BVS('input_pid_tgid', 64) self.state.add_constraints( (pid_tgid & 0xFFFFFFFF) > 0) self.state.add_constraints( (pid_tgid >> 32) > 0) return pid_tgid Symbolic state
R0 = input_pid_tgid >> 32 (= tgid, symbolic) Constraints: pid > 0, tgid > 0 Figure 5: End-to-end trace of two eBPF instructions through our backend that highlights instruction lifting, VEX IR generation, helper dispatch, and the resulting symbolic state.
⟨𝑘 1 =𝑘, 𝑣 1 =1, 𝑒 1 =1⟩
Both paths return 𝑅0 = 0, and 𝜙 0 ∨ 𝜙 1 = true partitions the input space on the symbolic existence of the key prior to execution. Per-path ITE chains. Instantiating Equation (3) on each one-write trace and substituting 𝑒 1 = 1 (no deletes): 𝜋0 𝑉ctr (𝑘𝑞 ) ≜ Ite 𝑘𝑞 = 𝑘 ∧ 𝑒 1 = 1, 𝑣 0 [31:0] + 1, 𝑣 init = Ite 𝑘𝑞 = 𝑘, 𝑣 0 [31:0] + 1, 𝑣 init 𝜋1 𝑉ctr (𝑘𝑞 ) ≜ Ite 𝑘𝑞 = 𝑘, 1, 𝑣 init . The parallel presence chains follow the inner shape from Section 3.3 (branch on 𝑘𝑞 = 𝑘𝑖 alone, return 𝑒𝑖 ): 𝜋0 𝑃 ctr (𝑘𝑞 ) ≜ Ite 𝑘𝑞 = 𝑘, Ite(𝑒 1 = 1, 1, 0), 𝑝 init = Ite 𝑘𝑞 = 𝑘, 1, 𝑝 init 𝜋1 𝑃 ctr (𝑘𝑞 ) ≜ Ite 𝑘𝑞 = 𝑘, 1, 𝑝 init . Per-program ITE chains. Combining the per-path chains under their respective path predicates yields the per-program chains: 𝜋0 𝜋1 𝑉ctr (𝑘𝑞 ) ≜ Ite 𝜙 0, 𝑉ctr (𝑘𝑞 ), Ite 𝜙 1, 𝑉ctr (𝑘𝑞 ), 𝑉init 𝜋0 𝜋1 𝑃ctr (𝑘𝑞 ) ≜ Ite 𝜙 0, 𝑃 ctr (𝑘𝑞 ), Ite 𝜙 1, 𝑃 ctr (𝑘𝑞 ), 𝑃 init . Per Definition 3.4, mapctr ® 𝑘𝑞 ) = 𝑃ctr (𝑘𝑞 ), 𝑉ctr (𝑘𝑞 ) , with depenP (𝑥, dence on 𝑥® carried implicitly through 𝜙 0 (𝑥), ® 𝜙 1 (𝑥). ® Return-value output. Both paths return zero, so the output predicate from Definition 3.3 is out P (𝑥) ® ≜ 𝜙0 ∧ R = 0 ∨ 𝜙1 ∧ R = 0 . Since 𝜙 0 ∨ 𝜙 1 = true, this simplifies to R = 0. Equivalence check. Given the Rust translation’s analogous ITE 𝑅 (𝑘 ) and 𝑃 𝑅 (𝑘 ), and its return output R 𝑅 , the solver chains 𝑉ctr 𝑞 ctr 𝑞 checks satisfiability of the negated equivalence (Equation (6)) for the single map counters:
Symbolic execution output. Our angr-based engine explores two paths, corresponding to the map lookup returning a hit or a miss. Let 𝑝 = input_pid_tgid denote the symbolic 64-bit value from bpf_get_current_pid_tgid(), 𝑒 0 = key_exists_counters_v0 the symbolic 1-bit existence condition for map slot 0 prior to execution, and 𝑣 0 = init_map_counters_v0 the symbolic initial value at that slot. The lookup key is 𝑘 = zext64 (𝑝 [63:32]), i.e., the upper 32 bits of 𝑝 zero-extended to 64 bits. We write 𝑣 init and 𝑝 init for the shared initial value/presence arrays of the counters map. Each path performs exactly one write at key 𝑘 (write_seq = 1) with post-state existence bit 𝑒 1 = 1 (no path deletes).
𝐶 𝑅 𝐶 𝑅 ∃ 𝑝, 𝑒 0, 𝑣 0, 𝑘𝑞 : R𝐶 ≠ R 𝑅 ∨ 𝑉ctr (𝑘𝑞 ) ≠ 𝑉ctr (𝑘𝑞 ) ∨ 𝑃ctr (𝑘𝑞 ) ≠ 𝑃ctr (𝑘𝑞 ).
If UNSAT, the programs are equivalent for all inputs and all query keys. If SAT, the model assigns concrete values to 𝑝, 𝑒 0 , 𝑣 0 , 𝑘𝑞 that witness a divergence in either the value or presence chain.
D
Static Analysis Safety Engine
The safety engine is a pattern-based static analyzer that scans the LLM-produced Rust code for unsafe constructs that silently corrupt verifier-passing translations. Each rule is a string match, regex, or cross-pattern check; a hit rejects the translation from the safety stage and emits a structured violation (rule name, message, source
Conference’17, July 2017, Washington, DC, USA
Dasu et. al
s y nc :: a t o m ic :: A t o m i c U* :: f r o m \ _ p t r(p t r ) . f e t c h \ _ a d d(. . , O r d e r i n g :: R e l a x e d) on a valid *mut obtained via HashMap::get_ptr_mut(&k) or core::ptr::addr_of_mut!(STATIC). We forbid the (1) No mem::transmute for helper invocation. Casting raw helper IDs through transmute bypasses Aya’s typed wrapequivalent hand-rolled escape via core::arch::asm!, the pers and re-introduces C-level ABI risk on every helper call. feature(asm_experimental_arch) flag that enables it, (2) No hand-rolled unsafe extern "C" fn helper trampoand #[allow(invalid_reference_casting)] silencers lines. Equivalent escape: declaring a private extern binding used to feed inline asm a &T cast as *mut T, since these for a helper. It carries the same ABI/signature risk as transbypass Aya’s safe-API surface and the compiler’s aliasing mute and side-steps Aya’s safe surface. rules. (3) No direct calls to aya_ebpf::helpers::generated::*. (11) No folding of get_stackid’s Err arm into the successTranslations must use the typed safe wrappers typed slot. On StackTrace::get_stackid sites, an Err (bpf_probe_read_kernel<T>, bpf_probe_read_user_str_bytes, arm that writes the error code back into the 4-byte i32/u32 RingBuf::reserve, etc.) so that bounds, alignment, and struct field used as a HashMap key (Err(e) => e, Err(e) => e as i32, or .unwrap_or_else(|e| e)) preserves the Result handling stay uniform across the translation. (4) Helper Results must be handled. We do not allow translaC-side spurious-key-on-helper-failure bug bit-for-bit at the tions to discard a failable helper’s Result via let _ = ... or bytecode level. Prescribed shapes are an early-return on the .ok(). The translation must branch on Ok/Err or propagate Err arm, ?-propagation, or any pattern that does not feed with ?. the error code into the success-typed slot. (5) Ringbuf entries must be zero-initialized before submit. A program that passes the kernel verifier but violates any of RingBuf::reserve returns memory containing whatever these rules is still rejected. was last written to that slot. Submitting without an intervening write_bytes(0) or full structured initialization leaks stale kernel-stack bytes to userspace. (6) No non-atomic raw-pointer field writes into HashMap entries. We require value mutations on HashMap-family maps to go through get(&k) → stack copy → mutate → insert(&k, ©, 0). Atomic RMW via AtomicU*::from_ptr(get_ptr_mut(&k)).fetch_add(.., Relaxed) is allowed when atomicity is required. Aya’s API permits non-atomic get_ptr_mut(&k) plus unsafe { (*p).field = . . . } and pushes concurrency reasoning onto the caller. We forbid that form because it silently re-creates C’s data-race semantics on per-CPU maps and breaks the lookup-then-mutate invariant the verifier relies on. (7) No read_volatile loads from immutable global statics. Aya already provides Global<T>::load() for loader-initialized globals. Falling back to raw read_volatile loses the load barrier and the type-checked Aya surface. (8) No read-only static mut accessed via read_volatile. A static mut that is never written to is by definition immutable. A volatile read on it almost always indicates a missing loader-initialized binding that should have been a regular Global<T> (rule 7). (9) No untyped ringbuf reservations. Reserving a ringbuf entry as a byte array (RingBuf::reserve::<[u8; N]>(0) or declaring RingBufEntry<[u8; N]>) forces the translation to populate the slot via raw-pointer arithmetic, which replicates the C-style partial-init bug class that rule 5 is designed to close. Reservations must be typed: define a #[repr(C)] struct with named fields and reserve as EVENTS.reserve::<MyEvent>(0) so the type system enforces field-level initialization. (10) No inline-assembly atomic bypass. Atomic updates on map values or BSS globals must use c o re ::
span) that is fed back to the LLM (deterministic) or the agent (agentic) for repair. We enforce the following policies.