The theory of noninterference supports the analysis and the execution of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics. We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations. As illustrated via a database management system example, the activation of backward computations may trigger information flows that are not observable when proceeding in the standard forward direction. To capture the effects of back and forth computations, it is necessary to switch to a more expressive semantics that, in an interleaving framework, has been proven to be branching bisimilarity in a previous work by De Nicola, Montanari, and Vaandrager. In this paper we investigate a taxonomy of noninterference properties based on branching bisimilarity along with their preservation and compositionality features, then we compare it with the classical hierarchy based on weak bisimilarity.

翻译：无干扰理论支持多级安全系统中安全计算的分析与执行。经典的基于等价关系的无干扰方法主要依赖弱互模拟语义。我们证明，在可逆计算存在的情况下，该方法不足以识别潜在的隐蔽信道。通过数据库管理系统示例可说明，在执行标准正向计算时无法观察到的信息流，可能因逆向计算的激活而触发。为捕捉正反向计算的效果，需要采用更具表现力的语义——在先前的De Nicola、Montanari和Vaandrager的工作中，这种语义在交错框架下已被证明是分支互模拟。本文研究基于分支互模拟的无干扰属性分类体系及其保持性和组合性特征，并将其与基于弱互模拟的经典层次结构进行对比。