Noninterference Analysis of Reversible Systems: An Approach Based on Branching Bisimilarity
Andrea Esposito, Alessandro Aldini, Marco Bernardo, Sabina Rossi
TL;DR
The paper tackles information-flow security for reversible systems by shifting from weak to branching bisimilarity, enabling the detection of covert channels that arise when computations can proceed both forward and backward. It introduces a branching-bisimilarity–based taxonomy of noninterference properties (BrSNNI, BrNDC, SBrSNNI, P_BrNDC, SBrNDC) and proves preservation and limited compositionality results under operators such as restriction ($\setminus L$), hiding ($/ L$), and parallel composition ($\Vert_{L}$), while comparing with the FG01/FR06 weak-bisimilarity framework. A DBMS/authentication example demonstrates that backward computations can reveal information flows invisible in forward semantics, validating the necessity of branching-based analysis and connecting to back-and-forth bisimilarity (DMV90). The work extends the prior EAB23 by incorporating recursion, develops ancillary lemmas for branching congruence, and points toward quantitative extensions, thereby laying a solid foundation for secure reasoning about reversible distributed systems without action decoration.
Abstract
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.