April 4, 2017
Abstract
In this project we focus on the security of computer virtualization platforms. In particular, the main objective is to develop a formal idealized model of one such platform, establish non-interference security properties that should be guaranteed by the modeled control access mechanisms and to construct mathematical proofs, verified with the help of the Coq proof assistant, that those properties are verified by the model. The project has been partially funded by a grant Fondo Clemente Estable 2009 of the Uruguayan National research agency ANII and currently by a CSIC grant for R&D Projects - edition 2012.
Description and Objectives
Virtualization platforms, and more specifically hypervisors, allow several operating systems to coexist on commodity hardware, and provide support for multiple applications to run seamlessly on the guest operating systems they manage. Moreover, hypervisors provide a means to guarantee that applications with different security policies can execute securely in parallel, by ensuring isolation between their guest operating systems. In effect, hypervisors are increasingly used as a means to improve system flexibility and security, and their use has become ubiquitous in enterprise data centers and cloud computing. The increasingly important role of hypervisors in software systems makes them a prime target for formal verification. Indeed, several projects have set out to formally verify the correctness of hypervisor implementations. Reasoning about implementations provides guarantees that deployed hypervisors provide the expected properties. There are however significant hurdles with this approach, especially if one focuses on proving security properties rather than functional correctness. First, the complexity of formally proving non-trivial properties of implementations might be overwhelming in terms of the effort it requires; worse, the technology for verifying some classes of security properties may be underdeveloped: specifically, liveness properties are notoriously hard to prove, and there is currently no established method for verifying security properties involving two system executions, a.k.a. 2-properties, for implementations. Second, many implementation details are orthogonal to the security properties to be established, and may complicate reasoning without improving the understanding of the essential features for guaranteeing isolation among guest operating systems. Thus, there is a need for complementary approaches where verification is performed on idealized models that abstract away from the specifics of any particular hypervisor, and yet provide a realistic setting in which to explore the security issues that pertain to the realm of hypervisors. VirtualCert is a machine-checked model of virtualization that can be used to reason about isolation between operating systems in presence of cache-based side-channels. In contrast to the projects just mentioned VirtualCert abstracts away most implementations issues and specifies the effects of hypervisor actions axiomatically, in terms of preconditions and postconditions. We have developed, in the first place, a minimalistic idealized model of a hypervisor, and have formally proved that the hypervisor correctly enforces isolation between guest operating systems. For tractability and concreteness, we concentrate on memory management in paravirtualization platforms. Our model abstracts away many specifics of the underlying hardware and runtime environment such as I/O devices. Instead, our model focuses on the aspects that are most relevant for isolation properties, namely read and write resources on machine addresses, and is sufficiently complete to allow us to reason about isolation properties. Specifically, we show that an operating system can only read and modify memory it owns, and a non-influence property stating that the behavior of an operating system is not influenced by other operating systems. In addition, our model allows reasoning about availability; we have proved, under reasonable conditions, that all requests of a guest operating system to the hypervisor are eventually attended, so that no guest operating system waits indefinitely for a pending request. Overall, our verification effort shows that the model is adequate to reason about safety properties (read and write isolation), 2-safety properties (OS isolation), and liveness properties (availability). This work has been reported in our paper. Virtualization platforms, unfortunately, are often vulnerable to practical side-channel attacks. Cache attacks are a common class of side-channel attacks that use the cache as a side channel. Therefore, we have developed an extension of the idealized model in FM11 with a formalization of the cache and Translation Lookaside Buffer (TLB), a specific cache used to map virtual addresses to physical addresses. Then, drawing inspiration from physically observable cryptography, we consider an extended model of traces in which operating systems can draw observations on the history of the cache. The resulting model allows reasoning about the class of synchronous access-driven cache-based attacks; in particular, we prove that flushing the cache upon switching between guest operating systems ensures OS isolation and prevents such attacks. The main contribution of this work is a machine-checked proof of isolation in an idealized model of virtualization where the cache and the TLB may leak information. We have also stated and machine-checked a proof of transparency. Transparency states that the virtualization platform is a correct abstraction of the underlying hardware, in the sense that a guest operating system cannot distinguish whether it executes alone or together with other systems. Transparency is a 2-safety property; its formulation involves an erasure function which removes all the components of the states that do not belong to some fixed operating system. We define an appropriate erasure, establish its fundamental properties, and finally derive transparency. This work has been reported in our paper. The models and proofs described above have all been machine-checked in and the corresponding Coq code can be found in the of this site. Recently we have incorporated the treatment of errors into VirtualCert and proved that isolation theorems still apply. In addition, we have developed an executable specification of the hypervisor, and prove that it correctly implements the axiomatic model. The executable specification constitutes a first step towards a more realistic implementation of an hypervisor, and provides a useful tool for validating the axiomatic semantics developed in FM11 and CSF12.
Partners
VirtualCert is a research project in which collaborate Dr. Gilles Barthe from IMDEA Software, Spain, and a team of members of the Department of Computing Science (InCo), Gustavo Betarte, Juan Diego Campo and Carlos Luna.
Deliverables: COQ Code
The COQ modules containing the specification of the idealized model and the proofs of isolation and availability are available at VirtualCert
The COQ modules containing the specification of the idealized model extended with Cache and TLB, and the proofs of isolation and indistinguishability are available in VirtualCert (cache extensions).
The COQ modules containing the specification and implementation of the model with errors are available here.
Publications
Conferences
- G. Barthe; G. Betarte; J. D. Campo; C. Luna, Cache-leakage resilient OS isolation in an idealized model of virtualization. In IEEE 25th Computer Security Foundations Symposium (CSF), pp. 186-197, doi:10.1109/CSF.2012.17, 2012
- G. Barthe; G. Betarte; J. D. Campo; C. Luna, Formally verifying isolation and availability in an idealized model of virtualization. In Michael Butler & Wolfram Schulte, editors: FM 2011: Formal Methods, LNCS 6664, Springer-Verlag, pp. 231-245, doi:10.1007⁄978-3-642-21437-0.19, 2011.