Confining Data and Processes in Global Computing Applications.
Daniele Gorla
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, while network nodes are tagged with information
about which nodes can send data and spawn processes over them. These
restrictions/annotations are used to confine the movement of data and
processes. First, a general framework for describing global computing
applications is proposed and the issues related to confinement are
discussed in such a context. Then, the general framework is
instantiated onto three models for process interaction and mobility,
namely cKlaim (thekernel of Klaim), DPi (a
distributed version of the Pi-calculus) and M-cube (a variant of the
Mobile Ambient Calculus). For all of these formalisms, it is shown
that their semantics guarantees that computations proceed only while
respecting confinement constraints. It is proven that, after
successful static type checking, data can reside at, and cross only,
authorized nodes. Possible "localizations" of this property are
discussed that require checking only relevant sub-nets.