Toward the Verification of a Simple Hypervisor
Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying virtual machine monitors (hypervisors). This paper describes an ongoing project to develop and verify MinVisor, a simple but functional Type-I x86 hypervisor, proving protection properties at the assembly level using ACL2. Originally based on an existing research hypervisor, MinVisor provides protection of its own memory from a malicious guest. The authors' long-term goal is to fully verify MinVisor, providing a vehicle to investigate the modeling and verification of hypervisors at the implementation level, and also a basis for further systems research.