[2605.25411] Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
-->
Computer Science > Cryptography and Security
arXiv:2605.25411 (cs)
[Submitted on 25 May 2026]
Title:Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Authors:Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari, Gang Tan<br>View a PDF of the paper titled Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust, by Vishnu Asutosh Dasu and 5 other authors
View PDF<br>HTML (experimental)
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.
Subjects:
Cryptography and Security (cs.CR); Symbolic Computation (cs.SC)
Cite as:<br>arXiv:2605.25411 [cs.CR]
(or<br>arXiv:2605.25411v1 [cs.CR] for this version)
https://doi.org/10.48550/arXiv.2605.25411
Focus to learn more
arXiv-issued DOI via DataCite (pending registration)
Submission history<br>From: Vishnu Dasu [view email]<br>[v1]<br>Mon, 25 May 2026 04:23:29 UTC (488 KB)
Full-text links:<br>Access Paper:
View a PDF of the paper titled Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust, by Vishnu Asutosh Dasu and 5 other authors<br>View PDF<br>HTML (experimental)<br>TeX Source
view license
Current browse context:
cs.CR
next >
new<br>recent<br>| 2026-05
Change to browse by:
cs<br>cs.SC
References & Citations
NASA ADS<br>Google Scholar
Semantic Scholar
export BibTeX citation<br>Loading...
BibTeX formatted citation
×
loading...
Data provided by:
Bookmark
Bibliographic Tools
Bibliographic and Citation Tools
Bibliographic Explorer Toggle
Bibliographic Explorer (What is the Explorer?)
Connected Papers Toggle
Connected Papers (What is Connected Papers?)
Litmaps Toggle
Litmaps (What is Litmaps?)
scite.ai Toggle
scite Smart Citations (What are Smart Citations?)
Code, Data, Media
Code, Data and Media Associated with this Article
alphaXiv Toggle
alphaXiv (What is alphaXiv?)
Links to Code Toggle
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub Toggle
DagsHub (What is DagsHub?)
GotitPub Toggle
Gotit.pub (What is GotitPub?)
Huggingface Toggle
Hugging Face (What is Huggingface?)
ScienceCast Toggle
ScienceCast (What is ScienceCast?)
Demos
Demos
Replicate Toggle
Replicate (What is Replicate?)
Spaces Toggle
Hugging Face Spaces (What is Spaces?)
Spaces Toggle
TXYZ.AI (What is TXYZ.AI?)
Related Papers
Recommenders and Search Tools
Link to Influence Flower
Influence Flower (What are Influence Flowers?)
Core recommender toggle
CORE Recommender (What is CORE?)
Author
Venue
Institution
Topic
About arXivLabs
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs .
Which authors of this paper are endorsers? |<br>Disable MathJax (What is MathJax?)