@inproceedings{8ba8d5fb99f04826be408da7d096d7e2,
title = "Kernel extension verification is untenable",
abstract = "The emergence of verified eBPF bytecode is ushering in a new era of safe kernel extensions. In this paper, we argue that eBPF's verifier - -the source of its safety guarantees - -has become a liability. In addition to the well-known bugs and vulnerabilities stemming from the complexity and ad hoc nature of the in-kernel verifier, we highlight a concerning trend in which escape hatches to unsafe kernel functions (in the form of helper functions) are being introduced to bypass verifier-imposed limitations on expressiveness, unfortunately also bypassing its safety guarantees. We propose safe kernel extension frameworks using a balance of not just static but also lightweight runtime techniques. We describe a design centered around kernel extensions in safe Rust that will eliminate the need of the in-kernel verifier, improve expressiveness, allow for reduced escape hatches, and ultimately improve the safety of kernel extensions.",
keywords = "eBPF, kernel extension, operating system, safety, verification",
author = "Jinghao Jia and Raj Sahu and Adam Oswald and Dan Williams and Le, \{Michael V.\} and Tianyin Xu",
note = "We thank Md Sayeedul Islam and Wentao Zhang for early participation in the project. Williams{\textquoteright} group is supported in part by NSF grant CNS-2236966. Xu{\textquoteright}s group is supported in part by NSF grant CNS-1956007 and an Intel gift.; 19th Workshop on Hot Topics in Operating Systems, HotOS 2023 ; Conference date: 22-06-2023 Through 24-06-2023",
year = "2023",
month = jun,
day = "22",
doi = "10.1145/3593856.3595892",
language = "English (US)",
series = "HotOS 2023 - Proceedings of the 19th Workshop on Hot Topics in Operating Systems",
publisher = "Association for Computing Machinery",
pages = "150--157",
booktitle = "HotOS 2023 - Proceedings of the 19th Workshop on Hot Topics in Operating Systems",
address = "United States",
}