Design, Implementation and Verification of an eXtensible and
Modular Hypervisor Framework
Amit Vasudevan Sagar Chaki, Limin Jia Jonathan McCune, James
Newsome, Anupam Datta,
Proceedings of 34th IEEE Symposium on Security and Privacy
(OAKLAND), page 430-444, May 19-22, 2013.
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.
Online