Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel
Abstract elided by the publisher.
Related papers
- Verifying the Verifier: eBPF Range Analysis Verification CAV 2023
- End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT CAV 2024
- Simple and precise static analysis of untrusted Linux kernel extensions PLDI 2019
- Synthesizing JIT Compilers for In-Kernel DSLs CAV 2020
- A Flow-Sensitive Refinement Type System for Verifying eBPF Programs OOPSLA 2025
- Comparing the Precision of Abstract Operators in the eBPF Verifier Using Differential Synthesis SAS 2025
- End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers CAV 2022
- Honey Potion: An eBPF Backend for Elixir CGO 2025