CAREER: A Framework for Automated Verification of Hypervisors

University Of Washington, Seattle WA

Investigators

Abstract

Hypervisors are an essential component of modern computing devices, from personal laptops to cloud servers. They create the illusion of having multiple physical machines and provide vital support for resource management. Software bugs have proliferated due to the increasing complexity of modern hypervisors; such bugs can cause issues ranging from performance degradation to security vulnerabilities that allow malicious virtual machines to compromise the entire system. This project, IsoV, is to build highly reliable and secure hypervisors through the use of automated verification techniques that effectively eliminate entire classes of software bugs. IsoV will provide novel programming support for developing hypervisors and for formally verifying their correctness and isolation guarantees. The novelty in the project lies in the ideas behind the push-button approach to hypervisor design. The main idea of push-button verification is to design the interfaces of these systems to be finite and amenable to automated verification. The research goal of IsoV is to develop new designs and techniques for automated verification of hypervisors. This project focuses on two common classes of hypervisors: those that provide isolated execution environments to shield applications from untrusted or buggy operating systems; and those that safely partition resources among mutually distrustful virtual machines. The practical and educational goals of this project are to apply IsoV in building real systems; to release the tools and systems as open-source software; and to disseminate results widely. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.