Type-Based Enforcement of Non-Interference for Choreographic Programming
Programming Languages
2026-02-26 v1 Cryptography and Security
Distributed, Parallel, and Cluster Computing
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.
Keywords
Cite
@article{arxiv.2602.21630,
title = {Type-Based Enforcement of Non-Interference for Choreographic Programming},
author = {Marco Bertoni and Saverio Giallorenzo and Marco Peressotti},
journal= {arXiv preprint arXiv:2602.21630},
year = {2026}
}