|Title:||Compositional System Security in the Presence of Interface-Confined Adversaries|
|Authors:||Deepak Garg, Jason Franklin, Dilsun Kaynar, Anupam Datta|
|Publication Date:||February 19, 2010|
This paper presents 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 [1, 2] to a setting that involves an adversary whose exact program is not known. At a technical level, the paper presents an expressive 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.
Full Report: CMU-CyLab-10-004
Related Project : Principled Approach to Web Security