First Advisor

Bart Massey

Date of Award

5-24-2019

Document Type

Thesis

Degree Name

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

Department

Mathematics

Subjects

Operating systems (Computers) -- Design, Computer security, Rust (Computer program language)

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.

Rights

In Copyright. URI: http://rightsstatements.org/vocab/InC/1.0/ This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).

Persistent Identifier

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

Download

Share

COinS