pith. sign in

arxiv: 2605.25411 · v1 · pith:ASSV3SB2new · submitted 2026-05-25 · 💻 cs.CR · cs.SC

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

Vishnu Asutosh Dasu , Monika Santra , Md Rafi Ur Rashid , Ashish Kumar , Saeid Tizpaz-Niari , Gang Tan This is my paper

Pith reviewed 2026-06-29 21:59 UTC · model grok-4.3

classification 💻 cs.CR cs.SC
keywords eBPFprogram migrationRustformal verificationsymbolic executionmemory safetykernel securityLLM code translation
0
0 comments X

The pith

Heimdall translates legacy eBPF programs from C to Rust and formally proves equivalence for 94 percent of cases.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

eBPF programs run inside the Linux kernel for networking and security tasks, but many contain source-level bugs that pass the kernel verifier yet cause data corruption, leaks, or wrong enforcement. The paper documents six bug classes and finds concrete information leaks in ten open-source programs that expose prior events and even KASLR offsets. Heimdall automates migration of libbpf C code to Aya Rust by using large language models for initial translation, iteratively repairing compilation and verifier errors, blocking unsafe Rust patterns with static analysis, and confirming per-program behavioral equivalence through symbolic execution and Z3 checks. It achieves 96 proven-equivalent translations out of 102 programs. A sympathetic reader cares because the result shows a practical path to replace verifier-accepted but unsafe eBPF code with memory-safe equivalents while retaining the original observable effects.

Core claim

Heimdall is the first automated pipeline that converts production libbpf C eBPF programs to Aya Rust. It applies iterative LLM-based repair to resolve compilation and kernel-verifier failures, uses a static analysis safety engine to reject unsafe escape hatches, and establishes behavioral equivalence for each program via symbolic execution followed by Z3-based checking. Across 102 programs the system yields 96 formally proven-equivalent translations, preserving observable behavior.

What carries the argument

Iterative LLM repair combined with static safety analysis and symbolic execution plus Z3 equivalence checking that together enforce both compile-time and semantic equivalence per program.

If this is right

  • Production eBPF programs that currently leak data or corrupt state can be replaced by memory-safe Rust versions with per-program proof that observable behavior is unchanged.
  • The same migration pipeline can be applied to additional eBPF programs without manual rewriting.
  • Kernel developers gain a way to harden existing verifier-accepted code while keeping the same enforcement and tracing results.
  • Future eBPF development can target Rust directly with automated back-translation paths that carry formal guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The identified leaks indicate that stronger source-level checks could be added to the eBPF verifier itself to catch ring-buffer and stack-record issues before they reach userspace.
  • The same LLM-plus-formal-verification pattern might extend to migrating other low-level kernel-adjacent code written in C to safer languages.
  • If the repair convergence rate remains high on larger or more complex programs, the method could reduce the practical cost of adopting memory-safe languages inside the kernel ecosystem.
  • Testable extension: run the pipeline on the full set of programs in a public eBPF repository and measure the fraction that reach proven equivalence without manual intervention.

Load-bearing premise

The LLM repair loop will reliably reach compilable, verifier-passing translations and the symbolic execution plus Z3 checks will correctly detect any semantic differences introduced by the translation.

What would settle it

An eBPF program for which Heimdall outputs a translation that compiles and passes the verifier, yet on some input the Rust version produces different observable output than the original C version.

Figures

Figures reproduced from arXiv: 2605.25411 by Ashish Kumar, Gang Tan, Md Rafi Ur Rashid, Monika Santra, Saeid Tizpaz-Niari, Vishnu Asutosh Dasu.

Figure 1
Figure 1. Figure 1: Heimdall’s five-stage pipeline with retry loops. Orange boxes are LLM-driven steps and blue boxes are deter￾ministic 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… view at source ↗
Figure 2
Figure 2. Figure 2: Our eBPF support in angr. Five numbered hooks pair [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Tool-call distribution across the 96-program ver1 [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Purpose distribution of 68 subagent invocations 1 [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: End-to-end trace of two eBPF instructions through [PITH_FULL_IMAGE:figures/full_fig_p017_5.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper documents six classes of source-level bugs in verifier-accepted eBPF programs (including previously unreported information leaks in 10 open-source programs) and presents Heimdall, an LLM-driven pipeline that translates libbpf C programs to Aya Rust. The pipeline performs iterative repair for compilation and kernel-verifier failures, applies static analysis to reject unsafe Rust escape hatches, and uses symbolic execution plus Z3 to prove per-program equivalence to the original on observable behavior. Evaluation on 102 programs yields 96 formally proven-equivalent translations (94.1%), positioning Heimdall as the first automated system providing per-program formal guarantees for memory-safe migration of production eBPF programs.

Significance. If the pipeline's equivalence proofs and safety checks hold, the result is significant: it supplies the first automated, formally grounded migration path from legacy eBPF C to Rust while directly addressing real, verifier-passing bugs that can cause data corruption or leaks. The empirical scale (102 programs), the explicit focus on observable-behavior preservation rather than full semantics, and the combination of LLM repair with external symbolic verification constitute concrete strengths that advance practical hardening of kernel extensions.

major comments (1)
  1. [equivalence checking pipeline] The equivalence-checking pipeline (described after the repair loop): the claim of 'formally proven-equivalent' translations rests on the completeness of the eBPF semantics model used for symbolic execution; any unmodeled side effects or verifier-accepted but non-deterministic behaviors could allow semantic differences to pass the Z3 check undetected, directly affecting the 94.1% success rate.
minor comments (2)
  1. [evaluation] Clarify in the evaluation section how many of the 6 bug classes were actually present in the 102-program corpus and whether any of the 6 failures were due to those bugs rather than translation issues.
  2. [static analysis safety engine] The static-analysis safety engine description should include the precise set of disallowed Rust constructs and the soundness argument for why they suffice to prevent the documented source-level bugs.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed and constructive feedback. The single major comment is addressed point-by-point below. We believe a minor revision incorporating additional clarification on the scope of the equivalence model will strengthen the manuscript.

read point-by-point responses

  1. Referee: [equivalence checking pipeline] The equivalence-checking pipeline (described after the repair loop): the claim of 'formally proven-equivalent' translations rests on the completeness of the eBPF semantics model used for symbolic execution; any unmodeled side effects or verifier-accepted but non-deterministic behaviors could allow semantic differences to pass the Z3 check undetected, directly affecting the 94.1% success rate.

    Authors: We agree that the strength of the 'formally proven-equivalent' claim depends on the modeled semantics. The paper explicitly qualifies the guarantees as equivalence on observable behavior (see abstract and the equivalence-checking section), not full semantic equivalence. The symbolic execution model encodes the observable effects on maps, ring buffers, perf events, and return values—the channels through which eBPF programs interact with userspace and the rest of the kernel. Internal non-determinism or side effects that do not manifest through these observables are intentionally excluded from the model, as they fall outside the stated goal of preserving observable functionality. Any semantic difference confined to unmodeled behavior would not contradict the reported 94.1% figure. To prevent misinterpretation, we will insert a short paragraph in the revised manuscript that (1) restates the observable-behavior scope, (2) enumerates the modeled observables, and (3) notes that the approach does not claim to detect differences in unmodeled internal state. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's derivation consists of an empirical pipeline (LLM translation + iterative repair + static safety checks + per-program symbolic execution + Z3 equivalence) evaluated on 102 external programs, with the 94.1% success rate and formal guarantees resting on independent verification tools rather than any self-referential definition, fitted parameter renamed as prediction, or load-bearing self-citation. No equation or claim reduces to its own inputs by construction; the equivalence checks are external and falsifiable against the original C sources.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the correctness of LLM repair convergence, the soundness of the static analysis safety engine for Aya Rust, and the adequacy of symbolic execution plus Z3 for capturing observable eBPF behavior.

axioms (2)
  • standard math Symbolic execution combined with Z3 correctly decides behavioral equivalence between the original C eBPF program and its Rust translation for the observable outputs considered.
    This underpins the formal guarantees reported for the 96 successful translations.
  • domain assumption The static analysis safety engine accurately identifies and rejects all unsafe escape hatches that would violate memory safety in the generated Aya Rust code.
    Required to ensure the translated programs remain memory-safe after LLM generation.

pith-pipeline@v0.9.1-grok · 5832 in / 1497 out tokens · 45753 ms · 2026-06-29T21:59:31.270758+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

67 extracted references · 30 canonical work pages · 5 internal anchors

  1. [1]

    Can’t read in struct fields even with bpf_probe_read: -EFAULT

    2016. Can’t read in struct fields even with bpf_probe_read: -EFAULT. https: //github.com/iovisor/bcc/issues/622

    2016

  2. [2]

    invalid indirect read from stack with uninitialized struct

    2017. invalid indirect read from stack with uninitialized struct. https: //github.com/iovisor/bcc/issues/919

    2017

  3. [3]

    bpf_probe_read() returned-14

    2019. bpf_probe_read() returned-14. https://github.com/iovisor/bcc/issues/ 2245

    2019

  4. [4]

    invalid indirect read from stack off -16+4 size 16when tracing spinlocks

    2019. invalid indirect read from stack off -16+4 size 16when tracing spinlocks. https://github.com/iovisor/bcc/issues/2623

    2019

  5. [5]

    bpf_probe_read_user returns error (−14) and opensnoop emits empty filenames

    2020. bpf_probe_read_user returns error (−14) and opensnoop emits empty filenames. https://github.com/iovisor/bcc/issues/3175

    2020

  6. [6]

    Tetragon does not raise an event when the resolved value is null

    2025. Tetragon does not raise an event when the resolved value is null. https: //github.com/cilium/tetragon/issues/3728

    2025

  7. [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

    2018

  8. [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. In2013 Formal Methods in Computer-Aided Design. IEEE, 1–8

    2013

  9. [9]

    BCC Contributors. 2024. libbpf-tools: BPF CO-RE Tools. https://github.com/iov isor/bcc/tree/master/libbpf-tools

    2024

  10. [10]

    Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. InProceedings of the 8th USENIX Conference on Operating Systems Design and Implementation(San Diego, California)(OSDI’08). USENIX Association, USA, 209–224

    2008

  11. [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

    work page arXiv 2025

  12. [12]

    daeuniverse. 2023. dae: A Linux High-Performance Transparent Proxy Based on eBPF. https://github.com/daeuniverse/dae

    2023

  13. [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

    2008

  14. [14]

    Kumar Kartikeya Dwivedi, Rishabh Iyer, and Sanidhya Kashyap. 2024. Fast, Flexible, and Practical Kernel Extensions. InProceedings 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

    work page arXiv 2024

  15. [15]

    eBPF Foundation. 2024. eBPF: Extended Berkeley Packet Filter. https://ebpf.io/

    2024

  16. [16]

    Mehmet Emre, Ryan Schroeder, Kyle Dewey, and Ben Hardekopf. 2021. Trans- lating C to safer Rust.Proc. ACM Program. Lang.5, OOPSLA, Article 121 (Oct. 2021), 29 pages. doi:10.1145/3485498

    work page doi:10.1145/3485498 2021

  17. [17]

    Hasan Ferit Eniser, Hanliang Zhang, Cristina David, Meng Wang, Maria Chris- takis, 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

    work page arXiv 2024

  18. [18]

    Muhammad Farrukh, Smeet Shah, Baris Coskun, and Michalis Polychron- akis. 2025. SafeTrans: LLM-assisted Transpilation from C to Rust. arXiv:2505.10708 [cs.CR] https://arxiv.org/abs/2505.10708

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  19. [19]

    Galois. 2018. C2Rust. https://galois.com/blog/2018/08/c2rust/

    2018

  20. [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

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  21. [21]

    Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv

    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. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (Phoenix, AZ, USA)(PLDI 2019). Association for Computi...

    work page doi:10.1145/3314221.3314590 2019

  22. [22]

    Yoann Ghigoff, Julien Sopena, Kahina Lazri, Antoine Blin, and Gilles Muller

  23. [23]

    In18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)

    BMC: Accelerating Memcached using Safe In-kernel Caching and Pre- stack Processing. In18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 487–501. https://www.usenix.o rg/conference/nsdi21/presentation/ghigoff

  24. [24]

    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. InProceedings of the 14th International Conference on Emerging Networking EX- periments and Technologies(Heraklion, Greece)(CoNEXT ’18)...

    work page doi:10.1145/3281411.3281443 2018

  25. [25]

    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

    work page arXiv 2023

  26. [26]

    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

    work page arXiv 2024

  27. [27]

    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

    work page arXiv 2025

  28. [28]

    Kaiming Huang, Mathias Payer, Zhiyun Qian, Jack Sampson, Gang Tan, and Trent Jaeger. 2025. SoK: Challenges and Paths Toward Memory Safety for eBPF. InProceedings of the 2025 IEEE Symposium on Security and Privacy (SP). IEEE, 848–866

    2025

  29. [29]

    Ali Reza Ibrahimzada, Brandon Paulsen, Daniel Kroening, and Reyhaneh Jab- barvand. 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

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  30. [30]

    IO Visor Project. 2024. BCC: Tools for BPF-based Linux IO Analysis, Networking, Monitoring, and More. https://github.com/iovisor/bcc

    2024

  31. [31]

    Rishabh Iyer, Katerina Argyraki, and George Candea. 2022. Performance Inter- faces for Network Functions. In19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Renton, WA, 567–584. https://www.usenix.org/conference/nsdi22/presentation/iyer

    2022

  32. [32]

    Susmit Jha and Sanjit A Seshia. 2017. A theory of formal synthesis via inductive learning.Acta Informatica54, 7 (2017), 693–726

    2017

  33. [33]

    Le, Hubertus Franke, Hani Jamjoom, Tianyin Xu, and Dan Williams

    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. InProceedings of the 2025 USENIX Conference on Usenix Annual Technical Conference(Boston, MA, USA)(USENIX ATC ’25). US...

    2025

  34. [34]

    SWE-bench: Can Language Models Resolve Real-World GitHub Issues?

    Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2024. SWE-bench: Can Language Models Resolve Real- World GitHub Issues? arXiv:2310.06770 [cs.CL] https://arxiv.org/abs/2310.06770

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  35. [35]

    Marios Kogias, Rishabh Iyer, and Edouard Bugnion. 2020. Bypassing the Load Balancer Without Regrets. InProceedings of the 11th ACM Symposium on Cloud Computing(Virtual Event, USA)(SoCC ’20). Association for Computing Machin- ery, New York, NY, USA, 193–207. doi:10.1145/3419111.3421304

    work page doi:10.1145/3419111.3421304 2020

  36. [36]

    libbpf Contributors. 2024. libbpf-bootstrap: Scaffolding for BPF CO-RE applica- tions. https://github.com/libbpf/libbpf-bootstrap

    2024

  37. [37]

    Hongyi Lu, Shuai Wang, Yechang Wu, Wanning He, and Fengwei Zhang. 2024. MOAT: Towards Safe BPF Kernel Extension. In33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 1153–1170. https: //www.usenix.org/conference/usenixsecurity24/presentation/lu-hongyi

    2024

  38. [38]

    Tao Lyu, Kumar Kartikeya Dwivedi, Thomas Bourgeat, Mathias Payer, Meng Xu, and Sanidhya Kashyap. 2025. eBPF Misbehavior Detection: Fuzzing with a Specification-Based Oracle. InProceedings 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, ...

    work page doi:10.1145/3731569.3764797 2025

  39. [39]

    John McCarthy. 1993. Towards a mathematical science of computation. In Program verification: Fundamental issues in computer science. Springer, 35–56

    1993

  40. [40]

    Terminal-Bench: Benchmarking Agents on Hard, Realistic Tasks in Command Line Interfaces

    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 Dasu et. al Junhong Shen, Guanghao Ye, Haowei Lin, Jason Poulos, Maoyu Wang, Mari- anna Nezhurina, Jenia Jitsev, Di Lu, Orfeas Menis Mastromichalakis, Zhiwei X...

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  41. [41]

    Samuel Miserendino, Michele Wang, Tejal Patwardhan, and Johannes Heidecke

  42. [42]

    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

    work page arXiv

  43. [43]

    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. InProceedings 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...

    work page doi:10.1145/3341301.3359641 2019

  44. [44]

    Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specifi- cation and verification in the field: Applying formal methods to BPF just-in- time compilers in the Linux kernel. In14th USENIX Symposium on Operat- ing Systems Design and Implementation (OSDI 20). USENIX Association, 41–61. https://www.usenix.org/conference/osdi20/presentation/nelson

    2020

  45. [45]

    Network Security Group, ETH Zürich. 2023. Hercules: High-Speed Bulk Data Transfer Using XDP. https://github.com/netsec-ethz/hercules

    2023

  46. [46]

    Vikram Nitin, Rahul Krishna, Luiz Lemos do Valle, and Baishakhi Ray. 2025. C2SaferRust: Transforming C Projects into Safer Rust with NeuroSymbolic Tech- niques. arXiv:2501.14257 [cs.SE] https://arxiv.org/abs/2501.14257

    work page arXiv 2025

  47. [47]

    NTT Communications. 2023. Fluvia: IPFIX Exporter Using XDP. https://github.c om/nttcom/fluvia

    2023

  48. [48]

    Open Information Security Foundation. 2024. Suricata: Open Source IDS/IPS/NSM Engine. https://suricata.io/

    2024

  49. [49]

    Chaoyuan Peng, Muhui Jiang, Lei Wu, and Yajin Zhou. 2024. Toss a Fault to BpfChecker: Revealing Implementation Flaws for eBPF runtimes with Differential Fuzzing. InProceedings 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. do...

    work page doi:10.1145/3658644.36 2024

  50. [50]

    Polar Signals. 2024. Parca Agent: eBPF-based Always-On Continuous Profiler. https://github.com/parca-dev/parca-agent

    2024

  51. [51]

    Seshia, and Koushik Sen

    Manish Shetty, Naman Jain, Adwait Godbole, Sanjit A. Seshia, and Koushik Sen

  52. [52]

    arXiv:2412.14234 [cs.SE] https://arxiv.org/abs/2412.14234

    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

    work page arXiv

  53. [53]

    Momoko Shiraishi, Yinzhi Cao, and Takahiro Shinagawa. 2026. SmartC2Rust: Iterative, Feedback-Driven C-to-Rust Translation via Large Language Models for Safety and Equivalence

    2026

  54. [54]

    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. In2016 IEEE Symposium on Security and Privacy (SP). 138–157. doi:10.1109/SP.2016.17

    work page doi:10.1109/sp.2016.17 2016

  55. [55]

    Armando Solar-Lezama. 2013. Program sketching.International Journal on Software Tools for Technology Transfer15, 5 (2013), 475–495

    2013

  56. [56]

    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. In14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association,...

    2020

  57. [57]

    Hao Sun and Zhendong Su. 2024. Validating the eBPF Verifier via State Embedding. InProceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, 615–628

    2024

  58. [58]

    Hao Sun and Zhendong Su. 2025. Approximation Enforced Execution of Untrusted Linux Kernel Extensions. In34th USENIX Security Symposium (USENIX Security 25). USENIX Association, Seattle, WA, 7467–7485. https://www.usenix.org/con ference/usenixsecurity25/presentation/sun-hao

    2025

  59. [59]

    Hao Sun and Zhendong Su. 2025. Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction Refinement. InProceedings 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

    work page doi:10.1145/3731569.3764796 2025

  60. [60]

    Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2023. Verifying the Verifier: eBPF Range Analysis Verification. InComputer Aided Verification: 35th International Conference, CA V 2023, Paris, France, July 17–22, 2023, Proceedings, Part III(Paris, France). Springer-Verlag, Berlin, Heidelberg, 226–251. doi:10.1007/978-3...

    work page doi:10.1007/978-3-031-37709-9_12 2023

  61. [61]

    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

    work page arXiv 2025

  62. [62]

    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. In22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25). USENIX Association, Philadelphia, PA, 277–299. https://www.usenix.org/conference/nsdi25/pr...

    2025

  63. [63]

    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

    work page arXiv 2024

  64. [64]

    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

    work page arXiv 2023

  65. [66]

    Yusheng Zheng, Yiwei Yang, Maolin Chen, and Andrew Quinn. 2024. Kgent: Kernel Extensions Large Language Model Agent. InProceedings 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

    work page doi:10.1145/3672197.3673434 2024

  66. [67]

    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

    work page arXiv 2025

  67. [68]

    vmlinux.h

    Tal Zussman, Ioannis Zarkadas, Jeremy Carin, Andrew Cheng, Hubertus Franke, Jonas Pfefferle, and Asaf Cidon. 2025. cache_ext: Customizing the Page Cache with eBPF. InProceedings of the ACM SIGOPS 31st Symposium on Operat- ing Systems Principles(Lotte Hotel World, Seoul, Republic of Korea)(SOSP ’25). Association for Computing Machinery, New York, NY, USA, ...

    work page doi:10.1145/3731569.3764820 2025