Title:

A Causal Type System for Ambient Movements

 Abstract:

The Ambient Calculus was developed by Cardelli and Gordon as a
framework for mobile computation where ``ambients'', containing active
processes (and not just passive code), can move around---in and out of
other ambients.  In this view, the following question becomes a main
security concern: Is it possible for a given ambient to end up inside
another given ambient?

We present a type system for the calculus, parameterized by a set of
security constraints: static ones concerning where a given ambient may
reside, and dynamic ones expressing where a given ambient may be
dissolved.  A soundness result then guarantees that a well-typed
process never violates these constraints; additionally it ensures that
communicating subprocesses agree on their ``topic of conversation''.

The type system employs a notion of causality in that processes are
assigned ``behaviors''.  We argue that this significantly increases
the precision of the analysis and compensates for the lack of
``co-capabilities'' (an otherwise increasingly popular extension to
the ambient calculus); also it allows an ambient to hold multiple
topics of conversation.

Based on techniques borrowed from finite automata theory, type
checking of type-annotated processes is decidable. Under certain quite
natural restrictions, type inference is also possible.