Technical reports

Secure composition of untrusted code: wrappers and causality types

Peter Sewell, Jan Vitek

November 1999, 36 pages

DOI: 10.48456/tr-478

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-π 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.

Full text

PS (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-478,
  author =	 {Sewell, Peter and Vitek, Jan},
  title = 	 {{Secure composition of untrusted code: wrappers and
         	   causality types}},
  year = 	 1999,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-478.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-478},
  number = 	 {UCAM-CL-TR-478}
}