Comparing the Precision of Abstract Operators in the eBPF Verifier Using Differential Synthesis
No abstract available.
DOI 10.1007/978-3-032-07106-4_7
Related papers
- Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel SAS 2024
- A Flow-Sensitive Refinement Type System for Verifying eBPF Programs OOPSLA 2025
- Verifying the Verifier: eBPF Range Analysis Verification CAV 2023
- Synthesizing Precise Static Analyzers for Automatic Differentiation OOPSLA 2023
- End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT CAV 2024
- Synthesizing JIT Compilers for In-Kernel DSLs CAV 2020
- Simple and precise static analysis of untrusted Linux kernel extensions PLDI 2019
- End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers CAV 2022