TC: Small: V2M2: Towards a Verified Virtual Machine Monitor

虚拟化正在迅速成为计算系统的一项关键技术，有望在安全性、效率和可靠性方面带来显著的好处。完全实现这些优势取决于虚拟机监视器(管理程序)的可靠性。这项研究致力于开发一个非常高保证、商业质量的管理程序：(1)设计实用的工具和技术来使关于管理程序的推理变得可行；(2)通过对现有的简单研究管理程序的正式验证来磨练它们；(3)应用它们来开发和证明一系列越来越现实的管理程序模型，目标是实现一个完全功能的、经过正式验证的管理程序。首先，使用ACL2形式化分析工具对现有的研究管理程序进行建模和验证。在第二个轨迹中，开发了适用于各种管理程序实现的工具和方法。这项工作旨在推进对一类重要软件应用程序的形式化分析，并促进形式化方法的发展，特别是大型和复杂形式证明的管理。这项研究是得克萨斯大学奥斯汀分校正式方法和系统研究小组的合作成果。

Virtualization is rapidly becoming a key technology for computingsystems, promising significant benefits in security, efficiency, anddependability. Fully realizing these benefits depends upon thereliability of virtual machine monitors (hypervisors). This researchaims toward developing a very high assurance, commercial qualityhypervisor 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 existingresearch hypervisor is modeled and verified using the ACL2 formalanalysis tools. In the second track, tools and methodologies aredeveloped applicable to a wide variety of hypervisor implementations.This work aims to advance the formal analysis of an important class ofsoftware applications and to advance the state of the art in formal methods,particularly management of large and complex formal proofs. Thisresearch is a collaboration between the formal methods and systemsresearch groups at the University of Texas at Austin.