Romain Jacob
email: rjacob@ens-cachan.fr

Jean-Jacques Lesage
email: jean-jacques.lesage@ens-cachan.fr

Jean-Marc Faure
email: jean-marc.faure@ens-cachan.fr

Overview of Discrete Event Systems Opacity: models, validation, and quantification $

Keywords: Opacity, Discrete event systems, Validation, Verification, Enforcement, Quantification, Secrecy, Privacy, Security

Over the last decade, opacity of discrete event systems (DES) has become a very fertile field of research. Driven by safety and privacy concerns in network communications and online services, much theoretical work has been conducted in order to design opaque systems. A system is opaque if an external observer in unable to infer a "secret" about the system behavior. This paper aims to review the most commonly used techniques of opacity validation for deterministic models and opacity quantification for probabilistic ones. Available complexity results are also provided. Finally, we review existing tools for opacity validation and current applications.

Introduction

Online services and network communications have become ubiquitous over the past 30 years. This evolution in our everyday life brought along new preoccupations regarding security and privacy. Despite continuously releasing tons of information about everything we do and think, we still want some information to remain secret. Thus, a new problem has arisen in computer science, called Information Flow. It characterizes the (possibly illegal and indirect) transmission of secret data from a high level user to a low level one. Various information flow properties have been defined in the literature: anonymity, noninterference, secrecy, privacy, security, and opacity; e.g., refer to [START_REF] Schneider | Csp and anonymity[END_REF]; [START_REF] Focardi | A taxonomy of trace-based security properties for ccs[END_REF]; [START_REF] Hadj-Alouane | On the verification of intransitive noninterference in mulitlevel security[END_REF]; Bérard et al. (2015a); [START_REF] Alur | Preserving secrecy under refinement[END_REF].

In this paper, we focus on opacity. It is a general information flow property: anonymity and secrecy can be formulated as opacity problems. Opacity characterizes whether a given "secret" about a system behavior is hidden or not from an external observer, further called the intruder. It is assumed the intruder has full knowledge of the system's structure but only partial observability. Based on its observations, the intruder constructs an estimate of the system's behavior. The secret is said to be opaque if the intruder's estimate never reveals the system's secret. Specifically, the system is opaque if, for any secret behavior, there exists, at least, one other non-secret behavior that looks the same to the intruder.

Opacity is a rather recent field of research. It was first introduced in 2004 in computer science to analyze cryptographic protocols [START_REF] Mazaré | Using unification for opacity properties[END_REF]. It reached the discrete event systems (DES) community with the work of [START_REF] Bryans | Modelling opacity using petri nets[END_REF] which investigated opacity in systems modeled as Petri nets. Secrets were set as predicates over Petri net markings (i.e., states). In [START_REF] Bryans | Opacity generalised to transition systems[END_REF], previous work was extended by investigating opacity in labeled transition systems (LTS), in which secrets were defined as predicates over runs. More recently, Saboori and Hadjicostis investigated state-based opacity properties using finite-state automata (FSA) models [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]; [START_REF] Saboori | Verification and enforcement of state-based notions of opacity in discrete event systems[END_REF]). Many researchers have considered the validation of opacity properties which spans from system's opacity verification (e.g., [START_REF] Badouel | Concurrent secrets[END_REF]; [START_REF] Hadjicostis | Opacity formulations and verification in discrete event systems[END_REF]; [START_REF] Saboori | Verification of initial-state opacity in security applications of des[END_REF], 2009, 2010a, 2013)) to the synthesis of a controller/scheduler which assures opacity, either through supervision [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF]; [START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]; Saboori & Hadjicostis (2008a)) or enforcement [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]). In a general way, opacity validation w.r.t. a given secret and intruder is a yes/no question for logical models (whether with deterministic or nondeterministic transition function). In the opposite, if one is interested in quantifying the risk of possible information leakage from the system, it implies usage of probabilistic models (e.g., [START_REF] Bérard | Quantifying opacity[END_REF]Bérard et al. ( , 2015a)); [START_REF] Ibrahim | Secrecy in stochastic discrete event systems[END_REF]; [START_REF] Keroglou | Initial state opacity in stochastic des[END_REF]; Saboori & Hadjicostis (2010b,a)).

From a practical point of view, these properties are of great interest for anyone aiming for more privacy, safety, or even secrecy, in communication protocols, complex networked systems, or even a simple software architecture. It is ever more common to have privacy-related specifications in both software and hardware design. Using opacity theory, one can formally verify whether or not these specifications are satisfied, or, at least, have a quantitative measure for the risk of violation.

This paper aims to provide a comprehensive and general review of opacity related work considering DES models, hence, we purposefully leave out too technical details. We assume the reader has a general knowledge of DES theory and practice and of classically related problems (i.e., formalism of finite automata and probabilistic automata, diagnosis, verification, supervisory control...). In case of need, please refer to [START_REF] Cassandras | Introduction to discrete event systems[END_REF] for more information on these problems. This paper is an extended version of a paper presented by the authors at the 5 th IFAC International Workshop On Dependable Control of Discrete Systems (DCDS'15) [START_REF] Jacob | Opacity of discrete event systems: models, validation and quantification[END_REF].

After introducing relevant notations in Section 2, we synthesize different notions of opacity used in the literature in Section 3. Section 4 reviews validation methods of various opacity properties. Section 5 presents extensions to probabilistic models and Section 6 summarizes decidability and complexity of most approaches surveyed in this paper. Finally, applications of opacity in DES are presented in Section 7 and Section 8 suggests some perspectives for further research.

Preliminaries

Let E be an alphabet of events. E * is the set of all finite strings composed of elements of E, including the empty string ε. A language L ⊆ E * is a set of finite-length strings of labels in E. For a string t, |t| denotes the length of t. For a string ω, ω denotes the prefix-closure of ω and is defined as ω = {t ∈ E * |∃s ∈ E * , ts = ω}. The post-string ω/s of ω after s is defined as ω/s = {t ∈ E * , st = ω}.

A finite-state automaton G = (X, E, f, X 0 ) is a 4-tuple composed of a finite set of states X = {0, 1, ..., N -1}, a finite set of events E, a partial state transition function f : X × E → X, and a set of initial states X 0 . The function f is extended to the domain X × E * in the usual manner. The language generated by the system G describes the system's behavior and is defined by

L(G, X 0 ) = {s ∈ E * |∃i ∈ X 0 , f (i, s) is defined}; it is prefix-closed by definition.
Note that in opacity problems, the initial state needs not to be known a priori, therefore, we have a set of initial states instead of a single initial state. We consider partially observable systems. The event set is partitioned into an observable set E o and an unobservable set E uo . Given a string t ∈ E * , its observation is the output of the natural projection function P : E * → E * o , which is recursively defined as P (te) = P (t)P (e) where t ∈ E * and e ∈ E. The projection of an event P (e) = e if e ∈ E o , while P (e) = ε if e ∈ E uo ∪ {ε}. Finally, for a language J ⊆ E * , the inverse projection is defined as P -1 (J) = {t ∈ E * : P (t) ∈ J}.

Opacity of discrete event systems

In this section, we formalize different opacity properties of DES. In the general case, the intruder is assumed to have full knowledge of the system structure (plus eventually of the system's controller) but he/she has only partial observability over it. Opacity is parameterized by a secret predicate S and by the intruder's observation mapping P over the system's executions. A system is opaque w.r.t. S and P if, for any secret run in S, there is another run not in S which is observably equivalent.

In cases of DES models, the secret predicate S can be of two classes: a subset of executions (or parts of executions) or a subset of states. This classifies opacity properties into two families: language-based opacity and state-based opacity.

Language-based opacity -LBO

LBO has been formalized in different ways in the literature. It was first introduced in [START_REF] Badouel | Concurrent secrets[END_REF] and [START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]. LBO (also referred to as trace-based opacity) is defined over a secret behavior described by a language L S ⊆ E * . The system is opaque w.r.t. L S and the projection map P if no execution leads to an estimate that is completely inside the secret behavior. Alternatively, in [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF], LBO is defined over two sublanguages of the system, (L 1 , L 2 ) ⊆ (L(G, X 0 )) 2 . Sublanguage L 1 is opaque w.r.t. L 2 and an observation mapping θ if the intruder confuses every string in L 1 with some strings in L 2 under θ. In most recent papers considering LBO, the latter definition is used with the observation mapping θ being the natural projection mapping P .

Definition 1 (LBO -Strong Opacity). Given a system G = (X, E, f, X 0 ), a projection P , a secret language L S ⊆ L(G, X 0 ), and a non-secret language L N S ⊆ L(G, X 0 ), G is language-based opaque if for every string t ∈ L S , there exists another string t ∈ L N S such that P (t) = P (t ). Equivalently,

L S ⊆ P -1 [P (L N S )].
The system is language-based opaque if for any string t in the secret language L S , there exists, at least, one other string t in the non-secret language L N S with the same projection. Therefore, given the observation s = P (t) = P (t ), the intruder cannot conclude whether the secret string t or the non-secret string t has occurred. Note that L S and L N S do not need to be prefix-closed in general, nor even regular.

Part of the literature refers to Definition 1 as strong opacity. In [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF], a smoother opacity property is also introduced. Definition 2 (LBO -Weak Opacity). Given a system G = (X, E, f, X 0 ), a projection P , a secret language L S ⊆ L(G, X 0 ), and a non-secret language L N S ⊆ L(G, X 0 ), G is weakly opaque if for some string t ∈ L S , there exists another string t ∈ L N S such that

P (t) = P (t ). Equivalently, L S ∩ P -1 [P (L N S )] = ∅.
The system is weakly opaque if some strings in L S are confused with some strings in L N S . As a consequence, we can further define easily the property of no opacity. [START_REF] Ben-Kalefa | Opaque superlanguages and sublanguages in discrete event systems[END_REF] that LBO properties are closed under union, but may not be closed under intersection. They further discuss how to modify languages to satisfy the strong, weak, and no opacity by investigating sublanguages and superlanguages.

∩ P -1 [P (L N S )] = ∅. Remark 1. It is shown in Ben-Kalefa &
Example 1. From Wu & Lafortune (2013) -Consider the system G in Fig. 1 with

E o = {a, b, c}.
It is language-based opaque when L S = {abd} and L N S = {abcc * d, adb} because whenever the intruder sees P (L S ) = {ab}, it is not sure whether string abd or string adb has occurred. However, this system is not language-based opaque if L S = {abcd} and L N S = {adb, abd, abccc * d}; no string in L N S has the same projection as the secret string abcd.

Remark 2. In general, LBO refers to strong opacity in the literature, as in the rest of this paper.

State-based opacity -SBO

The state-based approach for opacity of DES was introduced in [START_REF] Bryans | Modelling opacity using petri nets[END_REF] for Petri nets models then extended to FSA in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]. The state-based approach relates to the intruder ability to infer that the system is or has been in a given "secret" state or set of states. Depending on the nature of the secret set, different opacity properties have been defined. 2005) and called final opacity in the context of Petri nets. The definition was then adapted to LTS in [START_REF] Bryans | Opacity generalised to transition systems[END_REF], and further developed in finite state automata models in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]. A system is CSO if the intruder can never infer, from its observations, whether the current state of the system is a secret state or not.

Definition 4 (Current-State Opacity). Given a system G = (X, E, f, X 0 ), a projection P , a set of secret states X S ⊆ X, and a set of non-secret states X N S ⊆ X, G is current-state opaque if ∀i ∈ X 0 and ∀t ∈ L(G, i) such that f (i, t) ∈ X S , ∃j ∈ X 0 and ∃t ∈ L(G, j) such that f (j, t ) ∈ X N S and P (t) = P (t ).

The system is CSO if for every string t that leads to a secret state, there exists another string t leading to a nonsecret state whose projection is the same. As a result, the intruder can never assert with certainty that the system's current state belongs to X S . Remark 3. In [START_REF] Bryans | Modelling opacity using petri nets[END_REF], the property of always-opacity is also introduced. A system is alwaysopaque (or total-opaque in [START_REF] Bryans | Opacity generalised to transition systems[END_REF]) over a set of runs if it is CSO for any state visited during these runs. This is equivalent to consider a set of secret states which lies on a prefix-closed language.

Example 2. From Wu & Lafortune (2013) -Consider G in Fig. 2 and the sets of secret and non-secret states X S = {3} and X N S = X\X S .

If E o = {b}, then G is current-state opaque because the intruder is always confused between ab and cb when observing b; that is, the intruder cannot tell if the system is in state 3 or 4.

However, if E o = {a, b}, CSO does not hold because the intruder is sure that the system is in state 3 when observing ab.

Initial-State Opacity -ISO

ISO property relates to the membership of the system's initial state within a set of secret states. The system is initial-state opaque if the observer is never sure whether the system's initial state was a secret state or not. Definition 5 (Initial-State Opacity). Given a system G = (X, E, f, X 0 ), a projection P , a set of secret initial states X S ⊆ X 0 , and a set of non-secret initial states X N S ⊆ X 0 , G is initial-state opaque if ∀i ∈ X S and ∀t ∈ L(G, i), ∃j ∈ X N S and ∃t ∈ L(G, j) such that P (t) = P (t ).

The system is ISO (or initial-opaque in [START_REF] Bryans | Modelling opacity using petri nets[END_REF]) if, for every string t that originates from a secret state i, there exists another string t originating from a non-secret state j such that t and t are observationally equivalent. Therefore, the intruder can never determine whether the system started from a secret state i or from a non-secret state j.

Example 3. From Wu & Lafortune (2013) -Consider G in Fig. 3 with E o = {a, b}, X S = {2}, and X N S = X\X S . G is initial-state opaque because for every string t starting from state 2, there is another string (τ )t starting from state 0 that looks the same.

However, ISO does not hold if X S = {0}. Whenever the intruder sees string aa, it is sure that the system originated from state 0; no other initial states can generate strings that look the same as aa.

Remark 4. There is one important difference to note between current-state and initial-state opacity in terms of monotony: initial state opacity exhibits a monotonic property (the set of possible initial states can only decrease as more observations become available), in contrast with current state opacity, for which there is no guarantee to obtain more relevant information over time.

Remark 5. [START_REF] Hadjicostis | Resolution of initial-state in security applications of des[END_REF] defines resolution of initial state w.r.t. a secret set of states S. It requires that when the system starts from a secret state, the observer will be able to eventually (i.e., after a finite sequence of events/observations) determine with certainty that the system's initial state lied within the set of secret states S. It is worth pointing out at this point that absence of resolution of initial state is necessary but not sufficient for ISO.

Initial-and-Final-State Opacity -IFO

In [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF], the authors introduce initialand-finite opacity. It is an extension of ISO and CSO which requires both the initial and final state to be hidden from the intruder. The only difference is that the secret is now defined over pairs of states (and not only states).

Definition 6 (Initial-and-Final-State Opacity).

Given system G = (X, E, f, X 0 ), projection P , set of secret state pairs X SP ⊆ X 0 ×X, and set of non-secret state pairs

X N SP ⊆ X 0 × X, G is initial-and-final-state opaque if ∀(x 0 , x f ) ∈ X SP and ∀t ∈ L(G, x 0 ) such that f (x 0 , t) = x f , ∃(x 0 , x f ) ∈ X N SP and ∃t ∈ L(G, X 0 ) such that f (x 0 , t ) = x f and P (t) = P (t ).
The system is initial-and-final-state opaque if for any string t that starts from x 0 and ends at x f , with (x 0 , x f ) ∈ X SP , there exists another string t starting from x 0 and ending at x f , where (x 0 , x f ) ∈ X N SP , that has the same projection. Therefore, the intruder can never determine whether the initial-and-final state pair is a secret pair or a non-secret pair.

Remark 6. ISO and CSO are special cases of IFO.

To obtain an ISO problem from an IFO formulation, set

X SP = X S × X and X N SP = X N S × X. Likewise, to obtain a CSO problem, set X SP = X 0 × X S and X N SP = X 0 × X N S . Example 4. From Wu & Lafortune (2013) -Consider again G in Fig. 3 and take X SP = {(3, 1)}.
G is initial-and-final state opaque if the non-secret state pair set is

X N SP = {(1, 0), (1, 1), (1, 2), (1, 3)}.
However, initial-and-final-state opacity property does not hold if we take X N S = {(0, 0)} since (0, 0) is the only state pair that corresponds to string aa; no other state pairs give strings that look the same as aa.

K-step opacity

Except for ISO, previously defined opacity properties do not consider the system behavior once it has exited a secret state. A more general problem would be to keep secret the fact the system was in a secret state a few steps ago. This property is called K-step opacity and was first introduced in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF].

Definition 7 (K-step (weak) opacity). Given a system G = (X, E, f, X 0 ), a projection P , and a set of secret states X S ∈ X, G is K-step (weakly) opaque w.r.t. X S and P for K ≥ 0 (or (X S , P, K)-(weakly

) opa- que) if ∀i ∈ X 0 , ∀t ∈ L(G, i), and ∀t ∈ t such that f (i, t ) ∈ X S and |P (t)/P (t )| ≤ K, ∃j ∈ X 0 , ∃s ∈ L(G, j)
, and ∃s ∈ s, such that f (j, s ) ∈ X N S , P (s) = P (t) and P (s ) = P (t ).

This definition can be reformulated as in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]. The system is (X S , P, K)-opaque if for every execution t of G and for every secret execution t prefix of t with an observable difference inferior to K, there exists two executions s and s observationally equivalent respectively to t and t such that s is not a secret execution (i.e., which does not bring the system in a secret state). G is (X S , P, 1)-opaque, but it is not (X S , P, 2)-opaque, as only (τ )aba is a compatible execution with the observation aba. Hence, after the second a has occurred, the intruder can deduce that the system was in state 2 two steps before.

Remark 7. K-step opacity is a direct extension of CSO. CSO is equivalent to 0-step opacity [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]).

In [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF], Definition 7 is referred to as Kstep weak opacity. The property of K-step strong opacity holds if the system is K-step weakly opaque and there exists a trace of the system (observably equivalent to the actual execution) which does not cross any secret state over the last K steps. This can be formalized with the following definition.

Definition 8 (K-step strong opacity). Given a system G = (X, E, f, X 0 ), a projection P , and a set of secret states X S ∈ X, G is K-step strongly opaque w.r.t. X S and P for K ≥ 0 (or (X S , P, K)-strongly opaque) if ∀i ∈ X 0 and ∀t ∈ L(G, i), ∃j ∈ X 0 and ∃s ∈ L(G, j) such that P (s) = P (t) and ∀s ∈ s, |P (s

)/P (s )| ≤ K ⇒ ∃j ∈ X 0 such that f (j , s ) ∈ X N S .
Example 6. From Falcone & Marchand (2013) -Consider G in Fig. 5 with G is (X S , P, K)-weakly opaque for any K ∈ N. The intuition is that we will always have confusion between pairs of states (5, 2), (6, 3), and (7, 4), such that the intruder will never know with absolute certainty that the system was in state 2 or 7 at a given point in time.

E o = {a, b, c}, X S = {2,
It also holds that the system is (X S , P, 1)-strongly opaque. However, it is not (X S , P, 2)-strongly opaque since after observing aba, we know that the system is either in state 7 (which is a secret state) or in state 4, which implies it was in state 2 (the other secret state) two steps ago. Ultimately, we know for sure that the system was in a secret state at most 2 steps ago.

Remark 8. In general, K-step opacity refers to weak opacity in the literature, as in the rest of this paper.

Infinite-step opacity

In [START_REF] Saboori | Verification of infinite-step opacity and analysis of its complexity[END_REF] and Saboori ( 2011), K-step opacity has been further extended to infinite-step opacity.

Definition 9 (Infinite-step opacity). Given a system G = (X, E, f, X 0 ), a projection P , and a set of secret states X S ∈ X, G is infinite-step opaque w.r.t. X S and P , or (X S , P, ∞)-opaque, if ∀i ∈ X 0 , ∀t ∈ L(G, i), and ∀t ∈ t such that f (i, t ) ∈ X S , ∃j ∈ X 0 , ∃s ∈ L(G, j), and ∃s ∈ s, such that f (j, s ) ∈ X N S , P (s) = P (t), and P (s ) = P (t ).

A system is infinite-step opaque if, for every execution of the system, after having observed an arbitrarily long sequence of events, the intruder cannot infer that the system was in a secret state at some point (at any step back in the execution).

Transformations between different opacity properties

The aforementioned opacity properties have strong connections between each other. Several works have addressed the translation between them. Saboori & Hadjicostis (2008a) adapts the languagebased definition to ISO in order to apply supervisory control methods (refer to Section 4.2). On the contrary, [START_REF] Cassez | Dynamic observers for the synthesis of opaque systems[END_REF][START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF] describes transformations from LBO to CSO. In [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF], the authors extend these works and provide a full transformation mapping between LBO, CSO, ISO, and IFO.

In addition, we already mentioned that K-step opacity is an extension of CSO. CSO is equivalent to 0-step opacity.

Finally, in Saboori ( 2011), a language-based translation of K-step opacity is suggested: trace-based K-step opacity. It is a special case of K-step opacity which, to the best of our knowledge, has never been used or considered in any other work. It is mentioned here for the sake of completeness.

Distributed opacity

Even though most opacity-related studies account for a single intruder only, a few of them consider distributed notions of opacity. Hence, [START_REF] Badouel | Concurrent secrets[END_REF] consider multiple intruders, each of them having its own observation mapping and secret of interest. The system is said to be concurrently opaque if all secrets are safe. A different notion, called joint opacity is presented in [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF] and [START_REF] Wu | Verification and Enforcement of Opacity Security Properties in Discrete Event Systems[END_REF]. In this setting, several intruders collaborate through a coordinator in order to discover the same secret. Finally, [START_REF] Paoli | Decentralized opacity of discrete event systems[END_REF] consider decentralized framework with and without coordination among agents and formalize definitions of decentralized opacity. It is shown to be an extension of co-observability, used in traditional supervisory control [START_REF] Ramadge | The control of discrete event systems[END_REF].

Infinite DES models

Up to a few years ago, opacity-related studies only considered finite-state DES models. There are recent works addressing extensions to infinite-state. CSO and diagnosability verification are investigated for infinite-state DES modeled by pushdown automata in [START_REF] Kobayashi | Verification of opacity and diagnosability for pushdown systems[END_REF] (therein called pushdown systems), as well as in [START_REF] Chédor | Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems[END_REF] and [START_REF] Chédor | Diagnosis, opacity and conformance testing for recursive tile systems[END_REF], in the more general setting of recursive tile systems.

Extension to timed DES has also been considered, but it has been shown in [START_REF] Cassez | The dark side of timed opacity[END_REF] that even for a very restrictive class of Timed Automata, opacity is already undecidable for a problem in dense-time. However, considering not dense-time domains (e.g., N) may render the opacity problem tractable.

Relation with other DES and information flow properties

We mentioned in Section 1 that opacity is a very general information flow property. Relations between several of these properties can be easily drawn.

Easiest is secrecy, in which the system predicate is secret if the predicate and its complement are simultaneously opaque [START_REF] Badouel | Concurrent secrets[END_REF]). It is also referred to as symmetrical opacity [START_REF] Bérard | Quantifying opacity[END_REF]). It was shown that anonymity [START_REF] Bryans | Opacity generalised to transition systems[END_REF][START_REF] Bérard | Verification of information flow properties under rational observation[END_REF] and some non-interference problems [START_REF] Cassez | Synthesis of noninterferent systems[END_REF][START_REF] Bryans | Opacity generalised to transition systems[END_REF][START_REF] Benattar | Control and synthesis of non-interferent timed systems[END_REF][START_REF] Bérard | Non-interference in partial order models[END_REF]) may be reduced to opacity by using suitable observation functions and depending on the type of secret under consideration. The equivalence between opacity and intransitive non-interference is proven in [START_REF] Mullins | Opacity with orwellian observers and intransitive non-interference[END_REF]. [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF] also establishes links between opacity, anonymity, and secrecy and shows that observability, diagnosability, and detectability can be reformulated as opacity as well.

More generally, opacity is a problem closely related to diagnosis [START_REF] Sampath | Failure diagnosis using discrete-event models[END_REF][START_REF] Zaytoon | Overview of fault diagnosis methods for discrete event systems[END_REF]: for opacity to hold, the secret should not be diagnosable from the viewpoint of the intruder. Some instances of opacity problem can be formulated as diagnosis ones (e.g., resolution of ISO from [START_REF] Hadjicostis | Resolution of initial-state in security applications of des[END_REF]). As a result, several opacity-related works try to bridge with the huge amount of work done in the diagnosis community; e.g., [START_REF] Dubreil | Monitoring confidentiality by diagnosis techniques[END_REF]; [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF]; [START_REF] Kobayashi | Verification of opacity and diagnosability for pushdown systems[END_REF]; [START_REF] Chédor | Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems[END_REF].

Ensuring opacity

Traditional opacity formulations from the literature were presented in Section 3. The questions are now the following: How does one know that a given system G is opaque w.r.t. a secret and the information available to intruders? Furthermore, if it is not, what can be done to make it opaque? These questions have been continuously addressed and this section aims to synthesize the approaches available in the literature.

There are three main approaches to ensure opacity properties of DES:

1. Verification, which roughly consists in modelchecking opacity properties;

2. Supervisory control theory (SCT), which restricts the system's behavior in order to preserve the secret;

3. Enforcement, which inputs observable events of the systems and outputs (possibly) modified information to observers, such that the secret is preserved.

The key difference to note between SCT and enforcement is that SCT constrains the system behavior (by restraining its output) by means of a supervisor while enforcement allows the system free-behavior but post processes all its output. For more details about these approaches and their pros-and-cons, one can refer [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]. The three mechanisms are illustrated by Fig. 6.

Verification of opacity properties

As mentioned in Introduction, opacity is a rather recent field of research. Verification of opacity relates directly to the general problem of verification of DES, which has been extensively studied and is well-known. It was shown in [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF] that opacity verification is equivalent to the universality problem (i.e., whether or not the system admits all possible words constructed on its alphabet). The specific task to perform is to encode the opacity property of interest (refer to Section 3) such that classical model-checking approaches and tools can be used. However, such opacity encoding might not be trivial, like for K-step opacity for instance. Verification of K-step opacity was tackled in [START_REF] Saboori | Verification of k-step opacity and analysis of its complexity[END_REF] by use of two types of K-delay state estimators. It is also developed in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF].

Remark 9. We mentioned in Section 3.6 that opacity can be related to diagnosability. [START_REF] Dubreil | Monitoring confidentiality by diagnosis techniques[END_REF] investigate the use of techniques from diagnosis of DES [START_REF] Zaytoon | Overview of fault diagnosis methods for discrete event systems[END_REF]) to detect and predict the flow of secret information and construct a monitor that allows an administrator to detect it.

In the sequel of this section, we choose to further present solely control and enforcement approaches, for which specific opacity-related methods have been developed. For more details about verification of LBO, refer to [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF]; for SBO, refer to [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF] and [START_REF] Hadjicostis | Opacity formulations and verification in discrete event systems[END_REF]. General results about verification of DES can be found in [START_REF] Cassandras | Introduction to discrete event systems[END_REF].

Supervisory control theory -SCT

The potential use of SCT for opacity validation of DES is rather obvious. Several works present construction of minimally restrictive opacity-enforcing supervisory controllers; e.g., [START_REF] Takai | A formula for the supremal controllable and opaque sublanguage arising in supervisory control[END_REF]; [START_REF] Takai | Verification and synthesis for secrecy in discrete-event systems[END_REF]; Saboori & Hadjicostis (2008a); [START_REF] Saboori | Verification and enforcement of state-based notions of opacity in discrete event systems[END_REF]; [START_REF] Saboori | Opacity-enforcing supervisory strategies via state estimator constructions[END_REF]; [START_REF] Ben-Kalefa | Supervisory control for opacity of discrete event systems[END_REF]. It is shown that optimal control always exists for strong-opacity [START_REF] Dubreil | Supervisory control for opacity. Automatic Control[END_REF][START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF].

In these approaches, the intruder is generally assumed to have full knowledge of the supervisor's structure in addition to the system's. Moreover, the set of events the intruder can observe is fixed.

The applicability of SCT depends on the hypothesis made on the system's model. Given E I , E O and E C being respectively, the set of events observable by the intruder, the set of events observable by the supervisor, and the set of controllable events, SCT can be directly applied in the following cases [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF]):

1.

E C ⊆ E O ⊆ E I ; 2. E I ⊆ E C ⊆ E O .
Furthermore, to deal with the following two cases, slight extensions of SCT have been suggested in [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF] and [START_REF] Dubreil | Supervisory control for opacity. Automatic Control[END_REF] 3.

E C ⊆ E I ⊆ E O ; 4. E I ⊆ E O and E C ⊆ E O
but without E C and E I being comparable. G is a representation of all sequences of possible moves of an agent in a three story building with a south wing and a north wing, both equipped with lifts and both connected by a corridor at each floor. Moreover, there is a staircase that leads from the first floor in the south wing to the third floor in the north wing. The agent starts from the first floor in the south wing. He can walk up the stairs (s) or walk through the corridors (c) from south to north without any control. The lifts can be used several times one floor upwards (u) and at most once one floor downwards (d) altogether. The moves of the lifts are controllable. Thus E C = {u, d}. The secret is that the agent is either at the second floor in the south wing or at the third floor in the north wing. The adversary may gather the exact subsequence of moves in E I = {u, c, s} from sensors, but he cannot observe the downwards moves of the lifts. Furthermore, all events are observable to the supervisor, i.e., E O = E. Hence, this example falls into the fourth of the aforementioned cases.

The derivation of the minimally restrictive supervisor ensuring the secret will not be disclosed is performed by a sequential derivation of condensed state estimators and their losing configurations. In a nutshell, a configuration is combination of the true system state (the upper line) and the best estimate the intruder can make of the system state (the lower line). A losing configuration is such that the intruder's estimate belongs to the set of secret states. One can track controllable actions backward from losing configurations on acyclic paths of the condensed estimator and disable the last controllable transition on each losing path. The next condensed state estimator is then derived, taking into account the newly disabled transitions. Once we get to a condensed state estimator without any losing configuration, we have reached the minimally restrictive supervisor. Refer to [START_REF] Dubreil | Supervisory control for opacity. Automatic Control[END_REF] for more details.

Fig. 8(a), (b), and (c) show the subsequent condensed state estimators needed to solve this example. losing configurations are boxed red, the controllable transitions to disabled in the next step are in dashed lines. Fig. 7(b) is the resulting supervisor.

One can notice that one secret state only remains in the controlled system. This means others secret states cannot be opaque to the intruder. If the agent aims to go and stay in state 1, 7 or 11, it will be inferred by the intruder. This is an example of ensuring current-state opacity by supervisory control. Note that this system is not 1-opaque (refer to Def. 7).

In [START_REF] Badouel | Concurrent secrets[END_REF], the authors solved the problem of concurrent secrecy (Section 3.4) using SCT. Sufficient conditions to compute an optimal supervisor preserving all secrets are provided, assuming that the supervisor has complete knowledge of the system and full control over it.

The work of Ben-Kalefa & Lin (2011) considers the verification of both strong and weak LBO. It shows that the solution to the Strong-Opacity Control Problem (SOCP) exists and is unique if all controllable events are observable. However solutions for the Weak-Opacity Control Problem (WOCP) does not exist. This means that if a system is not weakly opaque w.r.t. a given secret language, there exists no controllable and observable sublanguage which can assure weak opacity.

In [START_REF] Darondeau | Enforcing opacity of regular predicates on modal transition systems[END_REF], the authors lift the opacity enforcing control problem using SCT from a single finite transition systems to families of finite transition systems specified by modal transition systems [START_REF] Larsen | Modal specifications[END_REF]). The objective is to ensure opacity of a secret predicate on all LTS derived from a given modal transition system.

Using SCT is naturally more suited to language-based notions of opacity. However, the verification of initial state opacity has been addressed in Saboori & Hadjicostis (2008a) by means of reformulation of ISO into LBO, under regular SCT hypothesis (cases (1) and ( 2)). Similar work was performed in [START_REF] Saboori | Opacity-enforcing supervisory strategies via state estimator constructions[END_REF] for infinitestep opacity even though it cannot be so easily translated to LBO. It is shown that the approach for ISO can be extended by using a finite bank of supervisors and ensure infinite-step opacity in a minimally restrictive way.

Remark 10. In a nutshell, supervisory control resumes to find the supremal sublanguage that ensures opacity. In [START_REF] Ben-Kalefa | Opaque superlanguages and sublanguages in discrete event systems[END_REF], the authors further investigate language composition and show that opacity properties (with secrets being languages) are closed under union, but may not be closed under intersection. They also demonstrate the following results: (i) the supremal strongly opaque sublanguage exists and is unique;

(ii) the minimal strongly opaque superlanguage exists but may not be unique;

(iii) the minimal weakly opaque superlanguage exists but may not be unique;

(iv) the supremal not opaque sublanguage exists and is unique.

Enforcement of opacity properties

Opacity enforcement at run-time was introduced in Schneider ( 2000) and recently surveyed in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]. Enforcement does not restrict the system behavior anymore. Instead, it "hides" some of the system's output events whenever it is necessary. It is a non-intrusive approach compared to supervision. There are three main methods used for opacity enforcement:

1. Deleting occurrences of events from the output; 2. Adding events to the output; 3. Delaying the output.

Deletion of events

Considering a trace observed by the intruder, it may happen that the observation of the next event discloses the secret. A simple idea is to hide the occurrence of this event from observation at run-time (and possibly only this single occurrence) to avoid information flow.

Main work achieving this is synthesized in [START_REF] Cassez | Dynamic observers for the synthesis of opaque systems[END_REF] and [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF]. In this approach, the enforcer is a device called a mask. This mask restricts the observable outputs of the system either in a static or dynamic fashion. The latter case allows the mask to adapt to the intruder observation mapping (assumed to be dynamic) at each execution step.

Example 8. From [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF]. Consider the automaton G of Fig. 9, where the set of secret states is

X S = {2, 5}. If E O = E = {a,
b}, the system is not opaque (e.g., b * ab leads in the set of secret states). If either E O = {a} or E O = {b}, then it becomes opaque. Thus, one can define static sets of observable events, where at least one event will have to be permanently unobservable. This is a valid but very restrictive control. One could hide fewer events, the observable behavior of the system would be more important, and the control would be less restrictive. Thus, one should try to reduce as much as possible the hiding of events. On this particular example, we can be more efficient by using a dynamic mask that will render unobservable an event only when necessary. In this example, after observing b * , the intruder knows that the system is still in the initial state. However, if a subsequent a follows, then the intruder should not be able to observe b as this particular b would revel the system is in a secret state. We can then design a dynamic events hider as folat the beginning, everything is observable; when an a occurs, the mask hides any subsequent b occurrence and permits only the observation of a. Once an a has been observed, the mask releases its hiding by letting both a and b be observable again. Hence, event deletion is minimal.

In [START_REF] Zhang | Maximum information release while ensuring opacity in discrete event systems[END_REF] and [START_REF] Zhang | Maximum information release while ensuring opacity in discrete event systems[END_REF], the authors introduced the Maximum Information Release Problem which aims to restrict as few occurrences of output events as possible. They consider both strong and weak opacity. This work is very similar to the enforcement by means of a mask. The main difference comes from the initial definition of opacity used. They use the language inclusion definition from Lin (2011), while [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF] considers a state-based approach. This allows the Maximum Information Release Problem to adapt more easily to weak opacity, but the two methods are essentially the same.

Addition of events

Deleting events from the output was still considered as intrusive by some researchers. Even if the internal behavior of the system is no longer restricted (as it is with SCT), its actual output is.

To cope with this problem, Wu and Lafortune derived a method which artificially adds outputs to the set of observed events at run-time. This approach is called insertion functions (refer to Wu & Lafortune (2014); [START_REF] Wu | Verification and Enforcement of Opacity Security Properties in Discrete Event Systems[END_REF]). An insertion function is a monitoring interface at the system's output that changes it by inserting additional ("fake") occurrences of observable events.

Remark 11. These two approaches were suggested in [START_REF] Ligatti | Edit automata: Enforcement mechanisms for run-time security policies[END_REF], which proposed an enforcement mechanism called edit-automata. This mechanism featured the idea of "suppressing" and "inserting" actions in the current execution of a system but without direct application to information flow and opacity.

Delay of events

The last approach to enforce opacity properties is to delay emissions of one or several events which would have disclosed the secret, up to the point where the disclosure is of no interest anymore, or the system reaches a state in which opacity holds again. This method allows the full system behavior as well, but can only apply to secrets for which time duration is of concern. This approach has been presented in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF] and applied to K-step (weak) opacity in [START_REF] Saboori | Verification of k-step opacity and analysis of its complexity[END_REF]. It was later extended in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF] to K-step strong opacity.

Quantifying opacity

We presented in Section 3 the main formulations of opacity properties which have been considered in the literature. With these definitions, even decidable problems (refer to Section 6) only provide a yes/no answer to the system's opacity. Supervisory control (Section 4.2) and enforcement (Section 4.3) can manage to turn a non-opaque system into an opaque one.

However, this only accounts for logical models, with deterministic transition function, which is known to be a strong limitation in practice. Thus, researchers extended some definitions and tried to quantify opacity in a probabilistic setting. That is, how can one evaluate the possible information leakage of a system w.r.t. a given secret? Hence, for a given system's execution, we do not ask if there exists an observably equivalent execution, but how many there are, with a probabilistic measure taking into account the likelihood of such executions.

The reader should note that there is no absolute consensus on the interpretation of primitives. Depending on the authors and the problem considered, the model, the type of secret, and the meaning of probabilities can all vary to some extend. We attempt to formulate thereafter the problem statements as clearly as possible.

Quantification of language-based opacity

Initial work on quantification of opacity properties was presented in [START_REF] Lakhnech | Probabilistic opacity for a passive adversary and its application to chaum's voting scheme[END_REF] and reviewed in [START_REF] Bryans | Towards quantitative analysis of opacity[END_REF]. It provides quantitative measures of LBO in a probabilistic setting but it is limited to purely probabilistic models, based on labeled Markov chains.

In [START_REF] Bérard | Quantifying opacity[END_REF], two dual notions of probabilistic opacity are introduced:

(i) Liberal probabilistic opacity (LPO) measures the probability for an intruder observing a random execution of the system to be able to gain information he can be sure about. This definition provides a measure of how insecure the system is. LP O = 0 ⇔ LBO. Hence, computation of LP O is irrelevant for opaque systems.

(ii) Restrictive probabilistic opacity (RPO) measures the level of certitude in the information acquired by an intruder observing the system. RP O = 0 means the system is never opaque, whichever the running execution. Hence, computation of RP O express "how opaque" an opaque system is, which is irrelevant for non-opaque systems. 2015a) -Consider a Debit Card system in a store. When a card is inserted, an amount of money x to be debited is entered, and the client enters his/her pin number (all this being gathered under the action Buy(x)). The amount of the transaction is given probabilistically as an abstraction of the statistics of such transactions. Provided the pin is correct, the system can either directly allow the transaction, or interrogate the client's bank for solvency. In order to balance the cost associated with this verification (bandwidth, server computation, etc.) with the loss induced if an insolvent client was debited, the decision to interrogate the bank's servers is taken probabilistically according to the amount of the transaction. When interrogated, the bank can reject the transaction with a certain probability or accept it. This system is represented by the automaton of Fig. 10.

Let assume the intruder can only observe whether or not the bank is called. This can be achieved, for example, by measuring the time taken for the transaction to be accepted (it takes longer when the bank is called). Suppose the intruder wants to know if the transaction was worth more than 500, say euros. This is described by the opaque language L S = E * ("x > 1000" or "500 < x < 1000")E * .

This system is of course opaque, as there is always a chance of the bank being called (or not) whatever the transaction amount. It follows LP O = 0. However, if the intruder sees a call, there are rather high chances that the transaction was worth more than 500. RP O evaluates the level of confidence in this information. In this case, simple probabilistic calculi return RP O ≈ 0.718. Refer to [START_REF] Bérard | Quantifying opacity[END_REF] for more details on the computation procedure.

This work was extended in Bérard et al. (2015a) to Markov decision processes with infinite executions. Quantification is performed through the computation of a probabilistic disclosure (PD), which is the probabilistic measure that a run disclosing the secret has been executed. Several problems are addressed:

(i) Value: What is the P D of the system? (ii) General disclosure: Is P D bigger than a threshold? (iii) Limit disclosure: Is P D = 1? (iv) Almost-sure disclosure: does there exists a scheduler such that P D = 1?

(v) Almost-sure opacity: Is P D = 0?

Future extensions to this work would include the investigation of disclosure before some given delay, either as a number of steps in the spirit of [START_REF] Saboori | Verification of k-step opacity and analysis of its complexity[END_REF] or [START_REF] Saboori | Verification and enforcement of state-based notions of opacity in discrete event systems[END_REF], or for probabilistic timed systems with an explicit time bound. However this last perspective is seriously hindered by the undecidability of verification for dense time DES models [START_REF] Cassez | The dark side of timed opacity[END_REF].

Quantification of state-based opacity

Saboori first investigated the extension of state-based opacity properties to probabilistic models. Three probabilistic properties are introduced in [START_REF] Saboori | Probabilistic currentstate opacity is undecidable[END_REF],a, 2014) (i) Step-based almost current-state opacity considers the a priori probability of violating current state opacity following any sequence of events of length K. It requires this probability to lie below a threshold for all possible lengths k = (0, 1, . . . K). It is the extension of K-step opacity.

As for LBO, step-based almost current-state opacity aims to quantify the probability of the secret to be disclosed, which is only relevant for non-opaque systems.

(ii) Almost current-state opacity is equivalent to stepbased almost current-state opacity with no consideration regarding the length of the sequence of events, i.e., it considers the a priori probability of violating CSO following any sequence of events. It requires this probability to lie below a threshold. It is the extension of infinite-step opacity. Similarly, it is relevant only for non-opaque systems.

(iii) Probabilistic current-state opacity holds if the maximum increase in the conditional probability that the system's current state lies in the set of secret states (conditioned on a sequence of observations) compared to the case when no observation is available (prior probability) is bounded.

As for RPO, probabilistic current-state opacity is only relevant for opaque systems. Otherwise, the probability of being in a secret state reaches 1 eventually.

Example 10. From Saboori & Hadjicostis (2014) -Consider the probabilistic finite automaton from Fig. 11 with E 0 = E = {α, β, γ}. Assume X S = {4} and the initial probability distribution is π 0 = [1, 0, 0, 0, 0] (i.e., the system starts in state 0. The set of words disclosing the secret is referred to as L C = αγγ * βγ * (first γ is necessary to make sure the system is in the lower branch). The system is step-based almost current-state opaque with respect to a threshold θ if, for any k > 0,

P r k = t∈L C ,|t|=k

P r(t) < θ

There are no words in L C of length less than 3. P r 3 = P r(αγβ) = 0.045 and P r 4 = P r(t) = P r(αγγβ) + P r(αγβγ) = 0.018. It is not hard to see in this case that P r k decreases with k which implies that this system is step-based almost currentstate opaque for any θ > 0.045.

The set of words disclosing the secret for the first time is referred to as L P C = αγγ * β (i.e., no prefix of one of such words reveals the secret). The system is almost currentstate opaque with respect to a threshold θ if

P r ∞ = t∈L P C P r(t) < θ
In this case, P r ∞ = ∞ n=0 = 0.5 × 0.1 × (0.1) n × 0.9 = 0.05, which implies that this system is almost current-state opaque for any θ > 0.05.

Finally, assume now that X S = {3} and the initial probability distribution is π 0 = [0.2, 0.2, 0.2, 0.2, 0.2] . The system is probabilistic current-state opaque with respect to a threshold θ if

∀t ∈ E * O , ||π t (X S )|| -||π 0 (X S )|| ≤ θ
where π t (X S ) denotes the probability of being in a secret state after observing word t and ||.|| is vector 1-norm. We are interested in ensuring the confidence of being in the secret state is never higher than 0.75, that is, we want 0.75 -0.2 = 0.55-probabilistic current-state opacity. This does not hold, as after observing the sequence αβγ, the probability distribution vector π αβγ = [0, 0, 0, 0.79, 0.21] , and 0.79 -0.2 = 0.59 > 0.55.

These definitions were extended to ISO in [START_REF] Keroglou | Initial state opacity in stochastic des[END_REF] for systems modeled as probabilistic finite automata:

(i) Step-based almost initial state opacity captures the a priori probability that the system will generate behavior that violates initial state opacity after a certain number of events.

(ii) Almost initial-state opacity captures the a priori probability that the system will eventually generate behavior that violates initial state opacity.

Finally, [START_REF] Ibrahim | Secrecy in stochastic discrete event systems[END_REF] extended step-based almost current-state opacity from Saboori & Hadjicostis (2010a). Instead of the disclosure probability being below a threshold at each time step, it considers the probability of revealing the secret over the set of all behaviors. Two properties are introduced:

(i) S τ -Secrecy (stochastic-secrecy) holds if the probability of secret disclosure is always below τ . Secrecy ⇔ S 0 -secrecy.

(ii) I-S-Secrecy (increasing stochastic-secrecy) hold if whatever the threshold, there exists a size n of execution length beyond which every trace has a disclosure probability below the threshold.

Decidability and Complexity of opacity properties

Opacity is a very general property. As a result, many opacity problems are undecidable. This was demonstrated in [START_REF] Bryans | Opacity generalised to transition systems[END_REF] by reducing opacity verification to the reachability problem for Turing machines. It remains undecidable for general finite labeled transition systems if you do not restrict the class of observation function. Even when decidable, opacity problems are computationally complex to solve in general. This section synthesizes decidability and complexity results demonstrated in the literature.

Note that LBO, ISO, CSO, and IFO-referred to as general opacity problems -have been proven to be reducible into one another in polynomial time [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF], [START_REF] Chédor | Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems[END_REF]). Therefore, these problems have same decidability and complexity (since their complexity is, at least, polynomial).

We propose in Table 1 to 3 a general overview of decidability and complexity results published up to date in the literature. Several problems have been addressed by different approaches (e.g., initial-state opacity), which results in different order of complexity. When appropriate, we only kept the best (i.e., the smaller) order with the associated reference.

• Table 1 synthesizes decidability and complexity results of general opacity problems w.r.t the system's model and the observation mapping. Static observers are constrained to a fixed a priori interpretation of (un)observable events. Dynamic observers have different capabilities depending on previous events. Orwellian observers can also re-interpret past unobservable events on the base of subsequent observation. The first two are special cases of the latter.

• Table 2 gathers results from opacity quantification approaches.

• Finally, more specific complexity results are presented in Table 3.

Applications and related issues

Most opacity properties and validation strategies have been applied and evaluated in the literature. One reference case study is known as the Dinning cryptographers problem, introduced by [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF]; see e.g., [START_REF] Lakhnech | Probabilistic opacity for a passive adversary and its application to chaum's voting scheme[END_REF]; [START_REF] Bérard | Quantifying opacity[END_REF]; [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF]. It illustrates properties of ISO and CSO. Another ISO application is presented in [START_REF] Saboori | Verification of initial-state opacity in security applications of des[END_REF], related to encryption using pseudo-random generators. The same work also presents the problem of sensor network coverage for vehicle tracking (also detailed in Saboori & Hadjicostis (2011a)). Similar problems have been considered in [START_REF] Dubreil | Supervisory control for opacity. Automatic Control[END_REF], more precisely, the guidance of semi-autonomous agents traveling through finite networks, with the objective of preventing current positions from being known to adversaries that receive partial information from sensors (see Example 7). Opacity Issues in Games with Imperfect Information is another application considered in [START_REF] Maubert | Opacity issues in games with imperfect information[END_REF]. It exhibits relevant opacity verification problems, which noticeably generalizes approaches considered in the literature for opacity analysis in DES.

We mentioned in Introduction that opacity theory applies naturally in privacy-enhancing problems such as those we face nowadays in communication protocols design. In [START_REF] Saboori | Probabilistic currentstate opacity is undecidable[END_REF], the authors present a motivational example of the use of probabilistic opacity methods to evaluate the well-known anonymity protocol Crowds for the world-wide-web, initially presented in [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF]. More recently, Wu and Lafortune addressed the issue of Ensuring Privacy in Location-Based Services in Wu et al. (2014) and [START_REF] Wu | Verification and Enforcement of Opacity Security Properties in Discrete Event Systems[END_REF], using opacity enforcement techniques. To the best of our knowledge, this is the closest it gets to real-life applications so far.

Indeed, most of the current literature on opacity remains mainly theoretical. Nevertheless, there have been a few successful implementations. There are briefly introduced in the following subsection.

Tools and implementation

Saboori used the Umdes library (Umdes, 2009) to implement his verification method for infinite-step opacity, as described in [START_REF] Saboori | Verification of k-step opacity and analysis of its complexity[END_REF] and [START_REF] Saboori | Verification and enforcement of state-based notions of opacity in discrete event systems[END_REF]. Umdes is a library of C routines developed at the University of Michigan for studying DES modeled by finite automata.

Falcone developed a specific toolbox named Takos: a Java Toolbox for the Analysis of K-Opacity of Systems [START_REF] Takos | Takos: A java toolbox for analyzing the k-opacity of systems[END_REF]) to implement the K-step opacity enforcement method presented in Falcone et al. ( 2014) using delays. Finally, in Klai et al. (2014), a symbolic observation graph-based opacity checker has been implemented in C++ using a binary decision diagram package called BuDDy (BuDDy (1998)). Results are compared with the Takos toolbox on the also well known Dinning philosophers problem.

Conclusions and open problems

Over the past ten years, opacity applied to DES has been broadly studied. Almost all opacity problems proven decidable have a known complexity. Future trends are oriented toward infinite-state discrete event models, eventually coupled with probabilistic transition functions.

Some ongoing work tackles the verification of statebased opacity for some classes of Petri nets.

We already mentioned the similarities between opacity and diagnosis. There has been a quite decent amount of work related to prognosis (or predictability), which does not try to detect a fault but to predict that a fault will eventually happen in the future. It could be interesting to consider these approaches for the enforcement of opacity properties.

Moreover, in order to broaden the fields of applications, one could consider opacity validation from another perspective. Starting from a fully observable system and a given secret, which events one should "hide" in order to ensure opacity? This approach could provide a pragmatic methodology for people interested in designing opaque systems. Very recent work [START_REF] O'kane | Automatic design of discreet discrete filters[END_REF]) is a first attempt in this direction. It models both the information we need the system to reveal and those we want to be opaque as lower and upper bound filters. It shows that determining whether it is possible to satisfy both the distinguishability and indistinguishability constraints is NPhard, along with simulation results from their implementation.

As we are moving at high speed toward permanent connectedness, big data, user profiling and such, efficient tools to control the information we are disclosing and those to be kept private are becoming of paramount importance. Opacity is part of the answer. We believe it is now time to use this knowledge to handle the actual security and privacy problems we now face in our everyday life.

Romain Jacob was a final year Master student at ENS Cachan, France at the time of writing. After one year as visiting scholar at the University of California Berkeley, he completed his M.Eng. degree in Industrial Automation and Control from ENS Cachan (2015). He is now with the ETH Zürich where he is pursuing his Ph.D. on wireless sensor networks architectures and control. His research interests span from control synthesis and artificial intelligence to communication protocol, modeling and simulation.

Jean-Jacques Lesage received the Ph.D. degree from the Ecole Centrale de Paris and the "Habilitation diriger des recherches" from the University Nancy 1 in 1989 and 1994 respectively. He is currently Professor of Automatic Control at the Ecole Normale Suprieure de Cachan, France. His research interests are in the field of formal methods and models for synthesis, analysis and diagnosis of Discrete Event Systems (DES), and applications to manufacturing systems, network automated systems, energy production, and ambient assisted living.

Jean-Marc Faure received the Ph.D. degree from Ecole Centrale de Paris in 1991. He is currently Professor of Automatic Control and Automation Engineering at the Institut Superieur de Mecanique de Paris and researcher at Ecole Normale Superieure de Cachan, France. His research fields are modeling, synthesis and analysis of Discrete Event Systems (DES) with special focus on formal verification and conformance test methods to improve dependability of critical systems. J.-M. Faure is member of the IEEE and Associate Editor of the Journal T-ASE since 2012. He is chair of the steering committee of the IFAC workshop series "Dependable Control of Discrete Systems" and has served in many committees of IFAC and IEEE conferences.

Figure 1 :

 1 Figure 1: From Wu & Lafortune (2013) -Example 1 (LBO)

Figure 2 :

 2 Figure 2: From Wu & Lafortune (2013) -The system G discussed in Example 2 (CSO) and 4 (IFO)

Figure 3 :

 3 Figure 3: From Wu & Lafortune (2013) -The system G discussed in Example 3 (ISO)

Figure 4 :

 4 Figure 4: From Falcone & Marchand (2013) -System discussed in Example 5.

  7}, and X N S = X\X S . Secret states are shown as red square.

Figure 5 :

 5 Figure 5: From Falcone & Marchand (2013) -System discussed in Example 6.

Figure 6 :

 6 Figure 6: The main three approaches for ensuring opacity

Example 7 .

 7 From Dubreil et al. (2010). Let G be the transition system depicted in Fig.7(a), with X = {0, ..11}, X 0 = {0}, X S = {1, 5, 7, 11} and E = {u, d, c, s}. Let f be the transition function defined according to the arcs of the figure. Secret states are shown as red square.

Figure 7 :

 7 Figure 7: (a) G: Nominal model of the system; (b) G||S: Minimally restrictive supervisor ensuring opacity of G regarding the agent being at a secret floor.

Figure 8 :

 8 Figure 8: The three condensed state estimator; (a) A d 0 : first step, one losing configuration {11, 11}, 4 transitions to disabled; (b) A d 1 : second step, one losing configuration {1, 1}, 1 transition to disabled; (c) A d 2 : third step, no more losing configuration, minimally restrictive supervisor is reached.

Figure 9 :

 9 Figure 9: From Cassez et al. (2012) -Automaton G for Example 8

Figure 10 :

 10 Figure 10: From Bérard et al. (2015b) -The Debit Card system of Example 9 -,

Figure 11 :

 11 Figure 11: Example 10 -From[START_REF] Saboori | Current-state opacity formulations in probabilistic finite automata[END_REF]

  Definition 3 (LBO -No opacity). L S is no opaque w.r.t. L N S and P if L S is not weakly opaque w.r.t. L N S and P . Equivalently, L S

Table 1 :

 1 Decidability and complexity results for general opacity problems and regular languages

	System model	Observation Decidability	Complexity	Reference
		mapping
	Petri Nets	Static	Undecidable	-	Bryans et al. (2008)
	Finite labeled transition system	Static Dynamic Orwellian	Decidable Decidable Decidable	PSPACE-complete PSPACE-complete PSPACE-complete	Cassez et al. (2012) Bérard & Mullins (2014)
	Timed Automata (dense-time)	Static	Undecidable		Cassez (2009)
	Pushdown automata (PDA)	Static
	General case If X\X S is a visible PDA		Undecidable Decidable	-2-EXPTIME	Kobayashi & Hiraishi (2013)
	If X\X S and X S are visible PDA	Decidable	1-EXPTIME
	Recursive tile systems (RTS) Weighted RTS (CwRTS)	Static	Undecidable Decidable	-2-EXPTIME	Chédor et al. (2014)

Table 2 :

 2 Decidability and complexity results for quantified opacity problems

	Problem		Decidability	Complexity	Reference
	with controller observability being		Perfect/Partial	Perfect/Partial
							Bérard et al. (2015a)
	Value General disclosure	 	Decidable	Undecidable	Polynomial	-
	Limit disclosure	
	Almost-sure disclosure Almost-sure opacity		Decidable	Decidable for ω-regular secrets	Polynomial EXPTIME
	(Step-based) Almost current-state opacity		Decidable	PSPACE-hard
	Probabilistic current-state opacity opacity	Undecidable	-	Saboori & Hadjicostis (2014)
	(Step-based) Almost initial-state opacity		Decidable	-Keroglou & Hadjicostis (2013)
	S τ -Secrecy/I-S-Secrecy			Decidable	-		Ibrahim et al. (2014)

Table 3 :

 3 Other complexity results

	Problem	Complexity	Order	Reference
	Current-state opacity	PSPACE-complete	O(2 N )
	K-Step weak opacity	NP-hard	O((|E obs | + 1) K × 2 N )	Saboori (2011)
	Infinite-Step opacity	PSPACE-hard	-
	K-Step strong opacity	NP-hard	O((|E obs | + 1) K × 2 N )	Falcone et al. (2014)
	Initial-state opacity	PSPACE-complete	O(2 N )	Wu & Lafortune (2013)
	Resolution of initial-state	Polynomial	-	Hadjicostis & Keroglou (2014)
	LBO Strong-opacity	PSPACE-complete	-	Lin (2011)
	LBO Weak-opacity	Polynomial	-	Zhang et al. (2012)
	Static mask synthesis Dynamic mask systhesis	PSPACE-complete EXPTIME lower bound	--	Cassez et al. (2012)