x86-64 VM Monitor for seL4 verified microkernel
Very restricted virtualized environment for higher security
The security of any software system depends on its underlying Operating System (OS). However, even 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. For example, the Qubes' Xen Security Advisory Tracker reports that 53/283 (18%) of Xen vulnerabilities over the last eight years affected Qubes. As a step towards facilitating the implementation of more secure, Qubes-like systems, we propose to retarget it to the seL4 microkernel. 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 Xen replacement for Qubes, however, its virtualization support is currently limited. As a first step to enabling Qubes on seL4 we will implement a hardened, open-source, x86 64-bit Virtual Machine Monitor (VMM) for the seL4 microkernel capable of hosting the core Qubes OS virtual machines.
- The project's own website: https://trustworthy.systems/projects/TS/makatea
Why does this actually matter to end users?
How can you understand and trust a complex system, like the operating system managing the hardware and software on your computer? You can make the complexity simpler by cutting it up into parts, compartmentalizing what does what, where information is stored, which processes talk to each other. This way users can be sure their system only does what it is supposed to do and know precisely what goes in and what comes out. This can be done through virtual machines, which are isolated simulations of operating systems or programs on a computer. Simply put, you create virtual rooms where only one thing happens and only you have the keys to each door. This can give users complete control over what happens on their computer and ensures that if some malicious software finds a way in, it cannot get to the other rooms. This can be very important if your device contains sensitive information, if some ill-meaning third party tries to listen in, or when the device is part of some crucial infrastructure and is targeted for attacks.
The Qubes operating system is a pioneer in creating an isolated yet workable desktop. Users can segment programs and data into separate cubes, based on trust. The default cubes are 'work', 'personal' and 'untrusted', that are each run in an isolated virtual machine. If you open a phishing email in your 'untrusted' cube and malware manages to make its way into this specific environment, it cannot get to 'personal' or 'work' and therefore cannot compromise that data (or the entire operating system, which is the case with popular operating systems like Windows that have a huge attack surface). Various colors (think green, yellow, red) can be used to indicate what window and program works in what qube.
Security by isolation can and should be a great way to make operating systems more secure by design. Unfortunately even operating systems like Qubes need other programs to work that may be insecure (and have actual reported vulnerabilities). This project will make Qubes-like systems more secure by switching from a vulnerable dependency to a verified and well-maintained alternative.
Run by Neutrality, University of New South Wales (UNSW), and ITL
This project was funded through the NGI0 PET 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 825310.
