Ambient Calculus

Origin. Cardelli and Gordon (1998). Mobile computation in hierarchical spaces. Ambients as boundaries. Movement primitives. Foundation for mobile security.

Models. Ambients contain processes and sub-ambients. Movement: in, out, open. Hierarchy changes dynamically. Capability-based.

Formalism.

Syntax: P ::= 0 | P | Q | !P | (νn)P | n[P] | M.P

Ambient: n[P]: ambient named n containing P. Boundary with interior.

Capabilities: in n: enter ambient n. out n: exit ambient n. open n: dissolve n's boundary.

Capability prefix: M.P: perform M then continue as P. M ::= in n | out n | open n

Movement (in): n[in m.P | Q] | m[R] → m[n[P | Q] | R] n enters m.

Movement (out): m[n[out m.P | Q] | R] → n[P | Q] | m[R] n exits m.

Opening: open n.P | n[Q] → P | Q Dissolve boundary.

Structural congruence: P | 0 ≡ P n[(νm)P] ≡ (νm)n[P] (if m ≠ n) Standard rules.

Types: Ambient types: restrict capabilities. Immobile, locked ambients. Security properties.

Symbols.

Symbol	Unicode	Name	Meaning
n[P]	—	Ambient	Named boundary
in n	—	Enter	Move into n
out n	—	Exit	Move out of n
open n	—	Open	Dissolve n

Metatheory. The calculus is Turing complete, and Cardelli and Gordon showed that the fragment with movement and opening alone, before any communication primitive is added, already encodes Turing machines; their encoding of the asynchronous π-calculus uses the calculus extended with local communication. Its specification language is the ambient logic (Cardelli and Gordon, POPL 2000), a spatial modal logic with a location modality n[φ] and a composition adjunct φ ▷ ψ reading "put in parallel with any process satisfying φ, the result satisfies ψ". Sangiorgi (POPL 2001) proved that the equivalence induced by the ambient logic is intensional: logically equivalent processes are structurally congruent, so the logic separates processes that no context can tell apart, and it is strictly finer than barbed congruence. Charatonik, Dal Zilio, Gordon, Mukhopadhyay and Talbot (2001) settled model checking, showing it PSPACE-complete for the replication-free calculus against the logic without the composition adjunct, and undecidable once either replication or the adjunct is admitted. Merro and Zappa Nardelli (2005) gave the first labelled-transition characterization of reduction barbed congruence.

Applies to. Mobile code security. Firewalls. Administrative domains. Distributed systems. Web services.

Limitations. An ambient boundary is not a security boundary: any process holding the capability open n dissolves n without n's consent, and in n likewise moves an ambient into a host that never agreed to receive it. These grave interferences are what motivated Levi and Sangiorgi's safe ambients, which add co-capabilities so that both parties must consent. Movement is subjective — an ambient moves itself and cannot be moved — so objective mobility must be encoded. The ambient logic is intensional, distinguishing contextually equivalent processes, and so does not serve as a specification language for behaviour alone; and its full model-checking problem is undecidable. Barbed congruence has no easy proof method: a labelled characterization arrived only seven years after the calculus and requires an elaborate transition system. Nothing in the calculus expresses failure, latency or bandwidth, the properties distribution is chosen for.