Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Type-Based Enforcement of Non-Interference for Choreographic Programming

Marco Bertoni, Saverio Giallorenzo, Marco Peressotti

TL;DR

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 is developed.

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.

Type-Based Enforcement of Non-Interference for Choreographic Programming

TL;DR

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 is developed.

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.
Paper Structure (30 sections, 2 theorems, 9 equations, 2 figures)

This paper contains 30 sections, 2 theorems, 9 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Our approach.
  3. Structure of the Paper.
  4. Preliminaries on Choreographies
  5. Syntax
  6. Semantics
  7. Type System
  8. Soundness
  9. Natural Semantics.
  10. Attacker Observation Model.
  11. Well-formed Procedure Context.
  12. Well-typed Security Procedure Context.
  13. Deterministic Expressions.
  14. Instrumented Choreographies
  15. Instrumented stores.
  16. ...and 15 more sections

Key Result

theorem thmcountertheorem

Let $C$ be a choreography that is well-typed under the judgement $\Delta;\Gamma;\bot \vdash C$. Given two choreographic stores $\Sigma_1, \Sigma_2$, satisfying the $low$-equivalence relation $\Sigma_1 \equiv^\Gamma_{low} \Sigma_2$, suppose there exist terminating executions: then the resulting stores satisfy the relation $\Sigma'_1 \equiv^\Gamma_{low} \Sigma'_2$.

Figures (2)

  • Figure 1: Operational Semantics.
  • Figure 2: Typing Judgement.

Theorems & Definitions (2)

  • theorem thmcountertheorem: Termination-Insensitive Non-Interference
  • theorem thmcountertheorem: Well-typedness of the generated procedure context