pith. sign in

arxiv: 2606.24213 · v1 · pith:4ZALDILEnew · submitted 2026-06-23 · 💻 cs.OS · cs.CR

Kops: Safely Extending the eBPF Compilation Pipeline with Native Operations

Yusheng Zheng , Zhengjie Ji , Weichen Tao , Hao Sun , Wei Zhang , Dan Williams , Andi Quinn This is my paper

Pith reviewed 2026-06-25 21:53 UTC · model grok-4.3

classification 💻 cs.OS cs.CR
keywords eBPFJIT compilationkernel extensionsverified compilationtrusted computing basenative operationsperformance optimization
0
0 comments X

The pith

Kops lets userspace and kernel modules add native machine operations to eBPF by pairing each with a verifier-checked proof sequence of standard instructions.

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

The paper establishes that the eBPF JIT can be extended with optimized native code without modifying the kernel core, enlarging its trusted computing base, or lengthening release cycles. Each added operation is defined in two forms: a sequence of ordinary eBPF instructions that the existing verifier can check for safety, and a corresponding native emit that the JIT executes directly. Because verification happens on the proof sequence, only the native emit enters the trusted computing base. Lean 4 proofs confirm semantic equivalence for each pair. The result is concrete speedups on x86-64 and ARM64 while preserving the safety model that makes eBPF usable in the kernel.

Core claim

Kops supplies an extension interface in which every new operation consists of a proof sequence of vanilla eBPF instructions together with a native emit. The verifier checks the proof sequence in the usual way; the JIT emits the native code. Lean 4 proofs establish that each native emit computes the identical result as its proof sequence. Seven such operations (EInsn) covering rotates, conditional select, and similar hardware idioms are demonstrated, along with support for whole-program native replacement.

What carries the argument

The dual-form operation consisting of a proof sequence of vanilla eBPF instructions and a matching native emit, with the proof sequence serving as the sole safety anchor checked by the existing verifier.

If this is right

  • EInsn operations deliver up to 24% speedup on microbenchmarks and up to 12% on production applications on x86-64 and ARM64.
  • The same interface supports whole-program native replacement, reaching 2.358x speedup at the cost of a larger TCB.
  • Hardware idioms become the lowest-effort targets for the interface because they map directly to single machine instructions.
  • New operations can be introduced by userspace compilers or kernel modules without upstream kernel changes.

Where Pith is reading between the lines

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

  • The design could let domain-specific compilers emit eBPF programs that exploit architecture-specific idioms without waiting for kernel releases.
  • Similar dual-representation interfaces might apply to other verified bytecode systems that separate verification from code generation.
  • Over time the approach could shrink the measured gap between eBPF and natively compiled code while keeping the kernel's trusted surface small.

Load-bearing premise

The proof sequences must correctly capture the semantics of their paired native emits, and adding the interface must not create new verifier bypasses or attack surfaces.

What would settle it

An input on which the native emit produces a result different from the result of executing its corresponding proof sequence of eBPF instructions.

Figures

Figures reproduced from arXiv: 2606.24213 by Andi Quinn, Dan Williams, Hao Sun, Weichen Tao, Wei Zhang, Yusheng Zheng, Zhengjie Ji.

Figure 1
Figure 1. Figure 1: The eBPF execution pipeline. then lowers the result to bytecode restricted to the opera￾tions the instruction set defines. Optimization research also targets this stage, where compile-time optimizers such as Merlin [19], K2 [30], and EPSO [33] rewrite programs for speed and size. The optimizers all stay within the instruc￾tion set, a boundary the verifier enforces. The instruction set has no single-instruc… view at source ↗
Figure 2
Figure 2. Figure 2: Per-case speedup over the kernel eBPF JIT on the 27 pure-bytecode microbenchmarks, on x86-64 (top) and ARM64 (bottom). Each bar is one non-baseline path. The ARM64 paths come from separate runs, each over its own baseline. bytecode. The verified bytecode carries most of what a compiler needs to generate fast code. 3.4 C-RQ3: Which Operations Does the Kernel JIT Compile Poorly? The per-opcode kernel JIT com… view at source ↗
Figure 3
Figure 3. Figure 3: Compiling a 64-bit rotate with a variable shift. Di￾rect compilation to x86-64 emits a single ROL. Through eBPF the rotate becomes eight bytecode instructions, which the per-opcode kernel JIT translates separately into 15 machine instructions (Linux 6.1, x86-64) [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 6
Figure 6. Figure 6: Application-level EInsn policy probes. Workload throughput ratios are higher-is-better, while BPF cost ratios are lower-is-better. Cilium compares the full EInsn policy with the no-bulk policy; Katran compares a more-sites policy with the selected-family policy. The dashed line marks the stock eBPF baseline. 7.3 RQ3: Family-Selection Policy Sensitivity EInsn creates a policy surface above the Kops kernel m… view at source ↗
Figure 4
Figure 4. Figure 4: The original eBPF pipeline (orange) and the Kops pipeline (green). The original pipeline verifies and JIT-compiles the bytecode unchanged, producing under-optimized native code. With Kops, the compile-time recognizer rewrites supported operations into extended instructions, and the EInsn modules supply each operation’s proof sequence to the verifier and its native emit to the JIT, producing optimized nativ… view at source ↗
Figure 5
Figure 5. Figure 5: Microbenchmark execution-time speedup over the stock kernel eBPF JIT. Each benchmark is measured with three samples and INNER_REPEAT=100000; bars report speedup computed from median exec_ns, and higher is better. Panel (a) reports the x86-64 KVM EInsn-enabled run. Panel (b) reports the ARM64 AWS EInsn-enabled run over the 27 benchmarks with applied EInsn sites. Red lines mark the geomean speedup reported i… view at source ↗
read the original abstract

eBPF safely extends OS kernels in domains such as networking, observability, and security. The safety comes from an in-kernel compilation pipeline where a verifier checks every program, and a kernel just-in-time compiler (JIT) translates the verified bytecode to native code. The kernel keeps the JIT simple to stay trustworthy, translating one bytecode instruction at a time in a single pass. This single-pass design misses optimization opportunities, so eBPF runs up to twice as slow as natively compiled code in our characterization. Adding optimizations to the kernel JIT directly requires upstream acceptance and a long release cycle, enlarges the trusted computing base (TCB), and grows the per-architecture kernel code. To address this, we present Kops, an extension interface that lets userspace compilers and kernel modules introduce new operations without modifying the kernel core, while keeping a minimal trusted computing base (TCB). Each operation has two forms, a proof sequence of vanilla eBPF instructions that the existing verifier checks and a native emit of machine instructions that the JIT compiles. Because the verifier checks the proof sequence, the native emit is the only per-operation addition to the TCB. Hardware idioms are the lowest-hanging fruit for this interface. With Kops, we build EInsn, seven operations such as rotate and conditional select that CPUs execute as single instructions. Lean 4 proofs show that each native emit computes the same result as its proof sequence. On x86-64 and ARM64, EInsn speeds up eBPF microbenchmarks by up to 24% and production applications by up to 12%. The same interface also supports whole-program native replacement, reaching 2.358x at the cost of a larger TCB.

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

3 major / 2 minor

Summary. The paper introduces Kops, an extension interface for the eBPF kernel compilation pipeline. Each new operation is defined by a proof sequence of vanilla eBPF instructions (verified by the existing verifier) paired with a native emit of machine instructions. Only the emit enters the TCB. The authors implement EInsn (seven hardware-idiom operations such as rotate and conditional select), supply Lean 4 proofs of semantic equivalence between each proof sequence and its native emit, and report measured speedups of up to 24 % on microbenchmarks and 12 % on production applications on x86-64 and ARM64; whole-program native replacement reaches 2.358× at the cost of a larger TCB.

Significance. If the equivalence proofs and interface safety arguments hold, the work provides a principled way to add architecture-specific optimizations to eBPF without enlarging the kernel TCB or requiring upstream kernel changes. The combination of formal proofs, concrete performance numbers, and an explicit TCB analysis is a strength that could influence future kernel extensibility mechanisms.

major comments (3)
  1. [§3] §3 (Kops interface definition): the claim that the extension interface itself adds nothing to the TCB is load-bearing for the safety argument; the text must explicitly enumerate every new kernel entry point, data structure, and verifier hook introduced by Kops and show why none of them enlarges the trusted base beyond the per-operation emits.
  2. [§4.3] §4.3 (Lean 4 proofs): the equivalence statements are stated only for the seven EInsn operations; the paper must clarify whether the proof infrastructure is reusable for future operations or whether each new operation requires a fresh, manually written proof, because this directly affects the practicality of the “userspace compilers and kernel modules” claim.
  3. [§5] §5 (evaluation): the 24 % microbenchmark and 12 % application speedups are presented as direct consequences of EInsn; the text must state the exact baseline (vanilla JIT, no EInsn), the measurement methodology, and any data-exclusion rules so that readers can judge whether the reported ratios are robust.
minor comments (2)
  1. The abstract and §2 would benefit from a short table listing the seven EInsn operations together with the corresponding proof-sequence length and native instruction count.
  2. Figure captions in the evaluation section should explicitly state the number of runs and the error bars used.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the positive recommendation of minor revision and the detailed comments. We address each major comment below and will update the manuscript accordingly.

read point-by-point responses

  1. Referee: [§3] §3 (Kops interface definition): the claim that the extension interface itself adds nothing to the TCB is load-bearing for the safety argument; the text must explicitly enumerate every new kernel entry point, data structure, and verifier hook introduced by Kops and show why none of them enlarges the trusted base beyond the per-operation emits.

    Authors: We agree that an explicit enumeration is required to make the TCB argument fully rigorous. In the revised manuscript we will add a new subsection in §3 that lists every new kernel entry point (the Kops registration syscall and its handler), data structure (the operation descriptor table), and verifier hook (the proof-sequence validation path). We will show that none of these components executes or trusts native emit code; they merely register the emit and invoke the existing verifier on the proof sequence. Consequently the interface itself adds nothing to the TCB beyond the per-operation emits. revision: yes

  2. Referee: [§4.3] §4.3 (Lean 4 proofs): the equivalence statements are stated only for the seven EInsn operations; the paper must clarify whether the proof infrastructure is reusable for future operations or whether each new operation requires a fresh, manually written proof, because this directly affects the practicality of the “userspace compilers and kernel modules” claim.

    Authors: The current text presents the seven proofs as concrete instances but does not discuss reusability. We will revise §4.3 to state that the Lean 4 semantic model (eBPF instruction semantics and target-machine semantics) and the associated tactics are reusable across operations, while each new operation still requires its own equivalence theorem. This clarification will be added without altering the existing proofs. revision: yes

  3. Referee: [§5] §5 (evaluation): the 24 % microbenchmark and 12 % application speedups are presented as direct consequences of EInsn; the text must state the exact baseline (vanilla JIT, no EInsn), the measurement methodology, and any data-exclusion rules so that readers can judge whether the reported ratios are robust.

    Authors: We will expand the opening paragraph of §5 to state that all speedups are measured against the vanilla JIT with EInsn disabled. We will also document the methodology (100 iterations after warm-up, perf hardware counters on x86-64 and ARM64, no data points excluded except for obvious measurement artifacts such as context-switch spikes) so that the 24 % and 12 % figures can be evaluated for robustness. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper grounds its safety claim in Lean 4 proofs establishing semantic equivalence between proof sequences and native emits, with the verifier continuing to check the proof sequence. Performance numbers (24% microbenchmarks, 12% applications, 2.358x whole-program) are presented as direct empirical measurements rather than quantities derived from the paper's own equations or fitted parameters. No self-definitional steps, fitted-input predictions, load-bearing self-citations, uniqueness theorems, or ansatzes smuggled via citation are present. The derivation chain relies on external verification and benchmark results and does not reduce to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The design depends on the existing eBPF verifier correctly validating proof sequences and on the Lean proofs correctly establishing equivalence; no free parameters are introduced in the abstract.

axioms (1)
  • domain assumption The existing eBPF verifier can correctly and completely check the safety of any proof sequence composed of vanilla eBPF instructions.
    Invoked as the foundation for why only the native emit adds to the TCB.
invented entities (2)
  • Kops extension interface no independent evidence
    purpose: Mechanism allowing userspace compilers and kernel modules to register new operations with a proof sequence and native emit.
    Core new construct proposed to solve the optimization-vs-TCB tradeoff.
  • EInsn operations no independent evidence
    purpose: Seven concrete operations (rotate, conditional select, etc.) implemented via the Kops interface.
    New operations whose equivalence is proven and whose performance is measured.

pith-pipeline@v0.9.1-grok · 5858 in / 1482 out tokens · 37171 ms · 2026-06-25T21:53:01.164921+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

37 extracted references · 15 canonical work pages

  1. [1]

    Amazon Web Services. 2024. LNSym: Armv8 Native Code Symbolic Simulator in Lean.https://github.com/leanprover/LNSym. Accessed: 2026-06-09

    2024

  2. [2]

    Aqua Security. 2026. Tracee: Runtime Security and Forensics using eBPF.https://github.com/aquasecurity/tracee. Accessed: 2026-04-06

    2026

  3. [3]

    bpftrace Authors. 2019. bpftrace: High-level Tracing Language for Linux.https://github.com/bpftrace/bpftrace. Accessed: 2026-06-09

    2019

  4. [4]

    Marco Spaziani Brunella, Giacomo Belocchi, Marco Bonola, Salva- tore Pontarelli, Giuseppe Siracusano, Giuseppe Bianchi, Aniello Cam- marano, Alessandro Palumbo, Luca Petrucci, and Roberto Bifulco

  5. [5]

    In14th USENIX Symposium on Operating Systems Design and Imple- mentation (OSDI 20)

    hXDP: Efficient Software Packet Processing on FPGA NICs. In14th USENIX Symposium on Operating Systems Design and Imple- mentation (OSDI 20). USENIX Association, Virtual Event, 973–990. https://www.usenix.org/conference/osdi20/presentation/brunella

  6. [6]

    Cilium Authors. 2024. Cilium: eBPF-based Networking, Observability, and Security.https://cilium.io. Accessed: 2026-04-06

    2024

  7. [7]

    Jonathan Corbet. 2019. KRSI—the other BPF security module. LWN.net, https://lwn.net/Articles/808048/. Accessed: 2026-04-06

    2019

  8. [8]

    Jonathan Corbet. 2023. The extensible scheduler class. LWN.net, https://lwn.net/Articles/922405/. Accessed: 2026-04-06

    2023

  9. [9]

    Milo Craun, Adam Oswald, and Dan Williams. 2023. Enabling eBPF on Embedded Systems Through Decoupled Verification. InProceedings of the 1st Workshop on EBPF and Kernel Extensions(New York, NY, USA) (eBPF ’23). Association for Computing Machinery, New York, NY, USA, 63–69.https://doi.org/10.1145/3609021.3609299

    work page doi:10.1145/3609021.3609299 2023

  10. [10]

    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.https://doi.org/10.1145/3694715.3695950

    work page doi:10.1145/3694715.3695950 2024

  11. [11]

    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

  12. [12]

    InProceedings of the 40th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation(Phoenix, AZ, USA) (PLDI 2019)

    Simple and precise static analysis of untrusted Linux kernel extensions. InProceedings of the 40th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation(Phoenix, AZ, USA) (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 1069–1084.https://doi.org/10.1145/3314221.3314590

    work page doi:10.1145/3314221.3314590 2019

  13. [13]

    IO Visor Project. 2015. BCC: Toolkit for BPF-based Linux Tracing and Performance Analysis.https://github.com/iovisor/bcc. Accessed: 2026-06-09

    2015

  14. [14]

    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. In2025 USENIX Annual Tech- nical Conference (USENIX ATC 25). USENIX Association, Boston, MA, 325–342.https://www.useni...

    2025

  15. [15]

    Hsuan-Chi Kuo, Kai-Hsun Chen, Yicheng Lu, Dan Williams, Sibin Mohan, and Tianyin Xu. 2022. Verified programs can party: optimizing kernel extensions via post-verification merging. InProceedings of the Seventeenth European Conference on Computer Systems(Rennes, France) (EuroSys ’22). Association for Computing Machinery, New York, NY, USA, 283–299.https://d...

    work page doi:10.1145/3492321.3519562 2022

  16. [16]

    Xavier Leroy. 2009. Formal verification of a realistic compiler.Com- mun. ACM52, 7 (July 2009), 107–115.https://doi.org/10.1145/1538788. 1538814

    work page doi:10.1145/1538788 2009

  17. [17]

    Soo Yee Lim, Tanya Prasad, Xueyuan Han, and Thomas Pasquier

  18. [18]

    InProceedings of the 2024 on Cloud Computing Se- curity Workshop(Salt Lake City, UT, USA)(CCSW ’24)

    SafeBPF: Hardware-assisted Defense-in-depth for eBPF Ker- nel Extensions. InProceedings of the 2024 on Cloud Computing Se- curity Workshop(Salt Lake City, UT, USA)(CCSW ’24). Associa- tion for Computing Machinery, New York, NY, USA, 80–94.https: //doi.org/10.1145/3689938.3694781

    work page doi:10.1145/3689938.3694781 2024

  19. [19]

    Linux kernel contributors. 2026. BPF Kernel Functions (kfuncs). https://docs.kernel.org/bpf/kfuncs.html. Linux kernel documenta- tion. Accessed: 2026-06-10

    2026

  20. [20]

    InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21), June 20-25, 2021, Virtual, Canada

    Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: Bounded Translation Validation for LLVM. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21). ACM, New York, NY, USA, 65–79.https://doi.org/10.1145/3453483.3454030

    work page doi:10.1145/3453483.3454030 2021

  21. [21]

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

    2024

  22. [22]

    Jinsong Mao, Hailun Ding, Juan Zhai, and Shiqing Ma. 2024. Mer- lin: Multi-tier Optimization of eBPF Code for Performance and Com- pactness. InProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3(La Jolla, CA, USA)(ASPLOS ’24). Association for Computing Machinery, New York,...

    work page doi:10.1145/3620666.3651387 2024

  23. [23]

    Meta. 2018. Katran: A high performance layer 4 load balancer.https: //github.com/facebookincubator/katran. Accessed: 2026-04-06

    2018

  24. [24]

    Microsoft. 2026. eBPF for Windows.https://github.com/microsoft/ ebpf-for-windows. Accessed: 2026-04-06

    2026

  25. [25]

    George C. Necula. 1997. Proof-carrying code. InProceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Paris, France)(POPL ’97). Association for Computing Ma- chinery, New York, NY, USA, 106–119.https://doi.org/10.1145/263699. 263712

    work page doi:10.1145/263699 1997

  26. [26]

    Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, Virtual Event, 41–61.https://www.usenix. org/conference/osdi20/presenta...

    2020

  27. [27]

    Hao Sun and Zhendong Su. 2025. Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction Refinement. InPro- ceedings 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. https://doi.org/10.1145/3731569.3764796

    work page doi:10.1145/3731569.3764796 2025

  28. [28]

    Dave Thaler. 2024. BPF Instruction Set Architecture (ISA). RFC 9669. https://doi.org/10.17487/RFC9669

    work page doi:10.17487/rfc9669 2024

  29. [29]

    Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak

  30. [30]

    InComputer Aided Verification: 32nd International Conference, CA V 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II(Los Angeles, CA, USA)

    Synthesizing JIT Compilers for In-Kernel DSLs. InComputer Aided Verification: 32nd International Conference, CA V 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II(Los Angeles, CA, USA). Springer-Verlag, Berlin, Heidelberg, 564–586.https://doi.org/10.1007/ 978-3-030-53291-8_29

    2020

  31. [31]

    Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2023. Verifying the Verifier: eBPF Range Anal- ysis 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. https://doi.org...

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

  32. [32]

    Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastruc- ture. In11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO, 33– 47.https://www.usenix.org/conference/osdi14/technical-sessions/ presentation/wang_xi

    2014

  33. [33]

    Yiming Xiang, Wanning He, Mehbubul Hasan Al-Quvi, Emmett Witchel, and Ryan Huang. 2025. ePass: A Framework for Enhanc- ing Flexibility and Runtime Safety of eBPF Programs. Linux Plumbers Conference (LPC).https://lpc.events/event/19/contributions/2179/

    2025

  34. [34]

    Wong, Tanvi Wagle, Srinivas Narayana, and Anirudh Sivaraman

    Qiongwen Xu, Michael D. Wong, Tanvi Wagle, Srinivas Narayana, and Anirudh Sivaraman. 2021. Synthesizing safe and efficient ker- nel extensions for packet processing. InProceedings of the 2021 ACM SIGCOMM 2021 Conference(Virtual Event, USA)(SIGCOMM ’21). As- sociation for Computing Machinery, New York, NY, USA, 50–64. https://doi.org/10.1145/3452296.3472929

    work page doi:10.1145/3452296.3472929 2021

  35. [35]

    Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, and Emmanuel Baccelli. 2022. End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. InComputer Aided Verification: 34th International Conference, CA V 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part II(Haifa, Israel). Springer-Verlag, Berlin, He...

    work page doi:10.1007/978-3-031-13188- 2022

  36. [36]

    Yusheng Zheng, Tong Yu, Yiwei Yang, Yanpeng Hu, Xiaozheng Lai, Dan Williams, and Andi Quinn. 2025. Extending Applications Safely and Efficiently. In19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25). USENIX Association, Boston, MA, 557– 574.https://www.usenix.org/conference/osdi25/presentation/zheng- yusheng

    2025

  37. [37]

    Qian Zhu, Yuxuan Liu, Ziyuan Zhu, Shangqing Liu, and Lei Bu. 2025. EPSO: A Caching-Based Efficient Superoptimizer for BPF Bytecode. In 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)(Seoul, Korea, Republic of). IEEE Press, Piscataway, NJ, USA, 2945–2956.https://doi.org/10.1109/ASE63991.2025.00242 12 BPF Verifier BPF JIT...

    work page doi:10.1109/ase63991.2025.00242 2025