Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor (CMU-CyLab-08-008)

SecVisor is a hypervisor designed to guarantee that only code approved by the user of a system executes at the privilege level of the OS kernel [17]. We employ a model checker to verify the design properties of SecVisor and identify two design-level attacks that violate SecVisor’s security requirements. Despite SecVisor’s narrow interface and tiny code size, our attacks were overlooked in both SecVisor’s design and implementation. Our attacks exploit weaknesses in SecVisor’s memory protections. We demonstrate that our attacks are realistic by crafting exploits for an implementation of SecVisor and successfully performing two attacks against a SecVisorprotected Linux kernel. To repair SecVisor, we design and implement an efficient and secure memory protection scheme. We formally verify the security of our scheme. We demonstrate that the performance impact of our proposed defense is negligible and that our exploits are no longer effective against the repaired implementation. Based on this case study, we identify facets of secure system design that aid the verification process.