A Secure and Formally Verified Linux KVM Hypervisor [pdf]

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.

Neat, reminds me of rtlinux, using a Linux module to boot a microkernel with a reduced TCB and more useful semantics in some cases than a full Linux kernel.

> attackers may control peripherals to perform malicious memory accesses via DMA [19]. Side-channel attacks [20], [21], [22], [23], [24], [25] are beyond the scope of the paper

I have been trying to get my hands on modern NVMe : SR-IOv with separate namespace on NVMe device could help mitigating the risk IF you trust the firmware...

This is not at all my area of expertise or anything even remotely close to it but this seems to be a very similar sounding story to one of the core underpinnings of Fuschia.

My understanding was that they put everything kind of dangerous into the micro-kernel and then built their security model around ensuring that everything that interacted with it was only using a set of primitives that they could "guarantee" to be "safe".

Could someone who actually knows about this kind of thing let me know if I am even roughly in the ballpark of correct here?