Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework

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.