Making safe OS kernel extensions expressive, efficient, and easy to program

Jia, Jinghao

Permalink

https://hdl.handle.net/2142/129429 Copy

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