[Prev][Next][Index][Thread]
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
----------
Abstract:
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
http://www.cs.purdue.edu/homes/jv/pub/wrap99.ps.gz
http://www.cl.cam.ac.uk/users/pes20/index.html#WRAP