[HN Gopher] A Secure and Formally Verified Linux KVM Hypervisor ... ___________________________________________________________________ A Secure and Formally Verified Linux KVM Hypervisor [pdf] Author : tmfi Score : 22 points Date : 2021-06-01 20:10 UTC (2 hours ago) (HTM) web link (nieh.net) (TXT) w3m dump (nieh.net) | csdvrx wrote: | > 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... | monocasa wrote: | 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. ___________________________________________________________________ (page generated 2021-06-01 23:01 UTC)