Formally Verifying Isolation and Availability in an Idealized Model of Virtualization

"Hypervisors allow multiple guest operating systems to run on \n shared hardware, and offer a compelling means of improving the security and the flexibility of software systems. We formalize in the Coq proof assistant an idealized model of a hypervisor, and formally establish that the hypervisor ensures strong isolation properties between the different operating systems, and guarantees that requests from guest operating systems are eventually attended."