Withdraw
Loading…
Making safe OS kernel extensions expressive, efficient, and easy to program
Jia, Jinghao
Loading…
Permalink
https://hdl.handle.net/2142/129429
Description
- Title
- Making safe OS kernel extensions expressive, efficient, and easy to program
- Author(s)
- Jia, Jinghao
- Issue Date
- 2025-04-23
- Director of Research (if dissertation) or Advisor (if thesis)
- Xu, Tianyin
- Doctoral Committee Chair(s)
- Xu, Tianyin
- Committee Member(s)
- Bates, Adam
- Franke, Hubertus
- Le, Michael V.
- Marinov, Darko
- Williams, Dan
- Department of Study
- Siebel School Comp & Data Sci
- Discipline
- Computer Science
- Degree Granting Institution
- University of Illinois Urbana-Champaign
- Degree Name
- Ph.D.
- Degree Level
- Dissertation
- Keyword(s)
- Operating Systems
- Performance
- Programming Languages
- Security
- Safety
- Abstract
- OS Kernel extensibility has long been an essential capability of contemporary operating systems. In recent years, safe kernel extensions have gained significant traction, evolving from simple packet filters to large, complex programs that customize storage, networking, and scheduling. As the name suggests, these frameworks promise important safety properties for extension programs, including the absence of crashing behavior and proper termination. A notable example is the eBPF kernel extensions on Linux, which employs a static verification scheme to ensure safety properties hold on all program paths. With the increasing popularity, problems and issues in existing safe kernel extension frameworks gradually emerge. This dissertation dives into these problems for three important aspects of safe kernel extensibility—expressiveness, efficiency, as well as programmability—and identifies them as consequences of improper tradeoffs in the design of safe kernel extensions. On the expressiveness aspect, this dissertation looks at the use case of system call filtering with Linux’s Seccomp, where the existing cBPF extension fails to provide the needed expressiveness to support advanced system call security use cases. This dissertation proposes a new, programmable system call filtering mechanism, Seccomp-eBPF, which leverages the more expressive eBPF extensions through a carefully designed framework and security model. Using Seccomp-eBPF, users, whether privileged or not, are able to implement enhanced system call security policies to mitigate vulnerabilities that cannot be handled before. Next, on the efficiency aspect, this dissertation considers two instrumentation use cases of kernel extensions: kernel probing and kernel control flow integrity protection, both suffering from the inefficiency of existing mechanisms. For the kernel probing use case, this dissertation presents Uno-kprobe, a new kernel probe design that achieves universally trapless probing and eliminates the expensive context switches associated with existing trap-based probing implementation for kernel extensions. For kernel control flow integrity protection, this dissertation introduces eKCFI, an eBPF-based KCFI framework that features new instrumentation and attachment mechanisms, which achieves complete kernel code coverage, scalable eBPF program attachment, and efficient kernel instrumentation. Lastly, on the programmability aspect, this dissertation focuses on the existing eBPF extension framework, where the use of static verification incurs significant difficulties in programming eBPF programs—correct programs are often rejected by the verifier due to a gap between the high-level programming language and the low-level verification. This dissertation proposes a new design of safe kernel extension frameworks with Rex, in which extension safety is realized through the inherent language-based safety from Rust, combined with a lightweight extralingual runtime for properties unsuitable for static analysis. Rex eliminates the need for a static verifier and the associated efforts to work around verification issues, thereby closing the language-verifier gap and significantly improving extension programmability.
- Graduation Semester
- 2025-05
- Type of Resource
- Thesis
- Handle URL
- https://hdl.handle.net/2142/129429
- Copyright and License Information
- This dissertation contains research [77] published in Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HotOS ’23) and is adapted here with permission. © 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM. This dissertation contains research [63] published in Proceedings of the 1st Workshop on eBPF and Kernel Extensions (eBPF '23) and is adapted here with permission. © 2023 Copyright held by the owner/author(s). This dissertation contains research [74] published in Proceedings of the 2024 USENIX Annual Technical Conference (USENIX ATC'24). Copyright to the individual work is retained by the author[s].
Owning Collections
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…