Noninterference Analysis of Irreversible Systems and Reversible Systems Featuring both Nondeterminism and Probabilities
For security researchers, this provides a formal framework to analyze information flow in probabilistic systems, but it is an incremental extension of existing bisimilarity-based approaches.
The paper extends noninterference analysis to systems combining nondeterminism and probabilities, using probabilistic weak bisimilarity for irreversible systems and probabilistic branching bisimilarity for reversible systems. It establishes a taxonomy of properties, preservation and compositionality results, and validates the theory on a probabilistic smart contract lottery.
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.