Compositional security is a recognized central scientific challenge for trustworthy computing. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired end-to-end security property: an adversary may exploit complex interactions between components to compromise security. Such attacks have shown up in the wild in many different settings, including web browsers and infrastructure, network protocols and infrastructure, and application and systems software. While there has been progress on understanding secure composition in some settings, such as information flow control for non-interference-style properties, cryptographic
protocols, and certain classes of software systems, a number of important scientific questions pertaining to secure composition remain open. The broad goal of this project is to improve our scientific understanding of secure composition.
This project will focus on the following research directions.
Compositional Reasoning Principles for Higher-order Code. We propose to develop sound secure composition principles for trusted systems that interact with adversaries who have the capability to supply executable code to and modify code of the trusted system. We will build on prior work by Datta and collaborators on sound composition principles for trusted systems that interact with adversaries that can supply data (but not code) to tackle this problem.
Theoretical Categorization of Compositionality. We will generalize from the insights acquired during the development of compositional reasoning principles and prior technical work in the computer security community on challenges in composing certain specific classes of security
policies to arrive at semantic characterizations of classes of security policies that are and are not amenable to a compositional analysis. We plan to start from the security policy algebra in the prior work by Pincus and Wing, and expand the theory to larger classes of policy compositions.
Correspondence Between High-level Policies and Low-level Properties. We will develop a technical connection—a correspondence theorem—between high-level security policies (expressed either in the policy algebra or a logic) and lower level security properties expressed in our program logic. This result will connect our two lines of work and might also be useful in explaining failures of security policy composition in terms of failures of environmental assumptions. Case Studies. We will conduct a compositional analysis of a class of systems that combine trusted computing technology and memory protection mechanisms to provide strong security guarantees against powerful adversaries. We will also revisit the real-world examples in the Pincus- Wing paper using the new formalism.