Secure Composition of Untrusted Code: Wrappers and Causality Types

The use of software components from untrusted or partially-trusted sources is becoming common. A user would like to know, for example, that they will not leak personal data to the net, but it is often 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. In [1] we introduced a process calculus with constrained interaction to express wrappers and discussed the precise formulation of their security properties. In this work we study verification of wrapper information flow properties. We present a causal type system that statically captures the allowed flows between wrapped potentially badly-typed components; we use the type system to prove that a non-trivial wrapper has the desired property.

[1] Secure Composition of Insecure Components, Peter Sewell and Jan Vitek. Computer Security Foundations Workshop, CSFW-12, June 1999.

LS Home page or Talks in 1999/2000