Control and Synthesis of Non-Interferent Timed Systems. Benattar, G., Cassez, F., Lime, D., & Roux, O. H. CoRR, 2012.
Control and Synthesis of Non-Interferent Timed Systems [link]Paper  abstract   bibtex   
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). We consider timed non-interference properties for timed 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.
@article{benattar-2012,
  author    = {Gilles Benattar and
               Franck Cassez and
               Didier Lime and
               Olivier H. Roux},
  title     = {Control and Synthesis of Non-Interferent Timed Systems},
  journal   = {CoRR},
  Type = {E - Reports},
  volume    = {abs/1207.4984},
  year      = {2012},
  url       = {http://arxiv.org/abs/1207.4984},
  timestamp = {Wed, 10 Oct 2012 21:28:54 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-4984},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  keywords = {sceurity, non-interference},
  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). We consider timed non-interference properties for timed 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.
  }
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2011
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Downloads: 0