A Process Algebraic Theory of Reversible Concurrent Systems with Applications to Noninterference Analysis

This thesis explores reversible calculus in process algebra and its application to noninterference analysis, presenting advancements in both theoretical foundations and practical implications. In the rst part, we introduce a novel process calculus for reversible systems, allowing the modeling of both forward and backward behaviors without relying on communication keys or stack-based memories. Key contributions include the development of strong and weak bisimulation equivalences, their characterization through modal logic, and sound and complete axiomatiza- tions. We also establish connections with existing equivalences, showing how our approach aligns with reverse trace equivalences and branching bisimilarity for sequential processes and hereditary history-preserving bisimilarity for fully concurrent systems. In the second part, we investigate noninterference analysis for systems capable of reversing computations, with branching bisimilarity as the common thread of the investigation. For nondeterministic systems, we extend the classical taxonomy of noninterference properties, analyze their preservation and compositionality features, and demonstrate the need for branching bisimilarity in uncovering covert channels arising in reversible systems. This analysis is further extended to probabilistic systems, where we rene the taxonomy and illustrate its application to detect information ows in both reversible and irreversible systems. We also propose a Markovian branching bisimilarity for reversible Markovian processes, providing a unied framework for noninterference analysis. This work contributes to the understanding of reversible systems and their applications in secure information ow analysis, laying the foundation for future research in extending reversible calculi.