@article{ijc-14,
author = {Benattar, Gilles and Franck Cassez and Lime, Didier
and Roux, Olivier H.},
title = {Control and Synthesis of Non-Interferent Timed
Systems},
Type = {A - Journal},
journal = {International Journal of Control}, volume = {88}, number =
{2},
pages = {217--236},
year = {2015},
doi = {10.1080/00207179.2014.944356},
mywebpage = {timed},
urlpaper = {papers/ijc-2014.pdf},
ee = {http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full},
keywords = {security, non-interference},
category = {Non-interference},
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.}
}

{"_id":"NQrGGz293diEKfLHn","bibbaseid":"benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015","author_short":["Benattar, G.","Cassez, F.","Lime, D.","Roux, O. H."],"bibdata":{"bibtype":"article","type":"A - Journal","author":[{"propositions":[],"lastnames":["Benattar"],"firstnames":["Gilles"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"propositions":[],"lastnames":["Lime"],"firstnames":["Didier"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier","H."],"suffixes":[]}],"title":"Control and Synthesis of Non-Interferent Timed Systems","journal":"International Journal of Control","volume":"88","number":"2","pages":"217–236","year":"2015","doi":"10.1080/00207179.2014.944356","mywebpage":"timed","urlpaper":"papers/ijc-2014.pdf","ee":"http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full","keywords":"security, non-interference","category":"Non-interference","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.","bibtex":"@article{ijc-14,\nauthor = {Benattar, Gilles and Franck Cassez and Lime, Didier\nand Roux, Olivier H.},\ntitle = {Control and Synthesis of Non-Interferent Timed\nSystems},\nType = {A - Journal},\njournal = {International Journal of Control}, volume = {88}, number =\n{2},\npages = {217--236},\nyear = {2015},\ndoi = {10.1080/00207179.2014.944356},\nmywebpage = {timed},\nurlpaper = {papers/ijc-2014.pdf},\nee = {http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full},\nkeywords = {security, non-interference},\ncategory = {Non-interference},\nabstract = {We focus on the control and the\nsynthesis of secure timed systems which are modelled as timed automata. The\nsecurity property that the system must satisfy is a non-interference property.\nIntuitively, non-interference ensures the absence of any causal dependency from\na high-level domain to a lower level domain. Various notions of non-interference\nhave been defined in the literature, and in this paper, we focus on strong non-\ndeterministic non-interference (SNNI) and two (bi)simulation-based variants\nthereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties\nand their extensions have been mostly studied in the context of discrete event\nsystems, while it is now well-known that time is an important attack vector\nagainst secure systems. At the same time, there is an obvious interest in going\nbeyond simple verification to control problems: to be able to automatically make\nsystems secure. We consider non-interference properties in the challenging\nsetting of control of dense-time systems specified by timed automata and we\nstudy the two following problems: (1) check whether it is possible to find a\nsub-system so that it is non- interferent; if yes, (2) compute a (largest) sub-\nsystem which is non- interferent. We exhibit decidable sub-classes for these\nproblems, assess their theoretical complexities and provide effective algorithms\nbased on the classical framework of timed games.}\n}\n\n\n","author_short":["Benattar, G.","Cassez, F.","Lime, D.","Roux, O. H."],"key":"ijc-14","id":"ijc-14","bibbaseid":"benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/ijc-2014.pdf","Link":"http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full"},"keyword":["security","non-interference"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","yYF8uwWqay28JyxZC","qbqYFWskmoonRB43F"],"keywords":["security","non-interference"],"search_terms":["control","synthesis","non","interferent","timed","systems","benattar","cassez","lime","roux"],"title":"Control and Synthesis of Non-Interferent Timed Systems","year":2015}