Secure composition of untrusted code: box π, wrappers, and causality types

摘要: Software systems are becoming heterogeneous: instead of a small number large programs from well-established sources, user's desktop may now consist many smaller components that interact in intricate ways. Some will be downloaded the network sources only partially trusted. A user would like to know security properties hold, e.g., personal data is not leaked net, but it typically infeasible verify such well-behaved. Instead, they must executed secure environment provides fine-grain control allowable interactions between them, and other system resources.In this paper, we consider problem assembling concurrent software untrusted or trusted off-the-shelf components, using wrapper encapsulate enforce policies. We introduce model programming language, box-π calculus, supports composition enforcement information flow Several example wrappers expressed calculus; explore delicate guarantee. present novel causal type statically captures allowed flows wrapped possibly-badly-typed components; use prove an ordered pipeline enforces property.