On memory safety and undefined behavior of unikernels in Rust

• Über Speichersicherheit und undefiniertes Verhalten von Unikerneln in Rust

Kröning, Martin Werner; Monti, Antonello (Thesis advisor); Klimt, Jonathan Christoph (Consultant); Lankes, Stefan (Thesis advisor)

Aachen : RWTH Aachen University (2023)
Master Thesis

Masterarbeit, Rheinisch-Westfälische Technische Hochschule Aachen, 2023

Abstract

Rust is a new systems-programming language with innovative memory safety mechanisms. In 2018, the Hermit unikernel project was ported from C to Rust. Over the years, though, many foundational issues with Hermit's use of Rust's safety mechanisms were found. With this thesis, I fixed a large amount of those issues. I explored the meaning of memory safety, of undefined behavior, and of the guaranteed absence of undefined behavior, a property called soundness. To improve Hermit's safety situation, I created several new synchronization primitives, laying a safe and sound foundation for Hermit. I reworked the core of Hermit regarding safety and successfully eliminated a large variety of issues, resulting in a reduction of over 400 unsafe expressions in Hermit. Furthermore, I worked on automatically detecting undefined behavior in Hermit using the Miri interpreter. This work is the foundation for further safety improvements across all parts of Hermit.

Institutions

• E.ON Energy Research Center [080052]
• Institute for Automation of Complex Power Systems [616310]