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.

翻译：非干扰理论支持多级安全系统中安全计算的分析。经典的基于等价关系的非干扰方法主要依赖于互模拟等价。在非确定性设置下，通过弱互模拟等价评估非干扰对于不可逆系统是充分的，而对于可逆系统，分支互模拟等价最近被证明更为合适。本文研究相同两类系统，区别在于根据Hansson和Jonsson的交替模型，概率与不确定性共同作用。对于不可逆系统，我们扩展了Aldini、Bravetti和Gorrieri在生成反应概率设置下发展的结果；对于可逆系统，我们扩展了Esposito、Aldini、Bernardo和Rossi在纯非确定性设置下发展的结果。我们采用分别针对不可逆系统和可逆系统的弱互模拟等价与分支互模拟等价的概率变体，重新定义了非干扰性质。随后，我们研究了这些性质的分类体系、保持性与组合性，并与先前分类体系进行了比较。通过一个概率智能合约彩票案例，阐释了扩展非干扰理论的适用性。