Secure Composition of Untrusted Code: Wrappers and Causality Types

We consider the problem of assembling concurrent software systems from untrusted or partially trusted o -the-shelf components, using wrapper programs to encapsulate components and enforce security policies. In previous work we introduced the box- process calculus with constrained interaction to express wrappers and discussed the rigorous formulation of their security properties. This paper addresses the verication of wrapper information ow properties. We present a novel causal type system that statically captures the allowed ows between wrapped possiblybadly-typed components; we use it to prove that an example unidirectional- ow wrapper enforces a causal ow property.

• Type: Conference
• Year: 2000
• Where: CSFW
• Authors: Peter Sewell, Jan Vitek
• Keywords: Causal Ow Property, CSFW 2000, Ow Wrapper, Security Privacy, Wrapper Information Ow