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.
Information flow security in boundary ambients / C. Braghin, A. Cortesi, R. Focardi. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 206:2-4(2008), pp. 460-489.
Information flow security in boundary ambients
C. BraghinPrimo
;
2008
Abstract
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.