Design, Development and Automated Verification of an Integrity-Protected Hypervisor (CMU-CyLab-12-017)

Hypervisors are a popular mechanism for implementing software virtualization. Since hypervisors execute at a very high privilege level, they must be secure. A fundamental security property of a hypervisor is memory integrity – the hypervisor’s memory must not be modified by software running at a lower privilege level. In this paper, we present a methodology – called DRIVE – for designing, developing, and verifying hypervisors to ensure memory integrity. DRIVE combines the power of architectural constraints (captured by a set of system properties and verification conditions) with that of formal analysis (used to discharge the verification conditions). We prove that any hypervisor satisfying the DRIVE properties and verification conditions has memory integrity. We validate DRIVE by using it to develop a hypervisor called XMHF for multi-core systems. In particular, we show how to ensure the DRIVE properties in XMHF by combining hardware virtualization support with design and development decisions. We also show how to discharge the DRIVE verification conditions on XMHF using the CBMC model checker. CBMC verified XMHF’s implementation – about 4700 lines of C code – in about 80 seconds using less than 2GB of RAM.