CAREER: A Framework for Automated Verification of Hypervisors

管理程序是现代计算设备（从个人笔记本电脑到云服务器）的重要组成部分。它们创造了拥有多台物理机器的假象，并为资源管理提供了重要的支持。由于现代管理程序的日益复杂，软件bug已经激增；这些错误可能导致从性能下降到允许恶意虚拟机危害整个系统的安全漏洞等一系列问题。这个项目，IsoV，是通过使用自动验证技术来构建高度可靠和安全的管理程序，该技术可以有效地消除所有类型的软件错误。IsoV将为开发管理程序和正式验证其正确性和隔离保证提供新颖的编程支持。该项目的新颖之处在于管理程序设计的按钮方法背后的思想。按钮验证的主要思想是将这些系统的接口设计为有限的，并适应自动验证。IsoV的研究目标是为管理程序的自动验证开发新的设计和技术。本项目主要关注两类常见的管理程序：提供隔离的执行环境以保护应用程序免受不受信任或有缺陷的操作系统的影响；以及那些在互不信任的虚拟机之间安全地划分资源的虚拟机。该项目的实际和教育目标是将IsoV应用于构建实际系统；将工具和系统作为开源软件发布；并广泛传播结果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.