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 journalArticlepeer-review

10 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