Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework
Venue
IEEE Symposium on Security and Privacy (2013) (to appear)
Publication Year
2013
Authors
Amit Vasudevan, Sagar Chaki, Limin Jia, Jonathan McCune, James Newsome, Anupam Datta
BibTeX
Abstract
We present the design, implementation, and verification of XMHF - an eXtensible and
Modular Hypervisor Framework. XMHF is designed to achieve three goals - modular
extensibility, automated verification, and high performance. XMHF includes a core
that provides functionality common to many hypervisor-based security architectures
and supports extensions that augment the core with additional security or
functional properties while preserving the fundamental hypervisor security property
of memory integrity (i.e., ensuring that the hypervisor's memory is not modified by
software running at a lower privilege level). We verify the memory integrity of the
XMHF core - 6018 lines of code - using a combination of automated and manual
techniques. The model checker CBMC automatically verifies 5208 lines of C code in
about 80 seconds using less than 2GB of RAM. We manually audit the remaining 422
lines of C code and 388 lines of assembly language code that are stable and
unlikely to change as development proceeds. Our experiments indicate that XMHF's
performance is comparable to popular high-performance general-purpose hypervisors
for the single guest that it supports.
