Security boundaries in mobile ambients

A new notion of security boundary is introduced to model multilevel security policies in the scenario of mobile systems, within Cardelli and Gordon's ''pure'' mobile ambients calculus. Information leakage may be expressed in terms of the possibility for a hostile ambient to access confidential data that are not protected inside a security boundary. A control flow analysis is defined, as a refinement of the Hansen-Jensen-Nielsons's CFA, that allows to properly capture boundary crossings. In this way, direct information leakage may be statically detected.