Checking Opacity of Vulnerable Critical Systems On-The-Fly

Checking Opacity of Vulnerable Critical Systems On-The-Fly

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) and Nejib Ben Hadj-Alouane (OASIS Research Lab/ENIT, University of Tunis El Manar, Tunisia)
DOI: 10.4018/ijitwe.2015010101
OnDemand PDF Download:
$30.00
List Price: $37.50

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.
Article Preview

Introduction

Computers and computer networks facilitate even the most important and vital aspects of the modern lifestyle such as voting systems, electronic banking and trading systems, cloud computing and the internal know-how of large-scale, and even small-scale, businesses. These systems, however, are both critical and open to observation by possibly malicious parties. These facts make it crucial to secure the information used and exchanged by these systems.

It is important, then, to guarantee that no confidential information, private data or actions can be seen or deduced by an external observer. Opacity is a privacy property that formulates a system’s ability to keep hidden a secret from a passive, but knowledgable, observer.

Since its introduction in (Mazaré, 2004), and then its generalization to transition systems (Bryans, Koutny, Mazaré, & Ryan, 2008), opacity has been applied and discussed several times in the literature including the discussion of its timed variant in (Frank Cassez, 2009). These studies made appear numerous definitions, types and applications of the concept of opacity, as well as many methods to verifying and enforcing it (Bryans et al., 2008; Frank Cassez, 2009; Dubreil, Darondeau, & Marchand, 2010; Lin, 2011; Mullins & Yeddes, 2013, 2014). In this paper we continue down the path of the study of opacity in three of its variants, namely, simple opacity, -step weak opacity and -step strong opacity within the context of finite Labeled Transition Systems (LTS).

A secret subset of a system’s behavior is “Opaque” if a passive knowledgable observer is unable to deduce the occurrence of the secret from his or her observation of this system (Mullins & Yeddes, 2014). Assuming that the system is modeled by a Labeled Transition System (LTS), an observer (or intruder) has a full knowledge of the system (i.e. the LTS) but during the execution, he or she have access to a limited subset of the system’s actions called observable events (or actions). Given the LTS having as a subset of states called secret states and an intruder observing the system through a subset of events called observable events, is said to be “Opaque” if for every execution leading to a secret state, there exists another execution having the same projection on , that does not (end in a secret state). In this case, we say that is unable to know if the system had reached (ended in) a secret state or not.

We note that opacity can be formulated in two different ways, either by considering a subset of states as the secret and in this case we are talking about state-based opacity, or by considering a subset of sequences of events (named a trace) as the secret, and in this case we are talking about trace-based opacity. In this paper we are solely interested in the formalization of state-based opacitiy.

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 13: 4 Issues (2018): 1 Released, 3 Forthcoming
Volume 12: 4 Issues (2017)
Volume 11: 4 Issues (2016)
Volume 10: 4 Issues (2015)
Volume 9: 4 Issues (2014)
Volume 8: 4 Issues (2013)
Volume 7: 4 Issues (2012)
Volume 6: 4 Issues (2011)
Volume 5: 4 Issues (2010)
Volume 4: 4 Issues (2009)
Volume 3: 4 Issues (2008)
Volume 2: 4 Issues (2007)
Volume 1: 4 Issues (2006)
View Complete Journal Contents Listing