Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.ic.2007.12.001 | Inf. Comput. |
Keywords | Field | DocType |
mobile ambient calculus,multi-level security policy,direct information leakage,high-level data,control flow analysis,initial process,indirect flow,information flow security,confidential data,information leakage,boundary ambients,satisfiability,static analysis,information flow | Information flow (information theory),Discrete mathematics,Information leakage,Computer security,Computer science,Control flow,Static analysis,Control flow analysis,Security policy,Ambient calculus,Distributed computing | Journal |
Volume | Issue | ISSN |
206 | 2-4 | Information and Computation |
Citations | PageRank | References |
8 | 0.69 | 26 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chiara Braghin | 1 | 105 | 8.86 |
| Agostino Cortesi | 2 | 791 | 66.19 |
| Riccardo Focardi | 3 | 1229 | 99.99 |