Send in your ideas. Deadline June 1, 2024
Theme fund: NGI0 Entrust
Start: 2022-12
More projects like this
Operating Systems


An x86, 64-bit Virtual Machine Monitor for the seL4, verified microkernel

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.

Run by Neutrality

Logo NLnet: abstract logo of four people seen from above Logo NGI Zero: letterlogo shaped like a tag

This project was funded through the NGI0 Entrust Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101069594.