Modelling and Formally Verifying Intel VT-x: Hardware Assistance for Processors Running Virtualization Platforms
Ram Chandra Bhushan1, Dharmendra K Yadav2
1Ram Chandra Bhushan, Research Scholar, Department of Computer Science and Engineering, Motilal Nehru National Institute of Technology Allahabad (Uttar Pradesh), India.
2Dharmendra K Yadav, Professor, Department of Computer Science and Engineering, Motilal Nehru National Institute of Technology Allahabad (Uttar Pradesh), India.
Manuscript received on 18 April 2019 | Revised Manuscript received on 25 April 2019 | Manuscript published on 30 April 2019 | PP: 241-247 | Volume-8 Issue-4, April 2019 | Retrieval Number: D6021048419/19©BEIESP
Open Access | Ethics and Policies | Cite | Mendeley | Indexing and Abstracting
© The Authors. Blue Eyes Intelligence Engineering and Sciences Publication (BEIESP). This is an open access article under the CC-BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
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.
Keywords: Formal Verification, Intel, mCRL2, Model Checkings
Scope of the Article: Computer Science and Its Applications