DocumentCode :
1590248
Title :
Building a Hypervisor on a Formally Verifiable Protection Layer
Author :
McCoyd, Michael ; Krug, Robert Bellarmine ; Goel, Deepak ; Dahlin, Mike ; Young, William
fYear :
2013
Firstpage :
5069
Lastpage :
5078
Abstract :
Virtualization promises significant benefits in security, efficiency, dependability, and cost. Achieving these benefits depends upon the reliability of the underlying hyper visor. Hyper visors provide complete control of the virtualized resources (protection), a reasonably accurate view of these resources (fidelity), and performance. To facilitate formal verification of protection, we present an architecture, aligned with the hardware virtualization barrier, that separates hyper visor protection from the other goals. The hyper visor is constructed on a minimal trusted computing base or "min visor" whose main responsibility is protection. Each real guest is paired with an untrusted fidelity guest that builds on the protection layer to provide a fully virtualized environment. This allows verification of protection without considering much of the functionality of a traditional hyper visor. We have coded such a protection layer, developed a simple hyper visor on it, and begun formally verifying its protection properties at the machine code level. The current paper is a progress report.
Keywords :
Hardware; Registers; Security; Software; Virtual machine monitors; Virtual machining; Virtualization; formal verification; hardware virtualization; hypervisor;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
System Sciences (HICSS), 2013 46th Hawaii International Conference on
Conference_Location :
Wailea, HI, USA
ISSN :
1530-1605
Print_ISBN :
978-1-4673-5933-7
Electronic_ISBN :
1530-1605
Type :
conf
DOI :
10.1109/HICSS.2013.121
Filename :
6480458
Link To Document :
بازگشت