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