On the Universally Composable Security of OpenStack


October 03, 2019


Hoda Maleki (University of Connecticut); Kyle Hogan (MIT); Reza Rahaeimehr (University of Connecticut); Ran Canetti, Mayank Varia, Jason Hennessey (Boston University and NetApp); Marten van Dijk (University of Connecticut); Haibin Zhang (UMBC)

IEEE Secure Development Conference September 25 - 27, 2019 McLean, VA 

We initiate an effort to provide a rigorous, holisticand modular security analysis of OpenStack. OpenStack is theprevalent open-source, non-proprietary package for managingcloud services and data centers. It is highly complex and consistsof multiple inter-related components which are developed byseparate, loosely coordinated groups. All of these properties makethe security analysis of OpenStack both a worthy mission and achallenging one. We base our modeling and security analysis inthe universally composable (UC) security framework. This allowsspecifying and proving security in a modular way — a crucialfeature when analyzing systems of such magnitude. Our analysishas the following key features: 

1) It isuser-centric: It stresses the security guarantees givento users of the system in terms of privacy, correctness, andtimeliness of the services.

2) It considers the security of OpenStack even when some ofthe components are compromised. This departs from thetraditional design approach of OpenStack, which assumesthat all services are fully trusted. 

3) It ismodular: It formulates security properties for individualcomponents and uses them to prove security properties ofthe overall system. 

Specifically, this work concentrates on the high-level struc-ture of OpenStack, leaving the further formalization and moredetailed analysis of specific OpenStack services to future work.Specifically, we formulate ideal functionalities that correspond tosome of the core OpenStack modules, and then proves securityof the overall OpenStack protocol given the ideal components. As demonstrated within, the main challenge in the high-level design is to provide adequately fine-grained scoping ofpermissions to access dynamically changing system resources.We demonstrate security issues with current mechanisms in caseof failure of some components, propose alternative mechanisms,and rigorously prove adequacy of then new mechanisms within ourmodeling.


A copy of the paper can be found at: link.