A variant of the Mobile Ambient calculus, called Boundary Ambients, is introduced, supporting the modelling of multi-level 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, absence of direct information leakage is granted as soon as the initial process satisfies some syntactic conditions. We then give a new notion of non-interference for Boundary Ambients aiming at capturing indirect flows, too. We design a Control Flow Analysis that computes an over-approximation of all ambients that may be affected at run-time by high-level data and we show that this static analysis can be used to enforce non-interference, i.e., to statically detect that no (direct or indirect) information leakage is ever possible at run-time.
|Titolo:||Information flow security in boundary ambients|
BRAGHIN, CHIARA (Primo)
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2008|
|Digital Object Identifier (DOI):||10.1016/j.ic.2007.12.001|
|Appare nelle tipologie:||01 - Articolo su periodico|