Toward the Verification of a Simple Hypervisor

Virtualization promises significant benefits in security, e fficiency, dependability,and cost. Achievingthese benefits depends upon the reliability of the underlyin g virtual machine monitors (hypervisors).This paper describes an ongoing project to develop and verify MinVisor, a simple but functionalType-I x86 hypervisor, proving protection properties at the assembly level using ACL2. Originallybased on an existing research hypervisor, MinVisor provides protection of its own memory from amalicious guest. Our long-term goal is to fully verify MinVisor, providing a vehicle to investigatethe modeling and verification of hypervisors at the implemen tation level, and also a basis for furthersystems research. Functionalsegmentsofthe MinVisorC codebase aretranslatedintoY86assembly,and verified with respect to the Y86 model. The inductive asse rtions (also known as “compositionalcutpoints”) methodology is used to prove the correctness of the code. The proof of the code that setsup the nested page tables is described. We compare this project to related efforts in systems codeverification and outline some useful steps forward.