Synthesis of opaque systems with static and dynamic masks. Cassez, F., Dubreil, J., & Marchand, H. Formal Methods in System Design, 40(1):88-115, 2012. ![Synthesis of opaque systems with static and dynamic masks [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper ![Synthesis of opaque systems with static and dynamic masks [link]](https://bibbase.org/img/filetypes/link.svg "link")
Link abstract bibtex Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observ- ability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.
@article{fmsd-12,
author = {Franck Cassez and
Jérémy Dubreil and
Hervé Marchand},
title = {Synthesis of opaque systems with static and dynamic masks},
journal = {Formal Methods in System Design},
volume = {40},
number = {1},
year = {2012},
pages = {88-115},
type = {A - Journal},
urlpaper = {papers/fmsd-2012.pdf},
ee = {http://dx.doi.org/10.1007/s10703-012-0141-9},
bibsource = {DBLP, http://dblp.uni-trier.de},
mywebpage = {},
keywords = {security, opacity, diagnosis},
abstract = {
Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observ- ability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.
},
}
Downloads: 0
{"_id":"6yDtmDaTDDRbrJ7gD","bibbaseid":"cassez-dubreil-marchand-synthesisofopaquesystemswithstaticanddynamicmasks-2012","author_short":["Cassez, F.","Dubreil, J.","Marchand, H."],"bibdata":{"bibtype":"article","type":"A - Journal","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Jérémy"],"propositions":[],"lastnames":["Dubreil"],"suffixes":[]},{"firstnames":["Hervé"],"propositions":[],"lastnames":["Marchand"],"suffixes":[]}],"title":"Synthesis of opaque systems with static and dynamic masks","journal":"Formal Methods in System Design","volume":"40","number":"1","year":"2012","pages":"88-115","urlpaper":"papers/fmsd-2012.pdf","ee":"http://dx.doi.org/10.1007/s10703-012-0141-9","bibsource":"DBLP, http://dblp.uni-trier.de","mywebpage":"","keywords":"security, opacity, diagnosis","abstract":"Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observ- ability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask. ","bibtex":"@article{fmsd-12,\n author = {Franck Cassez and\n Jérémy Dubreil and\n Hervé Marchand},\n title = {Synthesis of opaque systems with static and dynamic masks},\n journal = {Formal Methods in System Design},\n volume = {40},\n number = {1},\n year = {2012},\n pages = {88-115},\n type = {A - Journal},\n\n urlpaper = {papers/fmsd-2012.pdf},\n ee = {http://dx.doi.org/10.1007/s10703-012-0141-9},\n bibsource = {DBLP, http://dblp.uni-trier.de},\n mywebpage = {},\n keywords = {security, opacity, diagnosis},\n abstract = {\nOpacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observ- ability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.\n\n },\n}\n\n","author_short":["Cassez, F.","Dubreil, J.","Marchand, H."],"key":"fmsd-12","id":"fmsd-12","bibbaseid":"cassez-dubreil-marchand-synthesisofopaquesystemswithstaticanddynamicmasks-2012","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/fmsd-2012.pdf","Link":"http://dx.doi.org/10.1007/s10703-012-0141-9"},"keyword":["security","opacity","diagnosis"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["security","opacity","diagnosis"],"search_terms":["synthesis","opaque","systems","static","dynamic","masks","cassez","dubreil","marchand"],"title":"Synthesis of opaque systems with static and dynamic masks","year":2012}