Information leakage detection in boundary ambients

A variant of Mobile Ambient Calculus is introduced, called Boundary Ambient, to model multilevel security policies. Ambients that may guarantee to properly protect their content are explicitly identified as boundaries: a boundary can be seen as a resource access manager for confidential data. In this setting, we define a notion of non-interference which captures the absence of any (both direct and indirect) information leakage. Then, we guarantee non-interference by extending a control flow analysis that computes an over approximation of all ambients and capabilities that may be affected by the actual values of high level data.