Secure Composition of Untrusted Code
Secure Composition of Untrusted CodeJan Vitek
Sign up to use
Secure Composition of Untrusted Code

Secure Composition of Untrusted Code Wrappers and Causality Types

Sign up to use
Sign up to use
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."