Software Model Checking Secure Systems

Presented as part of the 2012 HCSS conference.

Abstract:

Hypervisors have become increasingly popular as a way to allow several guest operating systems to share the same hardware platform.  The hypervisor is maximally privileged software, as it has direct access to the hardware. The security of the hypervisor is extremely important since the security of the entire system that runs on the hypervisor depends critically on whether the hypervisor correctly enforces the desired security policies. In this talk, we present our work on using software model checking to ensure that the hypervisor implementation has desired security properties.  In particular, we develop techniques to verify security properties of hypervisors using an off-the-shelf software model checker for C (CBMC).  We address several technical challenges, including identifying the security properties that are desired of the hypervisors; defining the adversary model; and scaling up the verification techniques given the complex data structures that hypervisors operate on.  We focus on memory protection property: the malicious guest OS cannot access memory beyond the region that the hypervisor allocates for it, and the guest OS cannot write into the memory region where the hypervisor code and data reside.  We view the guest OS as the adversary, and model it based on the interfaces that the hypervisor exposes to the guest OS. To handle large page tables maintained by the hypervisor, which is crucial to ensuring memory protection, we rely on the key observation that the desired properties of these data structures, and the accesses to these data structures, have a uniform pattern: each row of the data structure is accessed independently of other rows. We develop a reduction technique that allows us to define a canonical adversary who has access to the interfaces to a page table of a fixed small size -- only one entry at each level. We prove a set of small-model theorems that show that if there exists a successful attack in a system that has a page table of arbitrary size, then there is an attack by the canonical adversary who has access to the small page table. As a result, analyzing the security properties of the hypervisor is reduced to model checking the canonical adversary, which is very fast.  We have successfully applied our techniques to the verification of several hypervisors, including SecVisor, ShadowVisor, and variants of the Xen hypervisor. We have identified previously unknown vulnerabilities in the design of SecVisor.

Biography:

Limin Jia is a Research Systems Scientist at CyLab at Carnegie Mellon University. She received her Ph.D. in Computer Science from Princeton University.  Her research interests include programming languages, language-based security, logic, and program verification. At CyLab, Limin's research focuses on formal aspects of security. She is particularly interested in applying language-based security techniques as well as formal logic to model and verify security properties of software systems.