Biblio

System assurance is the justified confidence that a system functions as intended and is free of exploitable vulnerabilities, either intentionally or unintentionally designed or inserted as part of the system at any time during the life cycle. The computation and communication backbone of Internet of Things (IoT) devices and other cyber-physical systems (CPS) makes them vulnerable to classes of threats previously not relevant for many physical control and computational systems. The design of resilient IoT systems encompasses vulnerabilities to adversarial disruption (Security), behavior in an operational environments (Function), and increasing interdependencies (Connectedness). System assurance can be met only through a comprehensive and aggressive systems engineering approach. Engineering methods to "design in" security have been explored in the United States through two separate research programs, one through the Systems Engineering Research Center (SERC) and one through the Defense Advanced Research Process Agency (DARPA). This paper integrates these two programs and discusses how assurance practices can be improved using new system engineering and system design strategies that rely on both functional and formal design methods.

Cloud computing allows users to delegate data and computation to cloud service providers, at the cost of giving up physical control of their computing infrastructure. An attacker (e.g., insider) with physical access to the computing platform can perform various physical attacks, including probing memory buses and cold-boot style attacks. Previous work on secure (co-)processors provides hardware support for memory encryption and prevents direct leakage of sensitive data over the memory bus. However, an adversary snooping on the bus can still infer sensitive information from the memory access traces. Existing work on Oblivious RAM (ORAM) provides a solution for users to put all data in an ORAM; and accesses to an ORAM are obfuscated such that no information leaks through memory access traces. This method, however, incurs significant memory access overhead. This work is the first to leverage programming language techniques to offer efficient memory-trace oblivious program execution, while providing formal security guarantees. We formally define the notion of memory-trace obliviousness, and provide a type system for verifying that a program satisfies this property. We also describe a compiler that transforms a program into a structurally similar one that satisfies memory trace obliviousness. To achieve optimal efficiency, our compiler partitions variables into several small ORAM banks rather than one large one, without risking security. We use several example programs to demonstrate the efficiency gains our compiler achieves in comparison with the naive method of placing all variables in the same ORAM.