I wonder if seL4 would make a better basis for Qubes than the Xen it is on now. In particular, does Xen provide anything seL4 doesn't?
In terms of security, the answer is a clear yes. Xen is kernel of 100+kSLOC of unverified code, while seL4 is verified. On top of that, Xen has Dom0 and thus a complete Linux system in its TCB. What Xen has over seL4 is the management/admin framework. But there is a project to port Qubes to seL4, waiting for the funding to be cleared.
Oh, cool. Thanks!
Can't help thinking, though, that we will still need something for administration. NixOS would seem a better choice than Fedora 18 (or whatever Qubes is on) for that.
I am also watching Spectrum with interest.