Compositional System Security with Interface-Confined Adversaries

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 [27,21] 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 illustrated through a small fragment of an idealized file system.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Deepak Garg, Jason Franklin, Dilsun Kirli Kaynar, Anupam Datta
• Keywords: Compositional Reasoning, ENTCS 2010, Formal Framework, Larger Trusted Components