Confining Data and Processes in Global Computing Applications
Rocco De Nicola, Daniele Gorla and Rosario Pugliese
Paper
appeared in
Science of Computer Programming.
An extended abstract appeared in ACM SAC'04.
Abstract:
A programming notation is introduced that can be used for
protecting secrecy and integrity of data in global computing
applications. The approach is based on the explicit annotations of
data and network nodes. Data are tagged with information about the
allowed movements, network nodes are tagged with information about
the nodes that can send data and spawn processes to them. The
annotations are used to \emph{confine} movements of data and processes.
The approach is illustrated by applying it to three paradigmatic
calculi for global computing, namely cKLAIM (a calculus at the
basis of KLAIM), Dpi\ (a distributed version of the
pi-calculus) and Mobile Ambients Calculus. For all of these
formalisms, it is shown that their semantics guarantees that
computations proceed only while respecting confinement
constraints. Namely, it is proven that, after successful static
type checking, data can reside at and cross only authorised nodes.
``Local'' formulations of this property where only relevant
sub-nets type check are also presented. Finally, the theory is
tested by using it to model secure behaviours of a UNIX-like
multiuser system.
@Article{DGP:SCP06,
author = {R. {De Nicola} and D. Gorla and R. Pugliese},
title = {Confining Data and Processes in Global Computing Applications},
journal = {Science of Computer Programming},
volume = {63},
number = {1},
pages = {57--87},
year = {2006},
publisher = {Elsevier},
}
Home page /
Publications