Secure Communications Processing for Distributed Languages

Reference: Abadi, Fournet, Gonthier (1999). Compaq SRC / Microsoft Research / INRIA technical paper. Source file: Secure_communications_processing_for_dis.pdf. URL

Summary

Abadi, Fournet, and Gonthier formalize communications processing — the marshaling, unmarshaling, and cryptographic operations that wrap distributed language primitives like RPC and RMI — within a process calculus. They study how local communication semantics (single machine or protected network) can be extended transparently to hostile distributed networks through a generic cryptographic “wrapper” that operates like a firewall with an encrypting tunnel.

The technical core uses the join-calculus and its cryptographic extension, the sjoin-calculus, to translate high-level join-calculus processes into protected low-level sjoin-calculus processes that exchange encrypted messages. They prove a full-abstraction theorem showing the wrapping preserves observational equivalence — attackers on the public network cannot distinguish wrapped processes that behave the same locally.

Key Ideas

• Join-calculus as basis for concurrent/distributed language semantics.
• Sjoin-calculus adds symmetric encryption primitives.
• Wrapper as filter/firewall doing marshaling + encryption uniformly.
• Full-abstraction theorem: wrapping preserves equivalences.
• Security reasoned compositionally across distribution boundaries.

Connections

• Multi-Agent Systems
• Agent Communication Languages
• Language Workbenches
• Distributed Security
• Capability Security
• LangSec

Conceptual Contribution

• Claim: The communications-processing layer of a distributed language (marshalling + crypto) can be compiled automatically from a local-semantics specification in such a way that distribution becomes observationally transparent even under an active network attacker.
• Mechanism: Abadi, Fournet and Gonthier use the join-calculus for local semantics and the sjoin-calculus (join + symmetric crypto primitives) for the low-level network, defining a wrapper translation that implements channel communication via encrypted tunnels gated by a firewall-like filter. A full-abstraction theorem proves that two source programs are observationally equivalent iff their wrapped versions are, so security reasoning composes with functional reasoning.
• Concepts introduced/used: Join Calculus, Sjoin Calculus, Full Abstraction, Communications Processing, Cryptographic Wrapper, Observational Equivalence, Marshalling
• Stance: formal-semantic
• Relates to: Provides the calculus-level counterpart to language-engineering security efforts like The Halting Problems of Network Stack Insecurity and A Language-Based Approach To Prevent DDoS; its transparent-distribution agenda links to the actor-style transparency claims of Programming Erlang Second Edition and the SOL/SINS encrypted inter-agent channels in Architectural Patterns for Dependable Software Systems - SOL.

Tags

#security #process-calculus #distributed-systems #cryptography