Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework
IEEE Symposium on Security and Privacy(2013)
摘要
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.
更多查看译文
关键词
automated verification,xmhf core,assembly language code,high performance,memory integrity,c code,hypervisor-based security architecture,modular hypervisor framework,additional security,fundamental hypervisor security property,security,virtualization,hardware,computer architecture,assembly language,virtual machines,formal verification,verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络