Date of Award

5-24-2019

Document Type

Thesis

Degree Name

Bachelor of Science (B.S.) in Mathematics and University Honors

Department

Mathematics

First Advisor

Bart Massey

Subjects

Operating systems (Computers) -- Design and construction, Rust (Computer programming language), Operating systems (Computers) -- Verification, Computer security

DOI

10.15760/honors.708

Abstract

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.

Persistent Identifier

https://archives.pdx.edu/ds/psu/28797

Share

COinS