Date of Award
Bachelor of Science (B.S.) in Mathematics and University Honors
Operating systems (Computers) -- Design and construction, Rust (Computer programming language), Operating systems (Computers) -- Verification, Computer security
Microkernels are a family of operating system kernels characterized by their small codebase. Due to their small size microkernels provide extra security and reliability as compared to larger, monolithic kernels. When combined with a capability-based architecture these benefits are enhanced, allowing for even greater security through the principle of least privilege. The seL4 microkernel, written in C and formally verified, takes advantage of this capability-based architecture.
Formal verification is an incredibly powerful tool--however, its cost is significant. Rust is a strongly-typed systems programming language that provides numerous safety advantages over C and C++, completely eliminating large classes of bugs. This makes the Rust programming language a good candidate for operating system development.
This thesis describes Wayless, a capability-based microkernel heavily inspired by seL4. The kernel aims to provide an seL4-compatible application binary interface (ABI), letting seL4 programs run without modification on Wayless. Wayless provides some of the same safety benefits as seL4 through use of the Rust programming language, without going through the process of formal verification. Development on Wayless is still in its early stages but progress has been promising: Wayless already implements most of seL4's system calls and a portion of seL4's capability system.
Cude, Waylon, "Wayless: A Capability-Based Microkernel" (2019). University Honors Theses. Paper 690.