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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Noninterference Analysis of Deterministically Timed Reversible Systems

  • Andrea Esposito,
  • Alessandro Aldini,
  • Marco Bernardo

摘要

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.