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

点击翻译按钮获取中文摘要

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.