|Title:||Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor Research Area|
|Authors:||Jason Franklin, Arvind Seshadri, Ning Qu, Sagar Chaki, Anupam Datta|
|Publication Date:||April 18, 2008|
SecVisor is a hypervisor designeed to guarantee that only code approved by the user of a system executes at the privilege level of the OS kernel . We employ a model checker to verify the design properties of SecVisor and identify two-designlevel 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 SecVisor-protected 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.
Full Report: CMU-CyLab-08-008