Hacker News - A Secure and Formally Verified Linux KVM Hypervisor [pdf]
Came across this and wanted to share. Haven’t really read into it, but this tl;dr by user monocasa seems informative:
TL;DR: Changes KVM on ARM to run a tiny verifiable codebase in EL2 (derived from the original KVM code?), and run the rest of the kernel in EL1, then uses standard formal verification techniques on that tiny EL2 component. In a sense, it changes KVM into a Type 1 hypervisor in order to reduce the verification needed to a manageable level.
Sounds especially interesting to me because it uses ARM, and an ARM Qubes is something I daydream about because of all the x86 issues and ME/PSP. However, I wonder if using a KVM to run Linux would lead to too much of a monoculture.