Control and synthesis of non-interferent timed systems

Gilles Benattar, Franck Cassez, Didier Lime*, Olivier H. Roux

*Corresponding author for this work

Research output: Contribution to journalArticle

6 Citations (Scopus)

Abstract

We focus on the control and the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower level domain. Various notions of non-interference have been defined in the literature, and in this paper, we focus on strong non-deterministic non-interference (SNNI) and two (bi)simulation-based variants thereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties and their extensions have been mostly studied in the context of discrete event systems, while it is now well-known that time is an important attack vector against secure systems.At the same time, there is an obvious interest in going beyond simple verification to control problems: to be able to automatically make systems secure.We consider non-interference properties in the challenging setting of control of dense-time systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non-interferent; if yes, (2) compute a (largest) sub-system which is non-interferent.We exhibit decidable sub-classes for these problems, assess their theoretical complexities and provide effective algorithms based on the classical framework of timed games.

Original languageEnglish
Pages (from-to)217-236
Number of pages20
JournalInternational Journal of Control
Volume88
Issue number2
DOIs
Publication statusPublished - 1 Feb 2015
Externally publishedYes

Keywords

  • control
  • non-interference
  • safety timed games
  • synthesis
  • timed automaton

Fingerprint Dive into the research topics of 'Control and synthesis of non-interferent timed systems'. Together they form a unique fingerprint.

  • Cite this