Control and Synthesis of Non-Interferent Timed Systems. Benattar, G., Cassez, F., Lime, D., & Roux, O. H. CoRR, 2012.
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
{"_id":"j6Qqc4v5f7oCF7JwQ","bibbaseid":"benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2012","author_short":["Benattar, G.","Cassez, F.","Lime, D.","Roux, O. H."],"bibdata":{"bibtype":"article","type":"E - Reports","author":[{"firstnames":["Gilles"],"propositions":[],"lastnames":["Benattar"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Didier"],"propositions":[],"lastnames":["Lime"],"suffixes":[]},{"firstnames":["Olivier","H."],"propositions":[],"lastnames":["Roux"],"suffixes":[]}],"title":"Control and Synthesis of Non-Interferent Timed Systems","journal":"CoRR","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. ","bibtex":"@article{benattar-2012,\n author = {Gilles Benattar and\n Franck Cassez and\n Didier Lime and\n Olivier H. Roux},\n title = {Control and Synthesis of Non-Interferent Timed Systems},\n journal = {CoRR},\n Type = {E - Reports},\n volume = {abs/1207.4984},\n year = {2012},\n url = {http://arxiv.org/abs/1207.4984},\n timestamp = {Wed, 10 Oct 2012 21:28:54 +0200},\n biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-4984},\n bibsource = {dblp computer science bibliography, http://dblp.org},\n keywords = {sceurity, non-interference},\n abstract = {\nIn 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.\n }\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2011\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n","author_short":["Benattar, G.","Cassez, F.","Lime, D.","Roux, O. H."],"key":"benattar-2012","id":"benattar-2012","bibbaseid":"benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2012","role":"author","urls":{"Paper":"http://arxiv.org/abs/1207.4984"},"keyword":["sceurity","non-interference"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F"],"keywords":["sceurity","non-interference"],"search_terms":["control","synthesis","non","interferent","timed","systems","benattar","cassez","lime","roux"],"title":"Control and Synthesis of Non-Interferent Timed Systems","year":2012}