Virtualization is rapidly becoming a key technology for computing systems, promising significant benefits in security, efficiency, and dependability. Fully realizing these benefits depends upon the reliability of virtual machine monitors (hypervisors). This research aims toward developing a very high assurance, commercial quality hypervisor by:
(1) designing practical tools and techniques to make reasoning about hypervisors feasible; (2) honing them through the formal verification of an existing simple research hypervisor; and (3) applying them to develop and prove a graduated series of more and more realistic hypervisor models, aiming toward a fully functional, formally verified hypervisor.
The project proceeds along two tracks. In the first, an existing research hypervisor is modeled and verified using the ACL2 formal analysis tools. In the second track, tools and methodologies are developed applicable to a wide variety of hypervisor implementations. This work aims to advance the formal analysis of an important class of software applications and to advance the state of the art in formal methods, particularly management of large and complex formal proofs. This research is a collaboration between the formal methods and systems research groups at the University of Texas at Austin.
