[seL4] Re: QubesOS+seL4

On Wed, Aug 03, 2022 at 12:20:14AM -0400, Demi Marie Obenour wrote:

[ Redirecting this inquiry to the more appropriate ailing list]

On 2 Aug 2022, at 05:55, ossgroup wrote:

I'm interested in porting QubesOS to seL4. Is there already an initiative for this? If not, would you mind pointing me in the right direction to get started?

People have been playing with this on-and-off, including a honours thesis here at UNSW years ago.

The closest current activity I’m aware off is our Makatea project which, in collaboration with Swiss company Neutrality, has a (presently) more limited aim of isolating servers on a private cloud: https://trustworthy.systems/projects/TS/makatea

A full Qubes port would be cool but a fair bit of work. I’d definitely like to see it done, and it’s clearly a more secure approach than having Xen (and therefore a whole Linux) in your trusted computing base.

Gernot

Qubes OS developer here. Switching from Xen to seL4 is something I have very much been interested in. However, there are several difficulties that would need to be overcome: 1. Qubes OS is a highly dynamic system with a human at the console. This means that static resource allocation is not possible even in principle, as there is no way to predict what workloads a person will want to run. Instead, the vast majority of resources must be allocated dynamically, with only a small amount reserved for the hypervisor and management stack. The management stack needs to support creating and destroying VMs, dynamic assignment of memory, CPU overcommit, PCI pass-through, and inter-VM networking. It also needs to support one VM providing block storage for another. 2. Qubes OS aims to support a wide variety of laptop and desktop computers. Currently, only x86_64 is supported, but support for POWER is planned once Xen gets support for it. Building separate system images for each supported system is not practical. Therefore, hardware must be detected at runtime, or at the earliest at install-time. Furthermore, Xen has already proven to have limitations in its hardware support compared to Linux, and I am worried that seL4’s hardware support might be even more limited. Hardware support also includes power management, suspend-to-RAM, and the ability to operate on existing system firmware. 3. Because Qubes OS aims to support the hardware people have, it needs to include mitigations for speculative execution security vulnerabilities. These mitigations must be chosen at runtime, as the hardware the kernel will run on is not known at compile-time. Furthermore, these mitigations need to be effective. This likely means that they need to be in the assembler parts of the kernel entry/exit paths. Requiring userspace code to be compiled with the same flags and/or compiler plugins as the kernel (such as to insert retpolines) might be an option. 4. seL4’s x86_64, IOMMU, VT-x, and SVM code would need to be security-supported and production-ready. This includes the use of interrupt remapping to avoid security holes in PCI pass-through, as well as loading microcode updates during kernel initialization. It also includes the aforementioned mitigations for speculative security flaws, as well as being able to release versions that mitigate new hardware vulnerabilities when those vulnerabilities are made public. For this to be possible, I believe it will be necessary for the seL4 developers to have access to information about vulnerabilities still under embargo. I am not sure if this could be arranged, or how difficult it would be. It may also be necessary to be in contact with people who are experts on the x86 architecture. Finally, making this code production-quality might well require formally verifying it, because of its complexity and the comparatively few people trying to find flaws in it. I have CC’d Marek Marczykowski-Górecki (Qubes OS Project Lead) and Andrew Cooper (Xen developer and x86 expert) in case either of them would like to contribute to the conversation. It is also worth noting that there is no getting around having Linux in the Qubes OS trusted computing base, at least in the near term. One can dramatically limit its exposed attack surface, and Qubes OS tries its best to do exactly that, but it is almost impossible to remove it altogether. The reason is that Qubes OS is a desktop OS. Users expect it to provide a rich and customizable GUI *and* to support a wide variety of hardware. Running the GUI in a Linux VM means that that VM must be trusted, but also makes this task orders of magnitude simpler. Running the GUI natively on seL4 means, at a minimum, reimplementing or porting GPU drivers and a desktop environment. Even FreeBSD lags behind Linux in this regard, and FreeBSD is itself a largely POSIX-compatible OS. Genode is an amazing accomplishment, but its hardware support is quite limited and it certainly does not provide several widely-used desktop environments. Qubes OS currently supports XFCE, KDE, i3, and AwesomeWM, and support for additional window managers is being considered. Even when Qubes OS switches to Wayland, we will at least need to support KWin (KDE Wayland compositor) and Sway. This list will grow, not shrink, over time. -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab