{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T17:10:31Z","timestamp":1710263431782},"reference-count":24,"publisher":"IGI Global","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,1,1]]},"abstract":"
Opacity is a security property capturing a system's ability to keep a subset of its behavior hidden from passive, but knowledgeable, observers. In this paper we use the formal definitions of opacity in three of its forms (simple opacity, -step weak opacity and -step strong opacity), basing on finite Labeled Transition Systems as a model. Then we present efficient algorithms for verifying opacity in all these forms within the context of a hybrid, on-the-fly approach. This approach is based on the construction of a Symbolic Observation Graph (SOG) that allows not only the abstraction of the systems behavior but also the preservation of the structure necessary for conducting opacity checking. Our preliminary experimental results are promising and demonstrate effectiveness facing the state-explosion problem which represents the main drawback of existing model checking techniques.<\/p>","DOI":"10.4018\/ijitwe.2015010101","type":"journal-article","created":{"date-parts":[[2015,8,7]],"date-time":"2015-08-07T21:15:59Z","timestamp":1438982159000},"page":"1-30","source":"Crossref","is-referenced-by-count":7,"title":["Checking Opacity of Vulnerable Critical Systems On-The-Fly"],"prefix":"10.4018","volume":"10","author":[{"given":"Amina","family":"Bourouis","sequence":"first","affiliation":[{"name":"OASIS Research Lab\/ENIT, University of Tunis El Manar, Tunisia"}]},{"given":"Kais","family":"Klai","sequence":"additional","affiliation":[{"name":"LIPN, CNRS UMR 7030 University of Paris 13, Sorbonne Paris City, France"}]},{"given":"Yamen","family":"El Touati","sequence":"additional","affiliation":[{"name":"OASIS Research Lab\/ENIT, University of Manouba, Tunisia"}]},{"given":"Nejib","family":"Ben Hadj-Alouane","sequence":"additional","affiliation":[{"name":"OASIS Research Lab\/ENIT, University of Tunis El Manar, Tunisia"}]}],"member":"2432","reference":[{"key":"ijitwe.2015010101-0","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000637"},{"key":"ijitwe.2015010101-1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-008-0058-x"},{"key":"ijitwe.2015010101-2","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"ijitwe.2015010101-3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02617-1_3"},{"key":"ijitwe.2015010101-4","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0141-9"},{"key":"ijitwe.2015010101-5","unstructured":"Dubreil, J. (2009, November). Monitoriting and Supervisory Control for Opacity Properties. University of Rennes 1."},{"key":"ijitwe.2015010101-6","first-page":"55","article-title":"Supervisory Control for Opacity.","author":"J.Dubreil","year":"2010","journal-title":"IEEE Transactions on Automatic Control"},{"key":"ijitwe.2015010101-7","author":"Y.Falcone","year":"2010","journal-title":"Various Notions of Opacity Verified and Enforced at Runtime"},{"key":"ijitwe.2015010101-8","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6761043"},{"key":"ijitwe.2015010101-9","first-page":"196","author":"S.Haddad","year":"2004","journal-title":"Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. Automated Technology for Verification and Analysis"},{"key":"ijitwe.2015010101-10","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2008.4574600"},{"key":"ijitwe.2015010101-11","first-page":"288","author":"K.Klai","year":"2008","journal-title":"MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs"},{"key":"ijitwe.2015010101-12","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(96)00112-4"},{"key":"ijitwe.2015010101-13","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2011.01.002"},{"key":"ijitwe.2015010101-14","first-page":"165","article-title":"Using unification for opacity properties.","volume":"4","author":"L.Mazar\u00e9","year":"2004","journal-title":"Proceedings of WITS"},{"key":"ijitwe.2015010101-15","unstructured":"Mullins, J., & Yeddes, M. (2013). Opacity with Orwellian Observers and Intransitive Non-interference. Computing Research Repository (CoRR), 1312.6426."},{"key":"ijitwe.2015010101-16","first-page":"344","article-title":"Opacity with Orwellian Observers and Intransitive Non-interference.","volume":"12","author":"J.Mullins","year":"2014","journal-title":"Discrete Event Dynamic Systems"},{"key":"ijitwe.2015010101-17","doi-asserted-by":"crossref","unstructured":"Saboori, Anooshiravan, & Hadjicostis, C. (2008). Verification of Initial-State Opacity in Security Applications of DES. Discrete Event Systems, 2008. WODES 2008. 9th International Workshop on (p. 6).","DOI":"10.1109\/WODES.2008.4605967"},{"key":"ijitwe.2015010101-18","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400083"},{"key":"ijitwe.2015010101-19","doi-asserted-by":"crossref","unstructured":"Saboori, Anooshiravan, & Hadjicostis, C. N. (2011). Verification of K-Step Opacity and Analysis of Its Complexity. IEEE T. Automation Science and Engineering, 8, 549\u2013559.","DOI":"10.1109\/TASE.2011.2106775"},{"key":"ijitwe.2015010101-20","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400083"},{"key":"ijitwe.2015010101-21","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2173774"},{"key":"ijitwe.2015010101-22","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-34805-0_30"},{"key":"ijitwe.2015010101-23","doi-asserted-by":"crossref","unstructured":"Wu, Y.-C., & Lafortune, S. (2012). Enforcement of Opacity Properties using Insertion Functions. IEEE 51st Annual Conference on Decision and Control (CDC) (pp. 6722\u20136728).","DOI":"10.1109\/CDC.2012.6426760"}],"container-title":["International Journal of Information Technology and Web Engineering"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=135302","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T04:46:30Z","timestamp":1654145190000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/ijitwe.2015010101"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2015,1,1]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"URL":"http:\/\/dx.doi.org\/10.4018\/ijitwe.2015010101","relation":{},"ISSN":["1554-1045","1554-1053"],"issn-type":[{"value":"1554-1045","type":"print"},{"value":"1554-1053","type":"electronic"}],"subject":["General Computer Science"],"published":{"date-parts":[[2015,1,1]]}}}