Compositional System Security with Interface-Confined Adversaries.

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 [Misra, J. and K.M. Chandy, Proofs of networks of processes, IEEE Transactions on Software Engineering 7 (1981), pp. 417–426; Jones, C.B., Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS) 5 (1983), pp. 596–619] 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. [Copyright &y& Elsevier]