  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. Our 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. Functional segments of the MinVisor C
code base are translated into Y86 assembly, and verified with respect to the
Y86 model. The inductive assertions (also known as "compositional cutpoints")
methodology is used to prove the correctness of the code. The proof of the code
that sets up the nested page tables is described. We compare this project to
related efforts in systems code verification and outline some useful steps
forward.
