Type-Based Enforcement of Non-Interference for Choreographic Programming

TL;DR

This paper introduces a type system for choreographic programming that enforces non-interference, preventing information leaks across security levels by analyzing explicit and implicit flows, and proves its correctness.

Contribution

It presents a novel policy-parametric type system for choreographies that ensures non-interference, including recursive procedures, with formal termination-insensitive proof.

Findings

The type system effectively prevents information leaks in choreographies.

It supports recursive procedures through constraint-based context reconstruction.

The system guarantees termination-insensitive non-interference.

Abstract

Choreographies describe distributed protocols from a global viewpoint, enabling correct-by-construction synthesis of local behaviours. We develop a policy-parametric type system that prevents information leaks from high-security data to low-security observers, handling both explicit and implicit flows through a program-counter discipline. The system supports recursive procedures via a procedure context that we reconstruct through constraint generation. We prove termination-insensitive non-interference with respect to a standard small-step semantics.