Model Checking Based Security Analysis On Hyper-V Based Hypervisor

Cloud computing is expected to transform the IT landscape in the very near future. At the core of such virtualization is the software called hypervisor. However, traditional and virtualization-aware security solutions do not map well to the virtualized environments for the complex and ever-dynamic nature of the cloud computing. Finding.vulnerabilities of hypervisor itself first is the essential way to make virtualization platform more secure.In order to find as many vulnerabilities in the hypervisor as possible, the evaluation process must include demonstration of correct correspondence between system representations at various levels of abstraction. Thus, we could use model-checking theory in formal analysis methods to discover vulnerabilities. Here remain some limitations when studying the security of hypervisor by applying the present model checking method:1. Some researches just verify the correctness of softwares rather than the security of them, such as VCC. VCC uses model checking method to verify the correctness of Hyper-V source code. Some code-level extended static analysis tools handle both behavioural aspects of underlying data structures as well as concurrency issues. But the security of softwares is out of consideration.2, Some methods are only suitable for open-source hypervisors. Some researches attempt to formally document the code’s intents and take security into consideration. But this is not suitable for hypervisors which are none open-source softwares.The paper focuses on using model-checking methods to address vulnerabilities of Hyper-V based hypervisor. The study follows the process of abstraction-modeling-specification-verification. The author’s major contributions are outlined as follows:1. The basic architecture of Hyper-V is analyzed. The paper studies Microsoft’s virtualization technology and architecture, and analyses the security features of Hyper-V. Sensitive instructions, privileged instructions, CPU’s states and the states transitions are classified into different levels. Different subjects’ executable instructions are defined. Three simple states’ state transition diagrams are constructed.2. The security reference model of Hyper-V’s CPU is constructed. We formally define every subject of Hyper-V. By using Promela and SPIN, we get CPU’s finite state model. The subjects in the CPU’s finite state model include a VMM, a VMPP and two VMCP. Based on this finite state model, we get CPU’s security reference model with the help of LTL.3. The security reference model of Hyper-V’s memory is constructed. The mappings from virtual memory to physical memory are described. We classify physical memory into three levels and define different memory access rights for different subjects. Based on subjects’ formal definitions and finite state models, attributes related to memory can be abstracted from subjects. We formally describe the subjects and construct memory’s finite state model. Finally, by analyzing memory’s transition rules and memory’s finite state model, we can use SPIN to construct the memory’s security reference model.4. The security reference model of CPU’s state for concurrent tasks is constructed. For DoS attacks, we construct the security reference model of CPU’s state for concurrent tasks based on Hyper-V’s architecture and scheduling mechanisms. This model can be used to abstract the related codes of hypercalls and reduce the workload of analyzing the codes.The security reference model of Hyper-V’s CPU, the security reference model of Hyper-V’s memory and the security reference model of CPU’s state for concurrent tasks establish the foundation for detecting the code security.