Noninterference Analysis of Irreversible or Reversible Systems with Nondeterminism and Probabilities
Andrea Esposito, Alessandro Aldini, Marco Bernardo
TL;DR
This paper extends noninterference analysis to probabilistic, nondeterministic, and reversible systems within the strictly alternating $HJ90$ framework. It defines probabilistic weak and branching bisimilarities to capture security properties across irreversible and reversible settings, respectively, and develops a taxonomy of noninterference notions with preservation and compositionality analyses. The authors adapt classical two-level security concepts (high/low actions) to probabilistic processes, derive congruence results, and connect backward/reversibility semantics to branching bisimilarity. The approach is demonstrated via a probabilistic smart contract lottery, highlighting practical implications for secure information flows in blockchain-like environments. Overall, the work generalizes previous probabilistic noninterference results to a richer setting and provides tools for modular verification and reversibility-aware security reasoning.
Abstract
Noninterference theory 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 the nondeterministic taxonomy. The adequacy of the extended noninterference theory is illustrated via a probabilistic smart contract lottery.