Carnegie Mellon University
The authors 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). They verify the memory integrity of the XMHF core - 6018 lines of code - using a combination of automated and manual techniques.