.png){kind=small}
L4 microkernels
Recently we’ve had an idea to create a hypervisor managing 2 virtual machines each one running simultaneously. One VM should run an RTOS and second a simple application performing calculations. This article is about considerations on using L4 microkernels on VM in such project.
|
|
Because of that rule microkernels implement only address spaces, threads and IPC (inter-process communication). Everything else is implemented in user space, which simplifies kernel code base at the cost of more context switches (e.g. drivers cannot talk with devices directly, they must do this by a call to the kernel for every I/O and device memory access). This level of abstraction gives every subsystem only the minimum amount of rights, adhering to the Principle Of Least Authority (POLA).
Advantages of microkernels:
- modularity - functionality can be added without changes to the kernel itself,
- security - POLA, address spaces are isolated by the kernel,
- robustness - simple code base, easy to test and review, drivers are implemented mainly in user space so bad driver cannot directly crash the kernel
Disadvantages:
- performance - more context switches between kernel and user space, especially for drivers
- complex process management
- as kernel itself is very simple, application usually must implement key components or ensure that another application implements it and communicate with that second application. This generates even more context switches.
Genode
Genode is an Operating System Framework. It is built from components which can be anything from device drivers to user applications. Genode defines API that applications must use to communicate with kernel.
There are many kernels in L4 family. Genode can use some of them by using
KERNEL=... flag for make. Prerequisites for building Genode are listed in
getting started
section, but it might not be complete (e.g. sel4 kernel requires some
additional Python modules). The most complete and reliable source about Genode
is
Genode Foundation book
.
seL4
This kernel can be build with:
|
|
Unfortunately, kernel seems to hang or stuck in loop in QEMU with black screen and output on serial port ending with:
|
|
This state didn’t change for more than 30 minutes, so it isn’t result of slow emulation. No tests were done on hardware platform.
seL4 manual mentions
use of virtualization. From this document it appears that VMX can be used for
treating each thread as a separate VM. The thread itself runs seL4_VMEnter()
syscall, which means it must be aware of VMX support (and of course of specific
kernel API). Such thread is both the VMM and VM.
Control over VMX is limited so it couldn’t break the rest of the system. I.e. the uses of external interrupt exiting, EPT and I/O ports bitmap are forced, so VM cannot monopolize CPU time or control resources outside of its permitted address space. These limitations are common to all L4 kernels as a consequence of POLA.
NOVA
NOVA is an OS virtualization architecture. It consists of two distinct parts. First one is microhypervisor, which is a privileged layer of virtualization, it is responsible for isolation and communication mechanisms. The other part runs in user-level environment, this piece is called VMM and it is not a part of hypervisor in NOVA’s language. This might be different from other definitions of those terms. For more information see this paper. It also contains some general information about device virtualization and benchmark results.
Following the microkernel approach, the NOVA microhypervisor provides the three basic abstractions:
- Address spaces isolating processes are called Protection Domains (PD),
- Threads are formed by Execution Contexts (EC) and Scheduling Contexts (SC),
- Inter-process communication is established via Portals.
VMM is the part that defines virtualization level of NOVA. It can be a faithful virtualization (where unmodified guest OS is run as Genode subsystem) via VirtualBox for most OSes or via Seoul VMM for Linux-based guests. Other VMMs might have better performance due to paravirtualization (by reducing required number of VM exits), but these require support from the guest OSes.
Summary
One of the VMs in original idea was supposed to be a complete RTOS, delivered in binary form. As such, it would be very difficult (if not impossible) to port this to run as an application under L4 kernel. Because of that we couldn’t use seL4, even though it is a good option if one starts such project from scratch.
NOVA is better suited for such uses. For Linux-like OS Seoul can be used as a VMM, for other systems choose VirtualBox. If OS has working drivers, other options with paravirtualization can be used for achieving better performance while keeping low size of VMM.
If you think we can help in improving the security of your firmware or you
looking for someone who can boost your product by leveraging advanced features
of used hardware platform, feel free to
book a call with us or
drop us email to contact<at>3mdeb<dot>com. If you are interested in similar
content feel free to sign up for our newsletter
