Secure composition of insecure components

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 down-loaded 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 infeasible 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. We study such wrappers, focusing 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