{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/129429"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/129429","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Making safe OS kernel extensions expressive, efficient, and easy to program","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_has_math":false,"creators":["Jia, Jinghao"],"institution":"University of Illinois Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Xu, Tianyin","Bates, Adam","Franke, Hubertus","Le, Michael V.","Marinov, Darko","Williams, Dan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-04-23","date_published":"2025-04-23","updated_at":"2026-07-22T22:25:05Z","subjects":["Operating Systems","Performance","Programming Languages","Security","Safety"],"languages":["en","eng"],"rights":["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]."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/129429","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Xu, Tianyin","Bates, Adam","Franke, Hubertus","Le, Michael V.","Marinov, Darko","Williams, Dan"]},{"key":"dc:creator","label":"Author","values":["Jia, Jinghao"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2025-04-23","2025-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Operating Systems","Performance","Programming Languages","Security","Safety"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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]."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/129429"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","The student, Jinghao Jia, accepted the attached license on 2025-04-22 at 17:03.","The student, Jinghao Jia, submitted this Dissertation for approval on 2025-04-22 at 17:40.","This Dissertation was approved for publication on 2025-04-23 at 09:29.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21901 on 2025-10-19 at 18:18:39","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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Making safe OS kernel extensions expressive, efficient, and easy to program"]}]}],"canonical_facts":{"dc:contributor":["Xu, Tianyin","Bates, Adam","Franke, Hubertus","Le, Michael V.","Marinov, Darko","Williams, Dan"],"dc:creator":["Jia, Jinghao"],"dc:date":["2025-04-23","2025-05"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","The student, Jinghao Jia, accepted the attached license on 2025-04-22 at 17:03.","The student, Jinghao Jia, submitted this Dissertation for approval on 2025-04-22 at 17:40.","This Dissertation was approved for publication on 2025-04-23 at 09:29.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21901 on 2025-10-19 at 18:18:39","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."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/129429"],"dc:language":["en","eng"],"dc:rights":["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]."],"dc:subject":["Operating Systems","Performance","Programming Languages","Security","Safety"],"dc:title":["Making safe OS kernel extensions expressive, efficient, and easy to program"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:05Z"}