Sciweavers

Share
ENTCS
2010

Compositional System Security with Interface-Confined Adversaries

8 years 5 months ago
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.
Deepak Garg, Jason Franklin, Dilsun Kirli Kaynar,
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2010
Where ENTCS
Authors Deepak Garg, Jason Franklin, Dilsun Kirli Kaynar, Anupam Datta
Comments (0)
books