Makatea

The security of any software system depends on its underlying Operating System (OS). However, even compartmentalization focused OSes such as Qubes, which are "reasonably secure" depend on large trusted computing bases (e.g. hypervisors) with hundreds of thousands of lines of code. seL4 is an open-source, formally-verified microkernel that has matured and been maintained for over a decade. seL4's small size (10,000 Lines of Code) and formal verification make it an appealing base to implement a hardened, open-source, x86 64-bit Virtual Machine Monitor (VMM) on. Makatea is a new hypervisor written from the ground up, capable of paravirtualisation, Hardware-Assisted Virtualisation and device emulation. Makatea also will allow to run software originally written for other platforms wherever seL4 can be made to run - and do so in a very controlled environment.