Kernel Extension DSLs Should Be Verifier-Safe!
eBPF allows developers to write safe operating system extensions, but writing these extensions remains challenging because it requires detailed knowledge of both the extension's domain and eBPF's programming interface. Most importantly, the extension must pass the eBPF verifier.
Authors
- Nesime Tatbul (ORCID: https://orcid.org/0000-0002-0416-7022)
- Justus Adam (ORCID: https://orcid.org/0000-0003-4046-534X)
- Malte Schwarzkopf (ORCID: https://orcid.org/0000-0002-5066-6332)
- Andrew Crotty (ORCID: https://orcid.org/0000-0002-8544-0982)
- Franco Solleza
- Akshay Narayan (ORCID: https://orcid.org/0000-0002-6626-141X)
Institutions
- John Brown University (US)
- Mitel (Canada) (CA)
Publication Details
- Published
- 2025-08-19
- DOI
- https://doi.org/10.1145/3748355.3748368
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00