Skip to main content

Technical Reports: CMU-CyLab-10-004

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

Abstract

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