Current-state opacity enforcement in discrete event systems under incomparable observations

Abstract

In this paper we tackle the opacity enforcement problem in discrete event systems using supervisory control theory. In particular, we consider the case where the intruder and the supervisor may observe different sets of events and neither of these sets needs to be contained in the other one. Moreover, there may be controllable events that cannot be observed by the supervisor. We propose a finite structure, called an augmented I-observer, to characterize the strings that will not leak the secret. Based on such a structure, a locally optimal supervisor enforcing current-state opacity is designed.

1 Introduction

Motivated by the concern about security and privacy in computer systems, communication protocols, etc., various notions of secrecy have been formulated, such as non-interference (Goguen and Meseguer 1982; Busi and Gorrieri 2004), anonymity (Reiter and Rubin 1998; Shmatikov 2004) and opacity (Hadj-Alouane et al. 2005; Bryans et al. 2005; Saboori and Hadjicostis 2008; Cassez et al. 2009; Wu and Lafortune 2013). Among them opacity is a useful notion for describing in a unitary framework some other security properties such as trace-based non-interference and anonymity (Bryans et al. 2008). In this paper we focus on an opacity property, called current-state opacity, in discrete event systems (DES). This opacity property was introduced in Bryans et al. (2005). Given a system, a subset of its states is considered as “secret”. There exists a malicious observer (called intruder) who attempts to detect when the system is in a secret state so that an attack can be launched. It is usually assumed that the intruder knows the structure of the system but has only partial observation of the system’s evolution. The system is said to be current-state opaque with respect to the given secret if based on its observations the intruder cannot determine with certainty if the current state of the system belongs to the secret.

It is proven that opacity verification problems in bounded systems are decidable (Tong et al. 2017a). There are several ways to verify opacity using the so-called observer automaton (Saboori and Hadjicostis 2008; Wu and Lafortune 2013; Lin 2011; Zhang et al. 2012) or Petri net based techniques (Tong et al. 2015a, b, 2016a, 2017b). Meanwhile, the opacity enforcement problem is another active topic that has received a lot of attention in the DES community. Given a system that is not opaque, the opacity enforcement problem consists in turning the system into an opaque one. Approaches to opacity enforcement may rely on supervisory control (Takai and Oka 2008; Dubreil et al. 2010; Ben-Kalefa and Lin 2011; Saboori and Hadjicostis 2012; Yin and Lafortune 2015), dynamically restraining the observability of events (Cassez et al. 2012), inserting additional events in the output behavior of the system (Wu and Lafortune 2014, 2015) and the runtime validation technique (Falcone and Marchand 2015). The aim of this work is to enforce current-state opacity (Bryans et al. 2005; Wu and Lafortune 2013) using supervisory control.

Given a system that is not current-state opaque with respect to a given secret, our purpose is to design a maximally permissive supervisor that restricts the behavior of the system to ensure that the controlled system is current-state opaque. There has been some related work on the design of supervisors to enforce opacity properties. In (Badouel et al. 2007), the authors consider the secret defined as a set of event sequences (such an opacity property is usually called language-based opacity) and a set of intruders having different observations. They assume that all events are observable and controllable to the supervisor, and show that the optimal supervisor always exists. Considering the same language-based opacity enforcement problem but with only one intruder, Dubreil et al. (2010, 2008) study a more general case where the supervisor may observe a set of events different from the one observed by the intruder in the presence of uncontrollable events. Saboori and Hadjicostis (2012) propose methods for designing optimal supervisors to enforce two different opacity properties: initial-state opacity and infinite-step opacity, with the assumption that the supervisor can observe all events. More recently, the common assumption that all controllable events are also observable (Dubreil et al. 2010, 2008; Saboori and Hadjicostis 2012; Badouel et al. 2007) is relaxed in Yin and Lafortune (2015) to enforce current-state opacity.

We point out that all the aforementioned works are carried out in the framework of finite automata and rely on Ramadge and Wonham’s basic theory of supervisory control for DES (Ramadge and Wonham 1989). Note that the objective of opacity enforcement is not concerned with liveness since opacity properties focus on a set of indiscernible runs from the perspective of the intruder instead of individual runs. In this paper we tackle the current-state opacity enforcement problem in the framework of finite automata and what distinguishes our work from the existing works consists in three aspects.

• No containment relation is assumed between the sets E _I , E _S of events observable by the intruder and by the supervisor, respectively. We call this general setting incomparable observations. In this sense, the problem considered here is more general than the one in Dubreil et al. (2010, 2008), Saboori and Hadjicostis (2012), Yin and Lafortune (2015), and Badouel et al. (2007).

• We also relax the assumption made in Takai and Oka (2008), Dubreil et al. (2010), Ben-Kalefa and Lin (2011), Saboori and Hadjicostis (2012), and Tong et al. (2016b) that all controllable events E _C should be observable.

• Finally, we consider the problem of enforcing opacity under the assumption that the intruder does not know that a supervisor is acting on the system. To address this problem, we define G-opacity of a language. We show that if a controlled system S u p/G is current-state opaque then its generated language L(S u p/G) is G-opaque but the converse does not hold in general case. However, if the intruder does not know the supervisor, L(S u p/G) being G-opaque is sufficient to guarantee that the intruder cannot detect if the current state belongs to the secret.

To be more clear, comparison between the proposed approach and previous ones (Dubreil et al. 2010; Yin and Lafortune 2015; Tong et al. 2016b) is summarized in Table 1. All the approaches are developed for deterministic finite automata but under different assumptions. The last row of Table 1 presents their computational complexity, where X is the set of states of the system and E _C is the set of controllable events. Note that the assumption that the intruder does not know the supervisor simplifies the problem of opacity enforcing due to the incomplete structural information available to the supervisor’s adversary.

Table 1 Comparison between the proposed approach and previous approaches

In this paper, first a structure called augmented I-observer is constructed. The augmented I-observer of a system is a deterministic finite automaton, where each state contains the current-state estimate of the intruder. Based on the augmented I-observer, evolutions of the system that satisfy current-state opacity can be characterized. Then we show that the current-state opacity enforcement problem can be reduced to the basic supervisory control problem under partial observation (Cassandras and Lafortune 2008). Note that the maximally permissive supervisor enforcing current-state opacity may not be unique. Thus we obtain a set of locally optimal supervisors where the adverb “locally” points out that the behavior of the controlled system under each of them is not strictly included in another. Finally, we show that based on the proposed approach it is possible to solve current-state opacity enforcement problem assuming that the intruder does not know the supervisor. To summarize, there are three main contributions of the paper:

• The definition of G-opacity of a language that enables us to formalize the opacity enforcement problem under the assumption that the intruder has no knowledge (or at most a partial knowledge) of the supervisor,

• The definition of a novel finite structure, the augmented I-observer, that enables one to relax the assumptions E _S ⊆ E _I (or E _I ⊆ E _S ) and E _C ⊆ E _S , and

• The demonstration that based on the notion of G-opacity and the augmented I-observer, the current-state opacity enforcement problem can be reduced to the basic supervisory control problem under partial observation, which is a result that has not been previously discussed in the literature. Then, locally optimal supervisors are achieved using appropriate supervisory control techniques.

This paper improves the results presented in the previous work (Tong et al. 2016b) to a more general setting, by removing the assumption that all events controllable by the supervisor should be observable. In addition, under the same assumptions, the proposed approach has lower complexity than the approach in Tong et al. (2016b).

The rest of this paper is organized as follows. Basic notions on automata and supervisory control theory are recalled in Section 2. Section 3 presents the definition of current-state opacity and the corresponding verification approach. In Section 4 the current-state opacity enforcement problem is formalized and a method for the synthesis of a locally optimal supervisor is proposed. Finally, this paper is concluded in Section 5, where our future work in this topic is also discussed.

2 Background

In this section we recall some elementary notions on automata and supervisory control. For more details, we refer the reader to Ramadge and Wonham (1989) and Cassandras and Lafortune (2008).

2.1 Automata

A system is modeled in this paper as a deterministic finite automaton (DFA) G = (X, E, δ, x ₀), where X is the finite set of states, E is the set of events, δ : X × E → X is the (partial) transition function, x ₀ ∈ X is the initial state. The transition function can be extended to δ : X × E ^∗→ X recursively: for all x ∈ X, δ(x, ε) = x and δ(x, σ e) = δ(δ(x, σ),e) for σ ∈ E ^∗ and e ∈ E. We denote by δ(x, σ)! the fact that σ is defined at x. The generated language of a DFA G = (X, E, δ, x ₀) is defined as

$$L(G)=\{\sigma\in E^{*}|\delta(x_{0},\sigma)!\}.$$

A string σ ^′ is a prefix of a string σ ∈ E ^∗ if for some σ ^″∈ E ^∗, σ = σ ^′ σ ^″. The prefix closure of a language L ⊆ E ^∗ is defined to be the language

$$\overline L=\{\sigma^{\prime}\in E^{*}|\sigma^{\prime}\sigma^{\prime\prime}\in L \text{ for some }\sigma^{\prime\prime}\in E^{*}\}.$$

If $\overline L=L$, we say that L is prefix-closed. Clearly, the generated language of a DFA is always prefix-closed, i.e., $L(G)=\overline {L(G)}$.

To model the partial observation of event sequences by the intruder and the supervisor, we denote by E _I ⊆ E and E _S ⊆ E the sets of events observable by the intruder and the supervisor, respectively. The natural projection $P_{I}:E^{*}\rightarrow E_{I}^{*}$ on E _I is defined as i) P _I (ε) = ε; ii) for all σ ∈ E ^∗ and e ∈ E, P _I (σ e) = P _I (σ)e if e ∈ E _I , and P _I (σ e) = P _I (σ), otherwise. Similarly, the natural projection $P_{S}: E^{*}\rightarrow E_{S}^{*}$ on E _S can be defined. Given an event sequence σ ∈ E ^∗, its projection w _i = P _I (σ) (resp., w _s = P _S (σ)) on E _I (resp., E _S ) is called an observation of the intruder (resp., supervisor). We denote by E _{U I} (resp. E _{U S} ) the set of events that cannot be observed by the intruder (resp., supervisor). We denote by E _C ⊆ E (resp., E _{U C} = E ∖ E _C ) the set of events that can (resp., cannot) be controlled by the supervisor.

Definition 1 (Unobservable Reach)

Given a system G = (X, E, δ, x ₀) and a state x, the unobservable reach R _I (x, ε) of x with respect to the intruder is

$$R_{I}(x,\varepsilon) = \{x^{\prime}\in X|\exists \sigma\in E_{UI}^{*}: \delta(x,\sigma) = x^{\prime}\}.$$

Obviously, x ∈ R _I (x, ε). Given an event e ∈ E _I , the e-reach R _I (x, e) of x is defined as R _I (x, e) = R _I (x ^′,ε), where x ^′ = δ(x, e).

2.2 Supervisory control

Given a system G = (X, E, δ, x ₀), the goal of supervisory control is to design a control agent (called supervisor) that restricts the behavior of the system within a specification language K ⊆ L(G). The supervisor observes a set of observable events E _S ⊆ E and is able to control a set of controllable events E _C ⊆ E. The supervisor enables or disables controllable events. When an event is enabled (resp., disabled) by the supervisor, all transitions labeled by the event are allowed to occur (resp., prevented from occurring). After the supervisor observes a string generated by the system it tells the system the set of events that are enabled next to ensure that the system will not violate the specification. A supervisor can be represented by S u p = (Y, E _S , δ _s , y ₀,Ψ), where (Y, E _S , δ _s , y ₀) is an automaton and

$$\Psi:Y\rightarrow \{E^{\prime}\subseteq E| E_{UC}\subseteq E^{\prime}\}$$

specifies the set of events enabled by the supervisor in each state. Figure 1 illustrates the paradigm of supervisory control under partial observation. Let σ ∈ L(G) be the string generated by the system and w _s = P _S (σ) be the corresponding observation of the supervisor. Then the set of events enabled by the supervisor is Ψ(y), where y = δ _s (y ₀, w _s ). System G under the control of a suitable supervisor S u p is denoted as S u p/G, and it satisfies L(S u p/G) ⊆ K.

Fig. 1

Supervisory control under partial observation

Definition 2 (Controllability)

Ramadge and Wonham (1989) Given a DFA G, a set of controllable events E _C , and a language K ⊆ L(G), K is said to be controllable (wrt L(G) and E _C ) if

$$\overline K E_{UC}\cap L(G)\subseteq \overline K,$$

where E _{U C} = E ∖ E _C .

In other words, the controllability of K requires that for any prefix σ of a string in K, if σ followed by an uncontrollable event e ∈ E _{U C} is in L(G), then it must also be a prefix of a string in K. It is known that controllability is preserved under arbitrary unions and consequently the supremal controllable sublanguage of a given language exists.

Definition 3 (Observability)

Ramadge and Wonham (1989) Given a DFA G, a set of controllable events E _C , a set of observable events E _S , and a language K ⊆ L(G), K is said to be observable (wrt L(G), E _S and E _C ) if for all $\sigma ,\sigma ^{\prime }\in \overline K$ and all e ∈ E _C such that σ e ∈ L(G), $\sigma ^{\prime } e\in \overline K$ and P _S (σ) = P _S (σ ^′), $\sigma e\in \overline K$ holds.

Roughly speaking, observability requires that supervisor’s observation of the system (i.e., the projection of σ on E _S ) provides sufficient information to decide after the occurrence of a controllable event whether the resultant string is still in $\overline K$. Unlike controllability, observability is however not preserved under union, therefore the supremal observable sublanguage of a given language may not exist. However maximal observable sublanguages exist, but are not usually unique.

Theorem 1

(Ramadge and Wonham 1989) Let K ⊆ L(G) be a prefix-closed nonempty language, E _C the set of controllable events and E _S the set of observable events. There exists a supervisor S u p such that L(S u p/G) = K if and only if K is controllable and observable.

Definition 4 (Supervisory Control and Observation Problem, SCOP)

Given a system G, a set of controllable events E _C , a set of observable events E _S by the supervisor, and a specification language K ⊆ L(G), find a locally optimal supervisor S u p such that:

• 1. L(S u p/G) ⊆ K

• 2. L(S u p/G) is maximal, i.e., for any other supervisor S u p ^′,

  $$L(Sup/G^{\prime})\subseteq K\Rightarrow L(Sup/G)\not\subset L(Sup/G^{\prime}).$$

A SCOP involves the system¹ G, the set E _S of events observable by the supervisor, the set E _C of events controllable by the supervisor, and the specification language K. To be concise, we call this problem SCOP(G, E _S , E _C , K).

Since the supremal observable sublanguage may not exist, there may not be the supremal controllable and observable sublanguage of a given language. Consequently, there may be multiple solutions to a SCOP and they are said to be “locally optimal” since under the control of the corresponding supervisors, the behaviors of the controlled system are incomparable.

The SCOP has been considered in the literature and many different methods have been proposed to solve it (Heyman and Lin 1994; Hadj-Alouane et al. 1996; Ru et al. 2014; Cai et al. 2015; Yin and Lafortune 2016a, b); in this work we briefly introduce the approach recently presented in Yin and Lafortune (2016a).

2.3 Approach based on the total controller

The authors of Yin and Lafortune (2016a) propose a structure, called total controller, based on which all locally optimal supervisors of the SCOP can be computed. Given a SCOP(G, E _S , E _C , K) with K = L(H), it is assumed, without loss of generality, that H = (X _H , E, δ _H , x _H,0) is a strict sub-automaton² of G. In other words, the language specification K of a SCOP is reduced to a state specification: a state x ∈ X is legal iff x ∈ X _H , i.e., σ ∈ K with x = δ(x ₀, σ). We denote by F = X ∖ X _H the set of forbidden states. In this subsection, such an approach is introduced through a numerical example.

Consider the system G = (X, E, δ, x ₀) in Fig. 2, where E _S = {a} and E _C = {a, b, c}. The set of forbidden states is F = {3,5}. The approach proposed by Yin and Lafortune (2016a) can be summarized as follows. First, construct a finite structure called a total controller, which enumerates all possible control policies of the system. In the total controller there are two types of states: Y-states $\mathcal {Y}\subseteq X$ in rounded boxes and Z-states $\mathcal {Z}=(Z,I)$ in rectangles, where Z ⊆ X and I is a control decision, i.e., it contains the set of events enabled by the supervisor. The initial state of the total controller is $\mathcal {Y}_{0}=\{x_{0}\}$. Y-states are driven to Z-states by control decisions. At each Y-state $\mathcal {Y}$, we enumerate all control decisions,³ and then the successor Z-state corresponding to a control decision is computed: Z is the set of states reachable from $\mathcal {Y}$ by firing unobservable events enabled by the control decision and I is the control decision. For instance, in Fig. 3, from Y-state {1}, for control decision {b} the Z-state reached is ({1,2},{b}) and for control decision {b, c} the Z-state reached is ({1 − 5},{b, c}). Z-states are driven to Y-states by observable events e ∈ E _S that are defined at a state in Z and enabled by the control decision I. The successor Y-state is the set of states reachable from a state in Z after the occurrence of e. For instance, from Z-state ({0},{a}) event a is enabled at 0 and is allowed by the control decision, therefore the Y-state reached is {1}.

Fig. 2

System G where E _S = {a}, E _C = {a, b, c} and states 3 and 5 should be unreachable

Fig. 3

Total controller of G in Fig. 2. Removing the state in the dashed box, the all inclusive controller is obtained

After the total controller is constructed, removing all the Y-states and Z-states that contain a forbidden state (i.e., 3 and 5 in this case) and the related arcs, the all inclusive controller is obtained. In Fig. 3 ({1 − 5},{b, c}) is such a state and should be removed. The all inclusive controller models all the control policies that enforce the specification language. Finally, after each Y-state we pick a control decision that is not a strict subset of any other decisions. A combination of those local maximal control decisions corresponds to a locally optimal supervisor.

It has been proven that the time complexity of the approach proposed in Yin and Lafortune (2016a) to solve the SCOP is $\mathcal { O}(|X||E|2^{|X|+|E_{C}|})$. In Fig. 3, each locally maximal control decision is colored. There are two optimal supervisors S u p ₁ and S u p ₂ (see Fig. 4) and the behaviors of the controlled system under different supervisors are L(S u p/G ₁) = {ε, a, a b} and L(S u p/G ₂) = {ε, a, a c}, respectively.

Fig. 4

The automaton structure of the two locally optimal supervisors: for S u p ₁, Ψ(0) = {a} and Ψ(1) = {b}; for S u p ₂, Ψ(0) = {a} and Ψ(1) = {c}

3 Current-state opacity and its verification

Current-state opacity has been defined in both automata and Petri nets frameworks (Bryans et al. 2005; Wu and Lafortune 2013; Tong et al. 2015a; Saboori and Hadjicostis 2007). In this section, we recall the definition of current-state opacity in finite automata and describe the approach in Saboori and Hadjicostis (2007) to checking this property.

Given a system, it is usually assumed that the intruder knows the system’s structure G but only the occurrence of some events can be detected by the intruder. Current-state opacity is defined as follows.

Definition 5 (Current-State Opacity)

Given a system G = (X, E, δ, x ₀), a secret S ⊆ X, and a set E _I of events observable by the intruder, G is said to be current-state opaque (CSO) wrt S and E _I if ∀σ ∈ L(G) such that δ(x ₀, σ) ∈ S,

$$\exists\sigma^{\prime}\in L(G):P_{I}(\sigma^{\prime})=P_{I}(\sigma)\text{ and }\delta(x_{0},\sigma^{\prime})\notin S. $$

In simple words, for any sequence of events σ that leads to a state in the secret, i.e., a secret state, there exists at least one sequence of events that reaches a non-secret state but produces the same observation P _I (σ) to the intruder. Therefore, when the intruder observes P _I (σ), it cannot conclude whether the current state is contained or not in the secret. Based on the system’s structure and its observation, the intruder can estimate the current state.

Definition 6 (Estimate of the Intruder)

Given a system G = (X, E, δ, x ₀) and an observation w _i of the intruder, the estimate of the intruder is defined as

$$\mathcal{C}_{I}(w_{i})=\{x\in X|\exists \sigma\in E^{*}: \delta(x_{0},\sigma)=x,P_{I}(\sigma)=w_{i}\}.$$

Therefore, if the intruder observes a sequence of events w _i , it knows that the current state could be any state in the set $\mathcal { C}_{I}(w_{i})$. Obviously, $\mathcal {C}_{I}(\varepsilon )=R_{I}(x_{0},\varepsilon )$. The estimate of the intruder after observing w _i can be iteratively computed by

$$ \mathcal{C}_{I}(w_{i})=\bigcup_{x\in \mathcal{C}_{I}(w_{i}^{\prime})} R_{I}(x,e), $$

(1)

where $w_{i}=w_{i}^{\prime }e$, $w_{i}^{\prime }\in E_{I}^{*}$, and e ∈ E _I (Cassandras and Lafortune 2008).

Theorem 2

(Saboori and Hadjicostis 2007) Let G = (X, E, δ, x ₀)be the system, S ⊆ X be the secret and E _I be the set of events observable by the intruder. The system is current-state opaque wrt S and E _I if and only if for all σ ∈ L(G),

$$\mathcal{C}_{I}(w_{i})\nsubseteq S,$$

where w _i = P _I (σ).

In simple words, to verify if a system is current-state opaque wrt the given secret, one needs to compute the intruder’s estimate $\mathcal { C}_{I}(P_{I}(\sigma ))$ for all words σ ∈ L(G) generated by the system and check whether $\mathcal {C}_{I}(P_{I}(\sigma ))\nsubseteq S$ holds. This can be done by constructing the observer (defined in Section 2.5.2 of Cassandras and Lafortune 2008) of the system for the intruder (i.e., wrt E _I ). The observer captures all state estimates of the intruder. More specifically, the state of the observer reached by w _i is equal to $\mathcal {C}_{I}(w_{i})$. Therefore, we can use the observer to verify current-state opacity. The algorithm to construct the observer can also be found in Cassandras and Lafortune (2008). Herein, it is not recalled for the sake of brevity.

Example 1

Consider the system in Fig. 5. Let E _I = {o ₂} and S = {5} (the secret state is in a box). The corresponding observer for the intruder is shown in Fig. 6. Since there exists w _i = o ₂ such that $\mathcal {C}_{I}(w_{i})=\{5\}\subseteq S$, by Theorem 2, the system is not current-state opaque wrt S and E _I .

Fig. 5

System G that is not CSO wrt S = {5} and E _I = {o ₂} in Example 1

Fig. 6

Observer of the system in Fig. 5 for the intruder

Let us introduce the following notion of opacity that is related to a sublanguage of the generated language of the system and is useful to formalize the result of the work.

Definition 7 (G-opaque Language)

Given a system G = (X, E, δ, x ₀), a secret S ⊆ X and a set E _I of events observable by the intruder, a sublanguage L ⊆ L(G) is said to be G-opaque (wrt S and E _I ) if ∀σ ∈ L such that δ(x ₀, σ) ∈ S,

$$\exists \sigma^{\prime}\in L(G): \delta(x_{0},\sigma^{\prime})\notin S,\quad P_{I}(\sigma)=P_{I}(\sigma^{\prime}). $$

Clearly, by Definitions 5 and 7, Corollary 1 follows.

Corollary 1

Given a system G = (X, E, δ, x ₀),a secret S ⊆ X and a set E _I of events observable by the intruder, G is current-state opaque wrt S and E _I if and only if L(G) is G-opaque.

In other words, CSO of a system G is equivalent to G-opacity of its generated language.

Proposition 1

Given a system G, a secret S ⊆ X, a set E _I of events observable by the intruder, and two G-opaque languages L ₁, L ₂ ⊆ L(G), then:

• i) L ₁ ∪ L ₂ is G-opaque;

• ii) ∀L ⊆ L ₁, L is G-opaque.

Proof

i) By assumption, L _i (with i = 1,2) is G-opaque. By Definition 7, for all $\sigma \in L_{i}, \mathcal {C}_{I}(P_{I}(\sigma ))\nsubseteq S$. Therefore, for all $\sigma \in L_{1}\cup L_{2}, \mathcal {C}_{I}(P_{I}(\sigma ))\nsubseteq S$, i.e., L ₁ ∪ L ₂ is G-opaque. ii) Given a subset L of L _i , for all $\sigma \in L, \mathcal {C}_{I}(P_{I}(\sigma ))\nsubseteq S$, i.e., L is G-opaque. □

The G-opacity property of a language is closed under union, and the supremal G-opaque sublanguage of a given language exists. Any sublanguage of a G-opaque language is still G-opaque.

Proposition 2

Let S u p/G be the controlled system of G = (X, E, δ, x ₀) under a supervisor S u p, E _I ⊆ E the set of events observable by the intruder, and S ⊆ X the secret. Given a language L ⊆ L(G), if is L S u p/G -opaque wrt S and E _I then L is G-opaque wrt S and E _I .

Proof

Assume that L is S u p/G-opaque. Then for all σ ∈ L such that δ(x ₀, σ) ∈ S, there exists σ ^′∈ L(S u p/G) such that δ(x ₀, σ ^′)∉S and P _I (σ) = P _I (σ ^′). Since L(S u p/G) ⊆ L(G), there also exists σ ^′∈ L(G) such that δ(x ₀, σ ^′)∉S and P _I (σ) = P _I (σ ^′). Therefore, L is G-opaque wrt S and E _I . □

If L(S u p/G) ⊆ L(G) is S u p/G-opaque (i.e., S u p/G is CSO) then L(S u p/G) is also G-opaque. Note that the converse of Proposition 2 is not true. In other words, even if the generated language L(S u p/G) of a controlled system S u p/G is G-opaque wrt S and E _I , the controlled system S u p/G may not be CSO wrt S and E _I . Therefore, CSO of S u p/G generally is a stronger requirement than L(S u p/G) being G-opaque.

Example 2

Consider the system G in Fig. 5 and its controlled system S u p ₂/G in Fig. 12b. Let S = {5}, E _I = {o ₁, o ₂}, E _S = {o ₁}, and E _C = {a, b, c}. Clearly, L(S u p ₂/G) is G-opaque wrt S and E _I but not S u p ₂/G-opaque. Namely, S u p ₂/G is not CSO wrt S and E _I . Indeed, when the intruder observes o ₁, if it knows the structure of S u p ₂/G, its estimate would be $\mathcal { C}_{I}(o_{1})=\{5\}\subseteq S$, i.e., S u p ₂/G is not CSO; on the contrary, if the intruder does not know the structure of S u p ₂/G, its estimate would be $\mathcal {C}_{I}(o_{1})=\{2,5,6\}\nsubseteq S$, i.e., the intruder is not able to discover the secret.

Example 2 also shows that if the intruder knows the supervisor S u p, to guarantee that the intruder does not discover the secret, L(S u p/G) should be S u p/G-opaque. On the contrary, if the intruder does not know the supervisor S u p, it is sufficient that L(S u p/G) is G-opaque. In the latter case, the problem is equivalent to synthesizing a supervisor S u p of G such that L(S u p/G) is G-opaque, which is clearly a weaker condition than S u p/G being CSO.

Note that G-opacity of L(S u p/G) may guarantee that the intruder cannot infer the secret also in some cases where the intruder knows that there is a supervisor acting on the system but has no sufficient information to determine it exactly. Suppose that the intruder knows that there is a supervisor and has some information on E _S and E _C but not precise. Then the intruder may synthesize an estimated supervisor S u p ^′ on G such that L(S u p ^′/G) is S u p ^′/G-opaque. However, if L(S u p/G) is S u p ^′/G-opaque, then the intruder is still not able to discover the secret.

Example 3

Consider Example 2 again. Suppose now that the intruder knows that there is a supervisor and believes the supervisor can observe $E^{\prime }_{S}=\{a,o_{1}\}$, and can control $E^{\prime }_{C}=\{b,c\}$, which are different from what the supervisor really can observe and control. The estimated supervisor synthesized based on $E^{\prime }_{S}$ and $E^{\prime }_{C}$ is S u p ^′ which disables event b when observing nothing. Consider the supervisor S u p ₂ defined in Example 2. It is easy to see that, L(S u p ₂/G) is S u p ^′/G-opaque wrt S and E _I . Therefore, under the control of S u p ₂ the intruder is still not able to infer the secret.

For simplicity, in the remainder of the paper it is directly assumed that the intruder does not know that a supervisor is controlling the plant to enforce opacity at all. Introducing such an assumption enables us to solve opacity enforcement using supervisory control in an efficient way. Meanwhile, imposing such an assumption is reasonable and meaningful. Indeed, this is realistic in many practical situations. Furthermore, it is interesting from a theoretical point of view since it provides some insights into tackling more general and complicated problems.

4 Current-state opacity enforcement by control

Given a system that is not current-state opaque wrt a secret, an interesting question is how to restrict its behavior or how to modify the observation structure such that the secret will never be revealed to the intruder. In this work we address the first issue using supervisory control theory (Ramadge and Wonham 1989). The supervisor will restrict the system’s behavior to prevent the evolutions leaking the secret. In this section, we present a novel approach to designing a locally optimal supervisor enforcing current-state opacity without assuming any containment relationship between E _S and E _I , and between E _C and E _S .

4.1 Problem formulation

The problem we want to solve in this work can be formalized as follows.

Definition 8 (Current-State Opacity Enforcement Problem, CSOEP)

Given a system G = (X, E, δ, x ₀), a secret S ⊆ X, a set E _I of events observable by the intruder, a set E _S of events observable by the supervisor, and a set E _C of controllable events, synthesize a locally optimal supervisor S u p such that

• 1. L(S u p/G) is G-opaque wrt S and E _I ;

• 2. For any other supervisor S u p ^′ such that S u p ^′/G is G-opaque wrt S and E _I it holds

  $$L(Sup/G)\not\subset L(Sup^{\prime}/G).$$

A CSOEP involves the system G, the set E _I of events observable by the intruder, the secret S, the set E _S of events observable by the supervisor and the set E _C of events controllable by the supervisor. To be concise, this problem is denoted as CSOEP(G, E _I , S, E _S , E _C ). A solution to the CSOEP is called a locally optimal supervisor.

Example 4

Consider again the system in Fig. 5. From Example 1 we know that the system is not current-state opaque wrt S = {5} and E _I = {o ₂}. Now we want to design a locally optimal supervisor S u p, so that L(S u p/G) is G-opaque. The sets of events observable ∖controllable by the intruder and the supervisor are shown in Table 2. In this case, E _I and E _S are not comparable, i.e., neither E _I ⊆ E _S nor E _S ⊆ E _I holds, and not all controllable events are observable, i.e., E _C ⫅̸ E _S .

Table 2 Observable and controllable events in Example 4

Proposition 3

There exists a solution to the CSOEP if and only if there exists a prefix-closed language K ⊆ L(G) such that

• 1. K is controllable (wrt L(G)and E _C ) and observable (wrt L(G), E _S and E _C );

• 2. K is G-opaque (wrt S and E _I );

• 3. For any other controllable, observable and G-opaque language K ^′⊆ L(G), K⊄K ^′.

Proof

By Theorem 1, the first item is a necessary and sufficient condition for the existence of a supervisor that restricts the behaviour of the system to K. Items 2 and 3 correspond to items 1 and 2, respectively, of Definition 8 that formalizes the requirements that a supervisor has to satisfy for being a locally optimal solution to the CSOEP.

□

Thus, to solve the CSOEP we have to compute a prefix-closed maximal controllable, observable and G-opaque sublanguage of L(G). It is known that the supremal observable sublanguage may not exist. Therefore such a maximal controllable, observable and G-opaque sublanguage, if it exists, may not be unique. In other words, there may exist a set of locally optimal supervisors.

In the next subsection, we introduce a structure, called augmented I-observer, based on which the supremal G-opaque sublanguage can be characterized and the optimal supervisors can be designed.

4.2 Synthesis of locally optimal supervisors

To design locally optimal supervisors, we have to characterize a maximal controllable and observable behavior of the system such that the secret will never be leaked. To do this, we need to first characterize the supremal G-opaque sublanguage of the system as the specification language K, and then compute a maximal controllable and observable sublanguage of K. Indeed, by Proposition 1 if a language is G-opaque, any sublanguage of it is still G-opaque. Unfortunately, the absence of specific containment relationships between sets E _I and E _S makes the solution via a single structure, as in Dubreil et al. (2010) and Yin and Lafortune (2015), tricky. In the following we provide an example where the approach in Dubreil et al. (2010) fails since none of the containment relationships E _I ⊆ E _S or E _S ⊆ E _I holds.

Example 5

Consider the system in Fig. 7. Let E _I = {a, d}, E _S = {b, c}, E _C = {c}, and S = {5}. Obviously, the system is not opaque wrt S and E _I since when the intruder observes ad it unambiguously knows that the current state is 5. According to Dubreil et al. (2010), observers of the system for the intruder and the supervisor should be constructed first. Then we have to compute the parallel composition N of these two observers to characterize the behavior that would leak the secret and that should be forbidden (see Fig. 8, states in shadow should be unreachable).

Fig. 7

System G that is not CSO wrt S = {5} and E _I = {a, d}

Fig. 8

Parallel composition N of the observers for the intruder and the supervisor

Finally, by computing the observer (wrt E _S ) of the parallel composition structure the optimal supervisor can be obtained. Without the assumption E _I ⊆ E _S or E _S ⊆ E _I , the parallel composition between the observers would introduce event sequences (e.g., σ = a b d) not belonging to P _o (L(G)), where P _o : E ^∗→ (E _I ∪ E _S )^∗. In the case at hand, being E _o = E, it is P _o (L(G)) = L(G). As a result, the behavior of the system would be over restricted. For instance, sequence ab does not leak the secret. However, it should be disabled: N tells that after uncontrollable event d occurs, sequence abd will lead to a state in shadow. Therefore, the obtained supervisor would not be optimal, or even no such an opacity enforcing supervisor exists (as in the case at hand). Note that assuming E _C = {o ₁} = E _S the approach in Dubreil et al. (2010) coincidentally works for Example 4 though neither E _I ⊆ E _S nor E _S ⊆ E _I holds.

In this work, we show that locally optimal supervisors for the CSOEP can be designed in two phases, without assuming E _I ⊆ E _S , or E _S ⊆ E _I , or E _C ⊆ E _S . First, by introducing a structure, called augmented I-observer, the supremal G-opaque sublanguage can be computed. Then, applying the method recalled in Section 2.3 to the augmented I-observer, the locally optimal supervisors can be designed.

The augmented I-observer of system G = (X, E, δ, x ₀) is a DFA denoted as $\mathcal {A}=(Q,E,\delta _{a},q_{0})$ and consists in the parallel composition of the observer for the intruder and the system G. In more detail, a state q ∈ Q of $\mathcal {A}$ is a pair (C _I , x), where C _I ⊆ X and x ⊆ X. The initial state of the augmented I-observer is q ₀ = (R _I (x ₀, ε),x ₀). Algorithm 1 illustrates the construction of the augmented I-observer. It also computes the set F = {q = (C _I , x) ∈ Q|C _I ⊆ S} that contains the set of states of $\mathcal {A}$ where the estimate C _I of the intruder is a subset of the secret. As proven in the following, set F allows one to identify a necessary and sufficient condition for current-state opacity of G, and to define the supremal G-opaque sublanguage of L(G).

Now we explain the main ideas behind Algorithm 1. The initial state of the augmented I-observer is q ₀ = (R _I (x ₀, ε),x ₀), i.e., the pair (set of states estimated by the intruder when observing nothing, initial state of the system). Given a state q = (C _I , x) ∈ Q and an event e ∈ E that is defined at x in G, using Algorithm 1, the generic state δ _a (q, e) = q ^′ = (C I′,x ^′) in the augmented I-observer is computed as follows. $C^{\prime }_{I}$ is updated to the new intruder estimate when event e is observed by the intruder; otherwise, $C_{I}=C_{I}^{\prime }$. State x ^′ is reached by the occurrence of e at x in G. If q ^′ is a new state, it is added to Q, otherwise Q does not change. The maximum number of states of the augmented I-observer is |X|× 2^|X|.

We finally note that the augmented I-observer differs from the parallel composition of observers proposed in Dubreil et al. (2010) and the parallel observer proposed in Tong et al. (2016b).

Example 6

Consider the problem in Example 4. Using Algorithm 1, the augmented I-observer is constructed and shown in Fig. 9, where states in F are in dashed boxes.

Fig. 9

Augmented I-Observer $\mathcal {A}$ of the system in Example 6, where states in F are in dashed boxes

Proposition 4

Let G = (X, E, δ, x ₀)be a system, E _I the set of events observable by the intruder, and S the secret. The augmented I-observer $\mathcal {A}=(Q,E,\delta _{a},q_{0})$ constructed using Algorithm 1 has the following properties:

• i) $L(\mathcal {A})=L(G)$ ;

• ii) $\{\sigma \in L(\mathcal {A})|\delta _{a}(q_{0},\sigma )\in F\}=\{\sigma \in L(G)| \mathcal {C}_{I}(P_{I}(\sigma ))\subseteq S\}$ .

Proof

• i) The statement follows from the fact that Steps 9 and 15 of Algorithm 1 consider all the events (and only them) that are defined at each state of G.

• ii) Let q = (C _I , x) = δ _a (q ₀, σ). By Steps 3 to 7, and 20 to 22 of Algorithm 1, and Eq. 1, $C_{I}=\mathcal { C}_{I}(P_{I}(\sigma ))$ holds. Therefore, δ _a (q ₀, σ) ∈ F if and only if $\mathcal {C}_{I}(P_{I}(\sigma ))\subseteq S$.

□

Moreover, by Steps 3 to 5 and 20 to 22 of Algorithm 1, there exists $\sigma \in L(\mathcal {A})$ such that $\mathcal {C}_{I}(P_{I}(\sigma ))\subseteq S$ if and only if F≠∅. Therefore, we have the following corollary showing that the augmented I-observer can also be used to verify current-state opacity.

Corollary 2

Given a system G, a secret S and the sets of events E _I and E _S , let $\mathcal {A}=(Q,E,\delta _{a},q_{0})$ be the augmented I-observer. G is current-state opaque wrt S and E _I if and only if F = ∅.

Proof

Follows from Steps 3 to 5 and 20 to 22 of Algorithm 1, Proposition 4 and Theorem 2. □

The following proposition shows how it is possible to compute the supremal G-opaque sublanguage of G using the augmented I-observer.

Proposition 5

The supremal G-opaque sublanguage of L(G) is $K=\{\sigma \in L(\mathcal {A})|\delta _{a}(q_{0},\sigma )\notin F\}$ .

Proof

First, we prove that K is G-opaque. Let σ ∈ K, δ _a (q ₀, σ) = q = (C _I , C _S ). Since q∉F, $C_{I}\nsubseteq S$, i.e., $\mathcal {C}_{I}(w_{i})\nsubseteq S$, where w _i = P _I (σ). Therefore, K is G-opaque. Now we show that K is the “largest” opaque sublanguage of L(G) and for any other opaque language L ⊆ L(G), L is contained in K. Let σ ∈ L and q = δ _a (q ₀, σ) = (C _I , C _S ). Since L is opaque, $\mathcal {C}_{I}(P_{I}(\sigma ))\nsubseteq S$, i.e., $C_{I}\nsubseteq S$, q∉F and σ ∈ K. Therefore, L is a subset of K and K contains all opaque sublanguages of G. □

Therefore, by means of the augmented I-observer we can compute the supremal opaque sublanguage of G, and by Propositions 1 and 3, the CSOEP can be solved by computing a maximal sublanguage of K that is prefix-closed, controllable and observable. The following theorem states that the CSOEP(G, E _I , S, E _S , E _C ) is equivalent to the SCOP$(\mathcal {A},E_{S},E_{C},K)$, i.e., based on the augmented I-observer locally optimal supervisors can be synthesized to enforce current-state opacity to a system G.

Theorem 3

The set of solutions to the CSOEP( G, E _I , S, E _S , E _C ) coincides with the set of solutions to the SCOP( $\mathcal {A},E_{S},E_{C},K$ ), where $\mathcal {A}$ is the augmented I-observer of G and $K=\{\sigma \in L(\mathcal { A})|\delta _{a}(q_{0},\sigma )\notin F\}$ .

Proof

We prove this theorem by showing that CSOEP(G, E _I , S, E _S , E _C ) and SCOP($\mathcal {A},E_{S},E_{C},K$) define the same supervisory control problem. By Proposition 1, any sublanguage of a G-opaque language is still G-opaque. By Proposition 5, K is the supremal G-opaque sublanguage of G. Therefore, condition 1 in Definition 8 can be rephrased as “ L(S u p/G) ⊆ K”, same as condition 1 in Definition 4. Moreover, $L(G)=L(\mathcal {A})$. Therefore, the CSOEP(G, E _I , S, E _S , E _C ) and the SCOP$(\mathcal {A},E_{S},E_{C},K)$ define the same supervisory control problem, and thus they share the same set of solutions. Namely, if S u p is a locally optimal supervisor of SCOP($\mathcal {A},E_{S}, E_{C},K$), then S u p is also a locally optimal supervisor of CSOEP(G, E _I , S, E _S , E _C ), and vice versa. □

In other words, CSOEP(G, E _I , S, E _S , E _C ) can be solved by synthesizing a locally optimal supervisor of $\mathcal {A}$ with F being the set of forbidden states.

Example 7

By Theorem 3, the CSOEP in Example 4 is reduced to the problem of finding a locally optimal supervisor S u p for $\mathcal {A}$ such that state q ₇ of $\mathcal {A}$ is not reachable in the controlled system. Applying the approach recalled in Section 2.2, first we construct the total controller in Fig. 10 and then, after removing all the states that contain forbidden state 7 (i.e., q ₇ in $\mathcal {A}$), we obtain the all inclusive controller. Finally, at each step we choose a local maximal control decision and all locally optimal supervisors are computed. There are two locally optimal supervisors: S u p ₁ and S u p ₂ with the same automaton structure shown in Fig. 11. For S u p ₁, Ψ(0) = {a, c, o ₁, o ₂} and Ψ(1) = {o ₁, o ₂}; for S u p ₂, Ψ(0) = {b, c} and Ψ(1) = {o ₁, o ₂}. The controlled systems under S u p ₁ and S u p ₂ are shown in Fig. 12.

Fig. 10

Total controller of $\mathcal {A}$ in Fig. 9. Removing the states in the dashed boxes, the all inclusive controller is obtained. For simplicity, in the diagrams, we use i (with i = 0,1,…,7) to denote state q _i in the augmented I-observer and omit all uncontrollable events in the control decisions, e.g., decision {} represents {o ₁, o ₂}, and so forth

Fig. 11

Supervisors of the CSOEP in Example 4: S u p ₁ and S u p ₂. They have the same automaton structure. However, for S u p ₁, Ψ(0) = {a, c, o ₁, o ₂} and Ψ(1) = {o ₁, o ₂}; for S u p ₂, Ψ(0) = {b, c, o ₁, o ₂} and Ψ(1) = {o ₁, o ₂}

Fig. 12

Controlled system under different locally optimal supervisors in Example 7

4.3 Computational complexity analysis

According to the previous analysis, in the worst case the number of states of the augmented I-observer is |X|× 2^|X|, where X is the set of states of G. Since the complexity of solving the SCOP is $\mathcal {O}(|Q||E|2^{|Q|+|E_{C}|})$, where Q is the set of states of the augmented I-observer, the worst-case complexity of solving the CSOEP is $\mathcal {O}(|X|\times 2^{|X|}|E|2^{|X|\times 2^{|X|}+|E_{C}|})$, i.e., double exponential in the number of states of G. It is clear that one exponential order comes from the construction of the augmented I-observer and the other one comes from the method adopted in this paper to solve the SCOP.

We point out that in some cases (e.g., finding a near optimal supervisor (Heymann and Lin 1994; Ushio 1999), on-line synthesizing the supervisor Cai et al. 2015), the complexity of solving the SCOP may decrease and consequently so would be the complexity of solving CSOEP.

Assuming that the intruder has no knowledge of the supervisor, the proposed approach can solve the same problems in Dubreil et al. (2010), Yin and Lafortune (2015), and Tong et al. (2016b) with the same or lower complexity: exponential or double exponential, respectively. Consider the problem in Dubreil et al. (2010) where E _I ⊆ E _S = E, E _C ⊆ E _S . The augmented I-observer contains all observations of the supervisor (i.e., $P_{S}(L(\mathcal {A}))=L(\mathcal {A})$). Therefore, the augmented I-observer can be used to synthesize the supervisor directly. Moreover, due to E _C ⊆ E _S the complexity of the proposed approach reduces to $\mathcal {O}(|X|\times 2^{|X|})$ as same as the complexity of the approach in Dubreil et al. (2010). On the other hand, the complexity of solving the problem in Tong et al. (2016b) (where E _S and E _I are incomparable but E _C ⊆ E _S ) using the proposed approach is $\mathcal {O}(2^{(|X|\times 2^{|X|})})$, lower than that of the approach in Tong et al. (2016b). In addition, if either E _S ⊆ E _I (or E _I ⊆ E _S ) or E _C ⊆ E _S holds, the supervisory synthesis problem considered in the paper cannot be solved using the approaches in Saboori and Hadjicostis (2012), Yin and Lafortune (2015), Dubreil et al. (2008), and Tong et al. (2016b).

5 Conclusions and future work

In this paper, we proposed a novel approach to solve the problem of current-state opacity enforcement in discrete event systems using finite automata. By constructing the augmented I-observer, all the strings that will leak the secret can be characterized. Based on the augmented I-observer, current-state opacity can be checked and a synthesis algorithm was provided to design a locally optimal supervisor, without assuming the existence of containment relationships between E _I and E _S , or between E _C and E _S .

There are several directions along which the current research could be extended. First we note that the proposed approach can be applied to systems modeled by nondeterministic finite automata (NFA). In this case the obtained augmented I-observer will be an NFA as well. We also point out that the proposed approach can be extended to Petri nets, a model that is more powerful than finite automata. Moreover, some structural properties of Petri nets may be useful to further reduce the computational complexity and this is one direction for our future research. The other direction is to develop a unified structure that combines the features of augmented I-observer and the total controller so that the complexity of solving CSOEP could decrease.