Andrea Esposito ; Alessandro Aldini ; Marco Bernardo ; Sabina Rossi - Noninterference Analysis of Reversible Systems: An Approach Based on Branching Bisimilarity

lmcs:12603 - Logical Methods in Computer Science, January 22, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:6)2025
Noninterference Analysis of Reversible Systems: An Approach Based on Branching BisimilarityArticle

Authors: Andrea Esposito ; Alessandro Aldini ; Marco Bernardo ; Sabina Rossi

    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.


    Volume: Volume 21, Issue 1
    Published on: January 22, 2025
    Accepted on: November 21, 2024
    Submitted on: November 28, 2023
    Keywords: Computer Science - Cryptography and Security

    Consultation statistics

    This page has been seen 240 times.
    This article's PDF has been downloaded 90 times.