Examining the Impact of Microarchitectural Attacks on Microkernels : a study of Meltdown and Spectre

Most of today's widely used operating systems are based on a monolithic design and have a very large code size which complicates verification of security-critical applications. One approach to solving this problem is to use a microkernel, i.e., a small kernel which only implements the bare necessities. A system usinga microkernel can be constructed using the operating-system framework Genode, which provides security features and a strict process hierarchy. However, these systems may still be vulnerable to microarchitectural attacks, which can bypassan operating system's security features, exploiting vulnerable hardware. This thesis aims to investigate whether microkernels are vulnerable to the microarchitectural attacks Meltdown and Spectre version 1 in the context of Genode. Furthermore, the thesis analyzes the execution cost of mitigating Spectre version 1 in a Genode's remote procedure call. The result shows how Genode does not mitigate the Meltdown attack, which will be confirmed by demonstrating a working Meltdown attack on Genode+Linux. We also determine that microkernels are vulnerable to Spectre by demonstrating a working attack against two microkernels. However, we show that the cost of mitigating this Spectre attack is small, with a cost of < 3 slowdown for remote procedure calls in Genode