Biblio

We initiate an effort to provide a rigorous, holistic and modular 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 worthy mission and a challenging one. We base our modeling and security analysis in the universally composable (UC) security framework. This allows specifying and proving security in a modular way – a crucial feature when analyzing systems of such magnitude. 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 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 prove security properties of the overall system. Specifically, this work concentrates on the high-level structure of OpenStack, leaving the further formalization and more detailed analysis of specific OpenStack services to future work. Specifically, we formulate ideal functionalities that correspond to some of the core OpenStack modules, and then proves security of 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 of permissions to access dynamically changing system resources. We demonstrate security issues with current mechanisms in case of failure of some components, propose alternative mechanisms, and rigorously prove adequacy of then new mechanisms within our modeling.

We present a methodology for using the EasyCrypt proof assistant (originally designed for mechanizing the generation of proofs of game-based security of cryptographic schemes and protocols) to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework. This allows, for the first time, the mechanization and formal verification of the entire sequence of steps needed for proving simulation-based security in a modular way: Specifying a protocol and the desired ideal functionality; Constructing a simulator and demonstrating its validity, via reduction to hard computational problems; Invoking the universal composition operation and demonstrating that it indeed preserves security. We demonstrate our methodology on a simple example: stating and proving the security of secure message communication via a one-time pad, where the key comes from a Diffie-Hellman key-exchange, assuming ideally authenticated communication. We first put together EasyCrypt-verified proofs that: (a) the Diffie-Hellman protocol UC-realizes an ideal key-exchange functionality, assuming hardness of the Decisional Diffie-Hellman problem, and (b) one-time-pad encryption, with a key obtained using ideal key-exchange, UC-realizes an ideal secure-communication functionality. We then mechanically combine the two proofs into an EasyCrypt-verified proof that the composed protocol realizes the same ideal secure-communication functionality. Although formulating a methodology that is both sound and workable has proven to be a complex task, we are hopeful that it will prove to be the basis for mechanized UC security analyses for significantly more complex protocols and tasks.

We construct the first fully succinct garbling scheme for RAM programs, assuming the existence of indistinguishability obfuscation for circuits and one-way functions. That is, the size, space requirements, and runtime of the garbled program are the same as those of the input program, up to poly-logarithmic factors and a polynomial in the security parameter. The scheme can be used to construct indistinguishability obfuscators for RAM programs with comparable efficiency, at the price of requiring sub-exponential security of the underlying primitives. In particular, this opens the door to obfuscated computations that are sublinear in the length of their inputs. The scheme builds on the recent schemes of Koppula-Lewko-Waters and Canetti-Holmgren-Jain-Vaikuntanathan [STOC 15]. A key technical challenge here is how to combine the fixed-prefix technique of KLW, which was developed for deterministic programs, with randomized Oblivious RAM techniques. To overcome that, we develop a method for arguing about the indistinguishability of two obfuscated randomized programs that use correlated randomness. Along the way, we also define and construct garbling schemes that offer only partial protection. These may be of independent interest.