Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust

• URL: http://arxiv.org/abs/2605.25411v1
• Date: Mon, 25 May 2026 04:23:29 GMT
• Title: Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
• Abstract summary: Extended Berkeley Packet Filter (eBPF) programs are kernel extensions used for networking, observability, and security enforcement in the Linux kernel.<n>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.<n>We present Heimdall, an automated pipeline that uses large language models to translate legacy libbpf C programs to Aya Rust.
• Score: 14.478602770508523
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• HazardAuditor: From Executable Threats to Safer Computer-Use Agents [50.06351661912873]
  Existing guard models target static prompts and responses.<n>Existing safety platforms produce evaluation verdicts rather than the normalized supervision a guard model needs to learn.<n>We introduce HazardAuditor, an execution-grounded framework that closes both gaps.
  arXiv  Detail & Related papers  (2026-09-14T07:09:33Z)
• FRESCO: Complete and Scalable Temporal Safety for CHERI Application Processors [18.51942378693278]
  CHERI provides hardware-enforced memory safety.<n>While prior work extends it with heap temporal safety, stack use-after-return remains unaddressed.<n>We present FRESCO, built on the principle that a stack capability must not outlive the frame that created it.
  arXiv  Detail & Related papers  (2026-08-26T19:36:30Z)
• From C to Idiomatic Rust: A Ship-of-Theseus Agentic Translation [0.13537117504260618]
  C underpins operating systems, embedded platforms, and network infrastructure because its abstractions map directly to machine behaviour.<n> Rust eliminates most of failure modes through a static ownership and borrowing model that enforces memory safety and aliasing constraints at compile time.<n>This paper presents a migration methodology that first generates a semantics-preserving, non-idiomatic Rust baseline and then incrementally rewrites it into idiomatic Rust using agentic AI.
  arXiv  Detail & Related papers  (2026-07-30T21:00:27Z)
• MemEvoBench: Benchmarking Memory MisEvolution in LLM Agents [78.95081012334116]
  Large Language Models (LLMs) with persistent memory enhances interaction continuity and personalization but introduces new safety risks.<n> contaminated or biased memory accumulation can trigger abnormal agent behaviors.<n>MemeEvoBench is the first benchmark evaluating memory safety in LLM agents against adversarial memory injection, noisy tool outputs, and biased feedback.
  arXiv  Detail & Related papers  (2026-04-17T07:29:52Z)
• ENCRUST: Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-Rust Translation [5.10072982044534]
  We present Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-construct Translation.<n>We present a two-phase pipeline for translating real-world C projects to safe Rust.<n>Phase 1 (Encapsulated Substitution) translates each function using an ABIutil wrapper that splits it into two components.<n>Phase 2 (Agentic Refinement) resolves unsafe constructs beyond per-function scope.
  arXiv  Detail & Related papers  (2026-04-06T08:46:14Z)
• SafeSeek: Universal Attribution of Safety Circuits in Language Models [49.59795225914787]
  We propose ourmethod, a unified safety interpretability framework.<n>Our method identifies functionally complete safety circuits in Large Language Models.<n>We validate ourmethod in two key scenarios in LLM safety.
  arXiv  Detail & Related papers  (2026-03-24T14:32:53Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBench is an evaluation framework for self-evolving benchmarks that scrapes and evaluates agents on freshly discovered kernel bugs.<n> kEnv is an agent-agnostic crash-resolution environment for kernel compilation, execution, and feedback.<n>Using kEnv, we benchmark three state-of-the-art agents, showing that they resolve 74% of crashes on the first attempt.
  arXiv  Detail & Related papers  (2026-02-02T19:06:15Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases.<n>We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem.<n>The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages.<n>This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• VeriFence: Lightweight and Precise Spectre Defenses for Untrusted Linux Kernel Extensions [0.07696728525672149]
  Linux's extended Berkeley Packet Filter (BPF) avoids user-/ kernel transitions by just-in-time compiling user-provided bytecode.<n>To mitigate the Spectre vulnerabilities disclosed in 2018, defenses which reject potentially-dangerous programs had to be deployed.<n>We propose VeriFence, an enhancement to the kernel's Spectre defenses that reduces the number of BPF application programs rejected from 54% to zero.
  arXiv  Detail & Related papers  (2024-04-30T12:34:23Z)
• MOAT: Towards Safe BPF Kernel Extension [10.303142268182116]
  The Linux kernel extensively uses the Berkeley Packet Filter (BPF) to allow user-written BPF applications to execute in the kernel space. Recent attacks show that BPF programs can evade security checks and gain unauthorized access to kernel memory. We present MOAT, a system that isolates potentially malicious BPF programs using Intel Memory Protection Keys (MPK)
  arXiv  Detail & Related papers  (2023-01-31T05:31:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.