causal wrapper types

We would like to announce the technical report

   Secure Composition of Untrusted Code:
       Wrappers and Causality Types

Peter Sewell    - University of Cambridge
Jan Vitek       - Purdue University



We consider the problem of assembling concurrent software systems from
untrusted or partially trusted off-the-shelf components, using
\emph{wrapper programs} to encapsulate  components and enforce
security policies. In [1] we introduced the \emph{box-$\pi$}
process calculus with constrained interaction to express wrappers and
discussed the rigorous formulation of their security properties. 
This paper addresses the verification of wrapper information
flow properties. We present a novel \emph{causal type system} that
statically captures the allowed flows between wrapped
possibly-badly-typed components; we use it to prove that a
unidirectional-flow wrapper enforces a causal flow property.

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

Technical Report 478, Computer Laboratory, University of Cambridge,
available from