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.

A hardware Trojan is a malicious circuit inserted into a device by a malicious designer or manufacturer in the circuit design or fabrication phase. With the globalization of semiconductor industry, more and more chips and devices are designed, integrated and fabricated by untrusted manufacturers, who can potentially insert hardware Trojans for launching attacks after the devices are deployed. Moreover, the most damaging attack in a smart grid is a large scale electricity failure, which can cause very serious consequences that are worse than any disaster. Unfortunately, this attack can be implemented very easily by synchronized hardware Trojans acting as a collective offline time bomb; the Trojans do not need to interact with one another and can affect a large fraction of nodes in a power grid. More sophisticatedly, this attack can also be realized by online hardware Trojans which keep listening to the communication channel and wait for a trigger event to trigger their malicious payloads; here, a broadcast message triggers all the Trojans at the same time. In this paper, we address the offline synchronized hardware Trojan attack, as it does not require the adversary to penetrate the power grid network for sending triggers. We classify two types of offline synchronized hardware Trojan attacks as type A and B: type B requires communication between different nodes, and type A does not. The hardware Trojans needed for type B turn out to be much more complex (and therefore larger in area size) than those for type A. In order to prevent type A attacks we suggest to enforce each power grid node to work in an unique time domain which has a random time offset to Universal Coordinated Time (UTC). This isolation principle can mitigate type A offline synchronized hardware Trojan attacks in a smart grid, such that even if hardware Trojans are implanted in functional units, e.g. Phasor Measurement Units (PMUs) and Remote Terminal Units (RTUs), they can only cause a minimal damage, i.e. sporadic single node failures. The proposed solution only needs a trusted Global Positioning System (GPS) module which provides the correct UTC together with small additional interface circuitry. This means that our solution can be used to protect the current power grid infrastructure against type A offline attacks without replacing any untrusted functional unit, which may already have embedded hardware Trojans.

Clone product injection into supply chains causes serious problems for industry and customers. Many mechanisms have been introduced to detect clone products in supply chains which make use of RFID technologies. This article gives an overview of these mechanisms, categorizes them by hardware change requirements, and compares their attributes.

Critical resource sharing among multiple entities in a processing system is inevitable, which in turn calls for the presence of appropriate authentication and access control mechanisms. Generally speaking, these mechanisms are implemented via trusted software "policy checkers" that enforce certain high level application-specific "rules" to enforce a policy. Whether implemented as operating system modules or embedded inside the application ad hoc, these policy checkers expose additional attack surface in addition to the application logic. In order to protect application software from an adversary, modern secure processing platforms, such as Intel's Software Guard Extensions (SGX), employ principled hardware isolation to offer secure software containers or enclaves to execute trusted sensitive code with some integrity and privacy guarantees against a privileged software adversary. We extend this model further and propose using these hardware isolation mechanisms to shield the authentication and access control logic essential to policy checker software. While relying on the fundamental features of modern secure processors, our framework introduces productive software design guidelines which enable a guarded environment to execute sensitive policy checking code - hence enforcing application control flow integrity - and afford flexibility to the application designer to construct appropriate high-level policies to customize policy checker software.

We introduce a Markov-model-based framework for Moving Target Defense (MTD) analysis. The framework allows modeling of a broad range of MTD strategies, provides general theorems about how the probability of a successful adversary defeating an MTD strategy is related to the amount of time/cost spent by the adversary, and shows how a multilevel composition of MTD strategies can be analyzed by a straightforward combination of the analysis for each one of these strategies. Within the proposed framework we define the concept of security capacity which measures the strength or effectiveness of an MTD strategy: the security capacity depends on MTD specific parameters and more general system parameters. We apply our framework to two concrete MTD strategies.