Modelling and formally verifying intel VT-x: Hardware assistance for processors running virtualization platforms

Abstract

The Virtualization in computer science is the process of creating a virtual replica of computer resources like processor, hardware platforms, network devices, etc. Hardware virtualization is the creation of Virtual Machines (VM) that acts like a real computer with an operating system. Virtualization is controlled by special software called hypervisor or Virtual Machine Monitor (VMM) which manages the resources for the running virtual machines. Virtual machines can’t access hardware resources directly. The modern processors are enabled with the mechanisms to support the virtual machine environment. Intel provides hardware-assisted virtualization mechanisms for Intel processors. Intel VT-x provides virtualization mechanisms for processor virtualization. In this paper, we present a novel work of verifying the properties of Intel VT-x formally. The verification is carried out on the design level using the mCRL2 tool. The formal verification of Intel VT-x along with its code written in the mCRL2 modelling language is presented.