Compositional System Security in the Presence of Interface-Confined Adversaries (CMU-CyLab-10-004) Deepak Garg Jason Franklin Dilsun Kaynar Anupam Datta 10.1184/R1/6467828.v1 https://kilthub.cmu.edu/articles/journal_contribution/Compositional_System_Security_in_the_Presence_of_Interface-Confined_Adversaries_CMU-CyLab-10-004_/6467828 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. 2010-02-19 00:00:00 CyLab tech report