Skip to main content

TS

Control and synthesis of non-interferent timed systems

Authors

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

ClearSy
Paris
France

NICTA

IRCCyN

Abstract

In this paper, we focus on 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 (CSNNI and BSNNI) 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.

BibTeX Entry

  @article{Benattar_CLR_15,
    journal          = {International Journal of Control},
    author           = {Benattar, Gilles and Cassez, Franck and Lime, Didier and Roux, Olivier H.},
    number           = {??},
    month            = mar,
    volume           = {??},
    year             = {2015},
    keywords         = {non-interference, synthesis, timed automaton},
    title            = {Control and Synthesis of Non-Interferent Timed Systems},
    pages            = {??}
  }

Download

Served by Apache on Linux on seL4.