Technical reports
Secure composition of insecure components
Peter Sewell, Jan Vitek
April 1999, 44 pages
DOI: 10.48456/tr-463
Abstract
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user’s desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g. that personal data is not leaked to the net, but it is typically infaesible to verify that such components are well-behaved. Instead they must be executed in a secure environment, or wrapper, that provides fine-grain control of the allowable interactions between them, and between components and other system resources.
In this paper we study such wrappers, focussing on how they can be expressed in a way that enables their security properties to be stated and proved rigorously. We introduce a model programming language, the box-π calculus, that supports composition of software components and the enforcement of security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee.
Full text
PS (0.2 MB)
BibTeX record
@TechReport{UCAM-CL-TR-463, author = {Sewell, Peter and Vitek, Jan}, title = {{Secure composition of insecure components}}, year = 1999, month = apr, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-463.ps.gz}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-463}, number = {UCAM-CL-TR-463} }