Control and Synthesis of Non-Interferent Timed Systems. Benattar, G., Cassez, F., Lime, D., & Roux, O. H. International Journal of Control, 88(2):217–236, 2015. Paper Link doi abstract bibtex 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.
@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.}
}
Downloads: 0
{"_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}