The Xenon separation VMM: Secure virtualization infrastructure for military clouds

In conventional military computing, security separation is provided by cryptography, for data in motion and data at rest. Security separation for data under computation is provided by separate hardware. Cloud computing shares hardware for all data under computation, so a new approach to security separation is needed for military clouds. Cryptographic separation of data under computation is not practical with current technology, so the separation must be accomplished by software, i.e. the virtualization infrastructure. The strongest known means of software separation is the separation kernel. Separation kernels are special virtual machine monitors (VMMs) that are small enough and simple enough to be mathematically verified. Unfortunately, strict separation kernels cannot virtualize the complex modern commodity hardware and guest virtual machine (VM) operating systems that are essential to cloud computing. The best alternative to a strict separation kernel is a a separation VMM. A separation VMM relaxes the strict size and simplicity goals of a separation kernel just far enough to be able to support commodity hardware and guest operating systems. Because they address all of the features of commodity hardware, separation VMMs are too large for formal mathematical verification. However, separation VMMs are small enough and simple enough to be completely specified by semiformal means, i.e. they are smaller and simpler than conventional VMMs. A separation VMM has a complete systematic assurance argument that it isolates guest VMs from each other and strongly protects itself from tampering. A separation VMM provides the strongest separation of cloud VMs that is consistent with virtualizing complex commodity operating systems, on shared complex commodity hardware.