Building a Hypervisor on a Formally Verifiable Protection Layer

Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying hyper visor. Hyper visors provide complete control of the virtualized resources (protection), a reasonably accurate view of these resources (fidelity), and performance. To facilitate formal verification of protection, we present an architecture, aligned with the hardware virtualization barrier, that separates hyper visor protection from the other goals. The hyper visor is constructed on a minimal trusted computing base or "min visor" whose main responsibility is protection. Each real guest is paired with an untrusted fidelity guest that builds on the protection layer to provide a fully virtualized environment. This allows verification of protection without considering much of the functionality of a traditional hyper visor. We have coded such a protection layer, developed a simple hyper visor on it, and begun formally verifying its protection properties at the machine code level. The current paper is a progress report.