Causal Type System for Ambient Movements
Torben Amtoft · 2006
The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code. 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 subject reduction property 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 (in contrast to other approaches) 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. 1