Noninterference Analysis of Deterministically Timed Reversible Systems

Information flow theory aims at guaranteeing the absence of covert channels among different security levels. As for the verification of noninterference via equivalence checking, in nondeterministic and probabilistic settings weak bisimilarity is adequate only for forward-computing systems, while branching bisimilarity has turned out to be appropriate for reversible systems too. In this paper we investigate noninterference for deterministically timed systems based on the model of Moller and Tofts. After recasting a selection of noninterference properties via timed variants of weak and branching bisimilarities, we analyze their preservation and compositionality aspects, establish their taxonomy, and compare it with the nondeterministic taxonomy for (ir)reversible systems. We illustrate the adequacy of our proposal on real-time database transactions.