Anupam Datta

Programming Language Methods for Compositional Security

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. These lectures will report on progress on applying programming language methods to address this problem and will be divided into two parts:

Part I: Protocol Composition Logic
Protocol Composition Logic (PCL) is a logic for proving security properties of network protocols that use public and symmetric key cryptography. The logic is designed around a process calculus with actions for possible protocol steps including generating new random numbers, sending and receiving messages, and performing decryption and digital signature verifcation actions. The proof system consists of axioms about individual protocol actions and inference rules that yield assertions about protocols composed of multiple steps. Although assertions are written only using the steps of the protocol, the logic is sound in a strong sense: each provable assertion involving a sequence of actions holds in any protocol run containing the given actions and arbitrary additional actions by a malicious adversary. This approach lets us prove security properties of protocols under attack while reasoning only about the actions of honest parties in the protocol. PCL supports compositional reasoning about complex security protocols and has been applied to a number of industry standards including SSL/TLS, IEEE 802.11i and Kerberos V5.

Part II: Logic of Secure Systems
We present a formal framework for compositional reasoning about secure systems. A key insight is to view a trusted system in terms of the interfaces that the various components expose: larger trusted components are built by combining interface calls in known ways; the adversary is confined to the interfaces it has access to, but may combine interface calls without restriction. Compositional reasoning for such systems is based on an extension of rely-guarantee reasoning for system correctness to a setting that involves an adversary whose exact program is not known. It generalizes prior work on Protocol Composition Logic. At a technical level, the approach is based on an expressve concurrent programming language with recursive functions for modeling interfaces and a logic of programs in which compositional reasoning principles are formalized and proved sound with respect to trace semantics. The methods are applied to representative examples of web-based systems and network protocols. As a running example, we consider an example mashup system and present a modular proof of integrity in the presence of a class of interface-confined adversaries. We also demonstrate the generality of our methods by presenting a modular proof of symmetric key Kerberos V5 in the presence of a symbolic adversary.


References:

Č
ć
ď
Anupam Datta,
Jun 19, 2010, 3:51 PM
ć
ď
Anupam Datta,
Jun 19, 2010, 6:11 AM
ć
ď
Anupam Datta,
Jun 19, 2010, 6:12 AM
ċ
ď
Anupam Datta,
Jun 16, 2010, 1:20 AM
Ċ
ď
Anupam Datta,
Jun 11, 2010, 9:49 AM
Ċ
ď
Anupam Datta,
Jun 11, 2010, 9:49 AM
Ċ
ď
Anupam Datta,
Jun 11, 2010, 9:49 AM
Comments