Noninterference Analysis of Irreversible Systems and Reversible Systems Featuring both Nondeterminism and Probabilities

TL;DR

This paper extends noninterference analysis to systems with nondeterminism and probabilities, differentiating between irreversible and reversible systems using probabilistic bisimilarities.

Contribution

It introduces probabilistic variants of noninterference properties for both irreversible and reversible systems, extending prior models to include probabilities.

Findings

Extended noninterference properties to probabilistic systems.

Compared probabilistic noninterference with earlier non-probabilistic taxonomies.

Illustrated theory with a probabilistic smart contract lottery.

Abstract

The theory of noninterference supports the analysis of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on bisimilarity. In a nondeterministic setting, assessing noninterference through weak bisimilarity is adequate for irreversible systems, whereas for reversible ones branching bisimilarity has been recently proven to be more appropriate. In this paper we address the same two families of systems with the difference that probabilities come into play in addition to nondeterminism according to the alternating model of Hansson and Jonsson. For irreversible systems we extend the results of Aldini, Bravetti, and Gorrieri developed in a generative-reactive probabilistic setting, while for reversible systems we extend the results of Esposito, Aldini, Bernardo, and Rossi developed in a purely nondeterministic setting. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities for irreversible and reversible systems, respectively. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with earlier taxonomies. The adequacy of the extended noninterference theory is illustrated via a probabilistic smart contract lottery.