LFCS Seminar: Tuesday 23 April-Andrea Esposito

Title: Noninterference Analysis of Reversible Probabilistic Systems

Abstract:

Noninterference theory supports the analysis of secure computations in multi-level security systems: when a group of agents at a high security level performs some actions, the effect of those actions should not be seen by any agent at a low security level. In a nondeterministic setting, the approach to noninterefence based on weak bisimilarity turns out not to be adequate for reversible systems. This limitation can be circumvented by employing a more expressive semantics, which has been proven to be branching bisimilarity. In this talk we present an extension of the aforementioned result to reversible systems that feature both nondeterministic and probabilistic behaviors. We recast noninterference properties by employing probabilistic variants of weak and branching bisimilarities. Then we investigate a taxonomy of those properties as well as their preservation and compositionality features, along with a comparison with the nondeterministic taxonomy.