A Decidable Notion of Timed Non-Interference

Issue title: Concurrency Specification and Programming (CS&P'2002), Part 1

Article type: Research Article

Authors: Barbuti, Roberto | Tesei, Luca

Affiliations: Dipartimento di Informatica, Università di Pisa, Via F. Buonarroti, 2, 56127 Pisa - Italy

Abstract: We present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against attacks.

Journal: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 137-150, 2003