Towards Security Analysis of OpenStack

OpenStack is the prevalent open-source, non-proprietary package for managing cloud services and data centers. It is highly complex and consists of multiple inter-related components which are developed by separate, loosely coordinated groups. All of these properties make the security analysis of OpenStack both a crucial mission and a challenging one. In this dissertation, we demonstrate how we can provide a rigorous, perceptible and holistic security analysis of OpenStack. We base our modeling and security analysis in the universally composable (UC) security framework, which has been so far used mainly for analyzing the security of cryptographic protocols. Indeed, demonstrating how the UC framework can be used to argue about security-sensitive systems which are mostly non-cryptographic, in nature, is one of the main contributions of this work. Our analysis has the following key features: 1- It is user-centric: It stresses the security guarantees given to users of the system, in terms of privacy, correctness, and timeliness of the services. 2- It provides defense in depth: It considers the security of OpenStack even when some of the components are compromised. This departs from the traditional design approach of OpenStack, which assumes that all services are fully trusted. 3- It is modular: It formulates security properties for individual components and uses them to assert security properties of the overall system. We formulate ideal functionalities that correspond to several OpenStack modules and then prove the security of the overall OpenStack protocol given the ideal components. The modeling paves the way toward a comprehensive analysis of OpenStack: it is extensible to the addition of new components and modular to an intra-component analysis. It turns out that some salient issues come up even at this relatively high level of representation and analysis. Specifically, we demonstrate that the scoping of permissions given by users to proxy tokens causes the overall security to fail as soon as any one of the components fails. We propose an alternative, more finely scoped token mechanism and assert that the new mechanisms suffice for regaining overall security even when some of the components are faulty