cs.CRcs.SC
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
May 25, 2026
The paper introduces Heimdall, an automated pipeline that uses LLMs and formal verification to safely and automatically migrate legacy, potentially buggy eBPF programs written in C to memory-safe Rust, achieving high rates of formally proven-equivalent translations.
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.
Finding Memory Leaks in C/C++ Programs via Neuro-Symbolic Augmented Static Analysis
MemHint is a neuro-symbolic static analysis pipeline that significantly improves…
Architecture-Derived CBOMs for Cryptographic Migration: A Security-Aware Architecture Tradeoff Metho…
The paper introduces SATAM, a novel method that derives context-rich Cryptograph…
VCAO: Verifier-Centered Agentic Orchestration for Strategic OS Vulnerability Discovery
The paper introduces VCAO, a novel verifier-centered agentic orchestration frame…
SPARK: Secure Predictive Autoscaling for Robust Kubernetes
SPARK introduces a predictive, traffic-aware autoscaling toolchain for Kubernete…
Triggering and Detecting Exploitable Library Vulnerability from the Client by Directed Greybox Fuzzi…
The paper proposes LiveFuzz, a directed greybox fuzzing technique that detects t…
The Verifier Tax: Horizon Dependent Safety Success Tradeoffs in Tool Using LLM Agents
The paper analyzes how runtime safety enforcement impacts the performance of mul…
Enabling Deterministic User-Level Interrupts in Real-Time Processors via Hardware Extension
The paper proposes a novel hardware extension that enables deterministic, kernel…
The Art of Building Verifiers for Computer Use Agents
The paper introduces the Universal Verifier, a robust system for verifying compu…