Apologies for the incoherent title: I'd like to better understand the design choices of this project and discuss how it relates to other projects in this space. First I'd like to say that I think that using crosvm is a really great decision. Google has a lot of manpower working on ChromeOS and Android, and building on their work is something that should pay off, especially for a project such as Spectrum that tackles such a huge undertaking (building a secure OS).
Here's a few questions to kick off the discussion:
- Have you considered using a micro kernel based host like seL4, similar to what Genode does (at least as I understand it)? - Have you considered gVisor  for lightweight compartmentalization? - Have you considered reusing stuff from the Whonix project?
- Have you considered using a micro kernel based host like seL4, similar to what Genode does (at least as I understand it)?
I don't know all that much about microkernels, but I have spoken to some microkernel experts. My understanding is that all the required parts are not yet in place to be able to use a microkernel as the host in a system like Spectrum. I am, however, trying to design the system so that the host system is responsible for as little as possible, and therefore hopefully making it possible to transition to a microkernel later should that look feasible.
In principle, the host system should do little other than running virtual machines. Ideally, most hardware interation could be delegated to VMs. This would make it possible to have a very tiny host kernel through disabling most kernel configuration options. The left over code should be just what is critical to run VMs. The paper "A Linux in Unikernel Clothing" compares a minimally-configured Linux kernel to several popular unikernels (not microkernels), with very promising results. It is focused on tiny kernels for single-purpose virtual machines, but I think it contains a lot of relevant insight for all levels of the Spectrum stack.
- Have you considered gVisor  for lightweight compartmentalization?
The main problem I see with gVisor is that it is designed to be run from a full-featured host system. For example, gvisor doesn't provide file system implementations. Instead, it expects to proxy through a file system existing on the host. In Qubes, and hopefully in Spectrum, the host system doesn't have any knowledge of VM file systems, to keep the host as separated from the activities of VMs as possible.
There may still be a place for gVisor in Spectrum -- for example, it could get a shared file system from a separately virtualized kernel. For now, though, one VMM is enough to be going on with. :)
- Have you considered reusing stuff from the Whonix project?
My understanding is that the main thing that Whonix provides is full system images for workstation and gateway machines. We probably wouldn't want to use these directly in Spectrum, because it would go against the principle of configuring the entire system with Nix. However, there will likely be lots of work in Whonix (configurations and so on) that can be reused to similar ends in Spectrum.
Great, happy to see that you considered all of these options and everything you say makes sense. Speaking of Whonix, you may be interested in a recent discussion about hardening a Linux desktop . Since Spectrum is designed to be compartmentalized using VMs, this mainly applies to hardening individual VMs, which is probably less significant than making sure the inter VM communication is secure, but nonetheless may be useful.