Skip to main content

Compositional Security

Researchers: Anupam Datta, Limin Jia, Amit Vasudevan, Sagar Chaki

Research Area: Trustworthy Computing Platforms and Devices

Cross Cutting Thrusts: Formal Methods | Software Security

Abstract

Scope: The security universe includes a large class of *computer systems*(cryptographic protocols, trusted computing systems, hypervisors, virtual machine monitors, and Web browsers, to name a few) that are designed to provide *security properties* in the presence of actively interfering * adversaries*. A unifying theme of this project is to develop *theories of security* that include formal models of systems, adversaries, and properties, and support rigorous analyses and principled design of secure systems. Most notably, we have developed *composition techniques* that enable us to analyze and design complex systems with known global security properties from smaller components with known local security properties without a requirement to fully re-analyze the components. Indeed scalability and composability have recently been recognized as one of the five hardest problems in the science of security. We have applied these methods to analyze security properties of cryptographic protocols for authentication, key exchange, and remote attestation (with hardware support) as well as to analyze properties of hypervisors. Outcomes: We have developed a *domain-independent theory of compositional security*that supports compositional analysis of a general class of systems against a class of adversaries whose capabilities are defined in terms of the system interfaces to which they have access. The technical approach is based on a logic of programs. We have applied the logic to analyze attestation protocols for trusted computing platforms discovering an insecure interaction between two standard protocols. We have further generalized the logic to support higher-order systems where adversaries can supply code to the system (e.g., a Web browser or hypervisor with call-back functions) in addition to data. This line of work generalizes our prior work on *Protocol Composition Logic(PCL) - *a domain-specific logic of programs useful for proving confidentiality and authentication properties of cryptographic protocols.Analysis using PCL has influenced three industry standards: IEEE 802.11i wireless authentication (based on our work), IETF GDOI secure group communication (based on an NRL-Kestrel study) and the IEEE 802.11s mesh security architecture (based on a Motorola study).