Noninterference Analysis of Stochastically Timed Reversible Systems

Noninterference theory aims at ensuring the absence of covert channels among different security levels. As far as the verification of information-flow properties via equivalence checking is concerned, in nondeterministic and probabilistic settings weak bisimilarity has turned out to be adequate only for standard systems, while branching bisimilarity has proven to be appropriate for reversible systems too. In this paper we investigate noninterference for stochastically timed systems represented in the interactive Markov chain model of Hermanns. After recasting a selection of noninterference properties via Markovian variants of weak and branching bisimilarities, we study their preservation and compositionality aspects, build their taxonomy, and compare it with the nondeterministic and probabilistic taxonomies. We show the adequacy of our proposal through some examples about a database management system.