[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)