Porting Hyperkernel to the ARM architecture

This work describes the porting of Hyperkernel, an x86 kernel, to the ARMv8-A architecture. Hyperkernel was created to demonstrate various OS design decisions that are amenable to push-button verification. Hyperkernel simplifies reasoning about virtual memory by separating the kernel and user address spaces. In addition, Hyperkernel adopts an exokernel design to minimize code complexity, and thus its required proof burden. Both of Hyperkernel’s design choices are accomplished through the use of x86 virtualization support. After developing an x86 prototype, advantageous design differences between x86 and ARM motivated us to port Hyperkernel to the ARMv8-A architecture. We explored these differences and benchmarked aspects of the new interface Hyperkernel provides on ARM to demonstrate that the ARM version of Hyperkernel should be explored further in the future. We also outline the ARMv8-A architecture and the various design challenges overcome to fit Hyperkernel within the ARM programming model.