IDEAS home Printed from https://ideas.repec.org/a/igg/jitwe0/v10y2015i1p1-30.html
   My bibliography  Save this article

Checking Opacity of Vulnerable Critical Systems On-The-Fly

Author

Listed:
  • Amina Bourouis

    (OASIS Research Lab/ENIT, University of Tunis El Manar, Tunisia)

  • Kais Klai

    (LIPN, CNRS UMR 7030 University of Paris 13, Sorbonne Paris City, France)

  • Yamen El Touati

    (OASIS Research Lab/ENIT, University of Manouba, Tunisia)

  • Nejib Ben Hadj-Alouane

    (OASIS Research Lab/ENIT, University of Tunis El Manar, Tunisia)

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.

Suggested Citation

  • Amina Bourouis & Kais Klai & Yamen El Touati & Nejib Ben Hadj-Alouane, 2015. "Checking Opacity of Vulnerable Critical Systems On-The-Fly," International Journal of Information Technology and Web Engineering (IJITWE), IGI Global, vol. 10(1), pages 1-30, January.
  • Handle: RePEc:igg:jitwe0:v:10:y:2015:i:1:p:1-30
    as

    Download full text from publisher

    File URL: http://services.igi-global.com/resolvedoi/resolve.aspx?doi=10.4018/ijitwe.2015010101
    Download Restriction: no
    ---><---

    More about this item

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:igg:jitwe0:v:10:y:2015:i:1:p:1-30. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Journal Editor (email available below). General contact details of provider: https://www.igi-global.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.