Our Partners

Makatea: Qubes-like OS on seL4

Aim

Develop a more secure, Qubes-like OSs for server-side use cases by basing them on seL4, and disaggregating services as simple, modular, and verifiable native components.

Context

Communication security is of critical importance for vital and purpose-driven sectors where cyberattacks can result in loss of lives, including humanitarian and human-rights organizations operating in conflict zones. The mission of our partner, Neutrality, is to safeguard the cyber network of organizations whose integrity and trust is essential in protecting people. Neutrality currently has the interest of 7 international humanitarian and human-rights organizations, including 5 recipients of the Nobel Peace Prize.

Such technology inherently depends on the security of the underlying operating system. Qubes OS is an excellent starting point for such an OS, consisting of a collection of components running in separate virtual machines (VMs). However, the security of the OS can only be as good as the isolation provided by the underlying hypervisor – if that is compromised, so is the whole OS.

Problem

Qubes OS is built on the Xen hypervisor. While much smaller than Linux-based hypervisors such as KVM, the Xen trusted computing base (TCB) is still highly complex and consists of 100s of thousands of lines of monolithic code. Serious vulnerabilities are regularly reported for Xen.

Solution

This project aims to significantly improve the security of a Qubes-like OS by basing it on seL4 instead of Xen, leveraging the formal correctness proofs and much reduced TCB of seL4. In particular, seL4's virtualisation design does not share the virtualisation layer, the virtual-machine monitor (VMM), between VMs, meaning the VMM cannot break isolation even if it is compromised. In addition, critical components can run natively on seL4, further reducing their dependence on unverified code.

Our contribution is to provide a 64-bit VMM for the 64-bit x86 architecture and help project partners to port Qubes OS to the seL4 platform. This leverages our experience with incremental cyber retrofit as pioneered in the DARPA HACMS program.

Support

The Makatea project is supported by a grant from the NLnet Foundation, which “supports organisations and people that contribute to an open information society.”

Latest News

• 2022-02-11: Security analysis and requirements documented.
• 2021-11-29: Public announcement.
• 2021-10-13: UNSW-Neutrality research agreement signed.

Contact