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.

翻译：编排式编程从全局视角描述分布式协议，支持通过构造正确性合成局部行为。我们开发了一种策略参数化类型系统，该系统能够防止高安全级数据向低安全级观察者的信息泄露，通过程序计数器机制同时处理显式和隐式信息流。该系统通过约束生成重构过程上下文，从而支持递归过程。我们基于标准小步语义证明了终止不敏感的非干涉性。