alt Hacker NewsI for one do not want any code in the TCB that is not formally verified, tiny, and easy to audit with every line of code justified.
SeL4 is the only open, mature, and formally verified L4 solution I am aware of that can run on modern servers, but IIRC given vCPUs are not first class objects and any low level CPU virtualization features are handled in user space, it comes at a real performance cost making it only suitable for single-core or non-performance-critical applications.
Nova by contrast was built to handle the expensive and trust critical TPM and vCPU handling directly for high performance remotely attestable multi-core applications without having to reach for something as heavy as Xen, though formal verification is admittedly not as complete as SeL4 yet AFAICT, though lots of recent progress here.
Those are pretty big tradeoffs, but if you or anyone else knows other viable xen alternatives this general shape with a tiny easily-auditable footprint, please chime in!
Like some of what I'm saying is just that if you tell a systems security person "we're using seL4 because of its formal verification", you're going to get eye rolls. Whatever else you want to say about it, the formally-verified configuration of seL4 doesn't actually do much, meaning whatever system you're building on top of it is going to be where all the security drama is anyways.
I'm certainly not telling you to use Xen. I wouldn't use Xen for anything untrusted.