Secure Composition of Untrusted Code Wrappers and Causality Types

Abstract: "We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. In previous work we introduced the 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 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."