一句话：提出基于分支双相似性的非干扰性质分类，揭示可逆计算中弱双相似性无法捕获的隐蔽信息流。
非干扰理论用于多级安全系统中的信息泄漏与安全计算分析。经典基于等价的方法多依赖弱双相似性，但本文指出在可逆计算场景下该语义不足以识别潜在隐蔽信道。以数据库管理系统为例，后向计算的激活可能引发标准前向执行中不可观测的信息流。为刻画来回计算效应，需采用表达能力更强的分支双相似性。本文系统研究基于分支双相似性的非干扰性质分类，分析其保持性与组合性，并与 Focardi 和 Gorrieri 基于弱双相似性的分类进行比较。结果表明分支双相似性可更精细地捕捉可逆系统中的信息流，为可逆计算的安全分析提供语义基础。
The theory of noninterference supports the analysis of information leakage 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, which 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 taxonomy of Focardi and Gorrieri based on weak bisimilarity.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{EspositoABR25,
title = {Noninterference Analysis of Reversible Systems: An Approach Based on Branching Bisimilarity},
author = {Andrea Esposito and Alessandro Aldini and Marco Bernardo and Sabina Rossi},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:6)2025}
}