A Secure and Formally Verified Linux KVM Hypervisor
https://www.youtube.com/watch?v=_11lrjGApIw
Here we include the proofs for KCore splitting into 34 layers, for our verified KVM implementation, SeKVM.
Proofs
34 Security-preserving layers
Bottom layer machine definition
These following definitions comprise the base layer of SeKVM’s refinement proofs. Note that AbsMachineState defines the machine state, and is used throughout the layer refinement proofs.
-
Machine state definition: AbsMachineState
-
Lock-related helpers: AbsMachineLocks
-
Layer definition: AbsMachine
-
Specification: AbsMachineSpec
Top-layer invariants
These invariants are proven over only the top-level specification, TrapHandlerSpec. They are used in the top-level security proofs.
-
Invariant definitions: Invariant
-
Invariant proofs: InvariantProof
Top-layer Security
-
Security property definition: SecurityDef
-
Noninterference tactics: NoninterferenceAux
-
Noninterference lemmas
-
Big-Step Noninterference Theorem
Demo
We demonstrate booting an Ubuntu 16.04 VM on our verified KVM implementation, SeKVM, running on an AMD Seattle Arm server. The server hardware has 8 CPUs and 16GB RAM. The demo VM is configured with 4 virtual CPUs, 12 GB RAM, and standard virtio network/block devices. We show the VM supports full Ubuntu Linux functionality, including disk encryption and networking. We first boot the VM from a LUKS-encrypted virtual disk, and login to its shell. We then run a script to download the Linux kernel source from kernel.org, over a virtual network interface backed by virtio.
