Noninterference Analysis of Reversible Probabilistic Systems

Noninterference theory supports the analysis of secure computations in multi-level security systems. In the nondeterministic setting, the approach to noninterefence based on weak bisimilarity has turned out to be inadequate for reversible systems. This drawback can be overcome by employing a more expressive semantics, which has been recently proven to be branching bisimilarity. In this paper we extend the result to reversible systems that feature both nondeterminism and probabilities. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities. 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 resulting noninterference theory for reversible systems is illustrated via a probabilistic smart contract example.