Mechanized Type-Based Enforcement of Non-Interference in Choreographic Languages

Eseguiamo un’analisi e un’enforcement type-based della non-interferenza in linguaggi coreografici. Partendo da una semantica di riferimento small-step per le coreografie, progettiamo un sistema di tipi parametrico rispetto alla policy (una gerarchia di livelli di sicurezza) che verifica, in modo statico, la conformità di un programma ai flussi d’informazione ammessi. Dimostriamo un teorema di soundness: se una coreografia è ben tipata rispetto a una policy, allora soddisfa la non-interferenza insensibile alla terminazione rispetto alla semantica di riferimento; in particolare, osservatori pubblici non possono dedurre informazioni segrete. Tutti i risultati principali sono meccanizzati in Lean 4.