seL4 Microkernel for virtualization use-cases: Potential directions towards a standard VMM

TL;DR

This paper explores how to develop a standardized, full-featured virtual machine monitor for the seL4 microkernel, emphasizing security, resource efficiency, and community-driven design for edge computing applications.

Contribution

It presents design principles and feature sets for a standard VMM on seL4, aiming to foster community discussion and development.

Findings

seL4 offers a secure, formally verified microkernel suitable for edge virtualization

Current userland tools for seL4 are immature and fragmented

Proposed directions aim to standardize and improve VMM support on seL4

Abstract

Virtualization plays an essential role in providing security to computational systems by isolating execution environments. Many software solutions, called hypervisors, have been proposed to provide virtualization capabilities. However, only a few were designed for being deployed at the edge of the network, in devices with fewer computation resources when compared with servers in the Cloud. Among the few lightweight software that can play the hypervisor role, seL4 stands out by providing a small Trusted Computing Base and formally verified components, enhancing its security. Despite today being more than a decade with seL4 microkernel technology, its existing userland and tools are still scarce and not very mature. Over the last few years, the main effort has been put into increasing the maturity of the kernel itself and not the tools and applications that can be hosted on top. Therefore, it currently lacks proper support for a full-featured userland Virtual Machine Monitor, and the existing one is quite fragmented. This article discusses the potential directions to a standard VMM by presenting our view of design principles and feature set needed. This article does not intend to define a standard VMM, we intend to instigate this discussion through the seL4 community.