Loïc Hélouët

Hervé Marchand

Laurie S L Ricker
email: lricker@mta.ca

Opacity with powerful attackers

come

Opacity with powerful attackers

Loïc Hélouët * Hervé Marchand * Laurie Ricker * * 1. INTRODUCTION Language-based security properties, such as non-interference or opacity, are a way to guarantee that a system fulfills some privacy requirements. The original work of [START_REF] Goguen | Security policies and security models[END_REF] is motivated by security issues: given a set of confidential actions performed only by users with high credentials, other users should not be able to infer from their observation whether a "high" action has occurred or not. The formal definition of non-interference states that occurrences of high actions should not affect what other users can see or do. Implicitly, this supposes that users have capabilities that allow them to check whether some actions are feasible, and can also be used to gain information about the current state of the system.

Non-interference is a limited class of properties: it only addresses questions of leakage from a high to a low level and, in the case of language-based interference, on the occurrence of high actions. However, the properties to protect are not always definable in terms of occurrences of actions from a given subset. A larger setting called opacity has been proposed [START_REF] Bryans | Opacity generalised to transition systems[END_REF] to consider hiding more general properties of runs. This notion formalizes the absence of information flow or, more precisely, the impossibility for an attacker to infer the truth of a predicate φ (it could be the occurrence in the system of some particular sequences of events, or the fact that the system is in some particular secret configuration). If the truth of this predicate can be inferred by an attacker, based on its knowledge of the system and the information deduced from its observations, then there is an information flow and the secret is revealed. This paper considers state-based opacity in a setting where attackers partially observe a system and, in addition to their observations, can query the system to discover the accepted inputs at the current state. In some sense, giving this additional power to attackers reintroduces the notion of capabilities from [START_REF] Goguen | Security policies and security models[END_REF]. We provide several different models of attackers, ranging from the usual attackers that can only observe a system and try to determine whether the system is currently in a sensitive secret state, to very powerful attackers that know at every instant the possible inputs accepted by the system. We then show how state-based opacity with powerful attackers can be checked. Lastly, we consider opacity enforcement: We bring back this question to the computation of a controller that forbids some inputs to the system to prevent an information flow. We show that opacity enforcement can be modeled as a game in which the controller tries to prevent an information flow, while the rest of the system may systematically perform the worst choices, allowing the attacker to gain information. An extended version (including proofs) is available at: https://hal.inria.fr/hal-01738169

PRELIMINARIES

Let Σ be an alphabet. A word w = a 1 . . . a n is an element of Σ * . We denote by the empty word. Given a subset Σ ⊆ Σ and a word w = a 1 . . . a n ∈ Σ * , the projection of w onto Σ is the word P Σ (w) obtained by erasing from w all letters from Σ \ Σ . Similarly, we denote by P -1 Σ (µ) the inverse projection of µ, i.e., P -1 Σ (µ) = {w ∈ Σ * | P Σ (w) = µ}. Definition 1. A Labelled Transition System G is a tuple (Q, q o , Σ, δ) where Q is a set of states with a distinguished element q o called the initial state, Σ is the set of events of G, δ ⊆ Q × Σ × Q is the transition relation.

The runs of G are sequences of transitions of the form ρ = q 0 a1 -→ q 1 . . . an -→ q n such that (q i , a i+1 , q i+1 ) ∈ δ for every i ∈ 0 . . . n -1. The word associated with a run ρ is the sequence of letters w = a 1 . . . a n (we also say that w labels run ρ). We denote by Run(G) the set of runs of G, and by L(G) the (regular) language of words that label runs of G. Furthermore, we assume that G is deterministic, i.e., ∀q ∈ Q, ∀a ∈ Σ, |(q, a, q )| ≤ 1. Note that as G is deterministic, for every word w ∈ L(G) there is a unique run ρ labeled by w. Thus, the map l : Run(G) → L(G) that associates runs with their labelings is a bijection.

We consider systems interacting with their environment, i.e., performing inputs and outputs. We assume that Σ is partitioned between the set of input events Σ ? , the set of output events Σ ! and the set of internal events Σ I . For a given state q ∈ Q, Γ(q) = {a ∈ Σ | ∃q , (q, a, q ) ∈ δ} denotes the active event set at q. Similarly, Γ ? (q) and Γ ! (q) denotes the set of input (respectively output) events that are admissible at state q. Given a set of states X ⊆ Q and a set of input events Σ ⊆ Σ ? , let Γ ? (X, Σ ) = {q ∈ X | Γ ? (q) = Σ }, i.e., the states of X that have exactly Σ as active input event set.

General notion of opacity

We consider a setting where a system should not leak any secret information that might be contained in the Preprints of WODES 2018 May 30 -June 1, 2018 Sorrento Coast, Italy actual run of the system. Such a secret can be depicted as a predicate φ over runs of the system, as in [START_REF] Bérard | Quantifying opacity[END_REF]. In this paper, we consider that the secret is represented as a subset of states S ⊆ Q. States of S can represent states in which a system is vulnerable to attacks, or states in which some confidential information is in use, and is not yet declassified. We denote by Run S (G) the set of runs of G ending in a state q ∈ S. We consider that attackers are agents of the system, which are equipped with observation and capabilities. They collect information online with executions of the system and try to infer with certainty whether the system's current state belongs to S. Definition 2. (Attackers). An attacker of G is a map A :

Run(G) → ((Σ ∪ { }) × O) * ,
where O is a finite alphabet of observed facts obtained through the use of capabilities. We further assume that attackers can be defined inductively, and from their final transitions: for a run ρ = q 0 . . . q n-1 an -→ q n , A(ρ) = A(q 0 . . . q n-1 ).obs A (a n , q n-1 ), where obs A : Σ×Q → (Σ×O)∪{ } defines the observation obs A (a, q) of the attacker when the system fires a from q.

The definition of attackers above is compositional, i.e., if ρ = ρ 1 .ρ 2 then A(ρ) = A(ρ 1 ).A(ρ 2 ), and transition-based, i.e., for a particular transition (q, a, q ), the observation is of the form (a, o) regardless of its position in a run. Note that an attacker is not necessarily aware of every move of the system as obs A (a, q) = for some actions and states, thus |A(ρ)| ≤ |ρ|. Let µ be an observation of the attacker, then the set of runs compatible with µ w.r.t. A is the set

[µ] A = {ρ ∈ Run(G) | A(ρ) = µ}. Definition 3. (Opacity). A secret S is opaque w.r.t. A iff ∀ρ ∈ Run S (G) there exists a run ρ in [A(ρ)] A such that ρ ∈ Run S (G).
Intuitively, opacity says that an attacker is not able to infer that a run is currently in a secret state based on its observation. Definition 2 allows us to decouple the information observed from transitions fired during a run, and information acquired from visited states. Though this definition is very generic, it encompasses many types of attackers, starting with the standard ones without capabilities, and whose observations are limited to a subset of actions Σ o ⊆ Σ. An attacker observes the system, and builds from its observation a belief, i.e., an estimation of a set of states in which the system could be.

Upon the arrival of a new observation, this belief can be updated as follows: Definition 4. (Belief update). Let G be a system, A be an attacker, X ⊆ Q be a belief, and (a, o) be an observation. We denote by δ A (X, (a, o)) the set of states X such that there exists a run ρ x,x from a state x ∈ X to a state of x ∈ X , and A(ρ x,x ) = (a, o). Belief updating extends to words and we can define a function ∆ A as: ∆ A (X, ) = X, ∆ A (X, w.(a, o)) = δ A (∆ A (X, w), (a, o)). Definition 5. (Observers). Let G = (Q, q o , Σ, δ). The observer of an attacker A is the deterministic automaton

Det A (G) = (X , X 0 , Σ A , δ A ), with X = 2 Q , X 0 = {q 0 } 1 and Σ A = Σ o ×O.
The construction of δ A depends on the power given to the attacker. However, with the restrictions given to attackers, Det A (G) is always a finite-state machine. We denote by T r A (G) = L(Det A (G)), the language generated by Det A (G). The classical notion of opacity can be generalized to observers with capabilities as follows: Proposition 1. Secret S is opaque w.r.t. G and A iff ∀ρ ∈ Run S (G), ∆ A (X 0 , A(ρ)) ⊆ S.

Proposition 1 says that a system is opaque if an attacker is not able to infer that a run is currently in a secret state by computing the beliefs obtained by synchronizing its observer automaton with the currently observed run. The verification of opacity is then reduced to the question of reachability of F = 2 S in Det A (G). This verification is PSPACE-complete [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF] in the standard setting where attackers observe only a subset of the labels attached to transitions (defined as attacker A 1 later in this section). As G is deterministic, Proposition 1 can be rephrased as a property of Det A (G). Furthermore, the PSPACE-completeness proof easily extends to the more general setting. Corollary 1. (of Proposition 1). Secret S is opaque w.r.t. G and A iff ∀µ ∈ T r A (G), ∆ A (X 0 , µ) ⊆ S. Corollary 2. Opacity of a system w.r.t. an attacker A is PSPACE-complete.

Attacker 1: Standard observer

A standard setting in opacity is to assume that the attacker A 1 observes the system through an interface (a subset of its actions). The attacker does not get information from the current state of the system, but is only aware of the last observable event triggered by the system. This can be modeled in our generic setting, by defining a single observed fact • (i.e., O = {•}) and a function obs A1 :

obs A1 (a, q) = if a ∈ Σ o , (a, •) otherwise.
Given a sequence w of G, the observation of the attacker A 1 is given by the natural projection P Σo (w). We denote by T r A1 (G) = P Σo (L(G)) this set of observations. Given an observation µ ∈ T r A1 (G), we denote by [[µ]] A1 = P -1 Σo (µ)∩L(G)∩Σ.Σ * o the set of sequences compatible with µ that end with an observable event. Given an observation µ ∈ T r A1 (G), we denote by ∆ o (X 0 , µ) = {δ(q 0 , [[µ]] A1 )}, the set of states in which the system can be after the observation of the trace µ, with X o = {q 0 }. Slightly abusing our notation, we use [[a]] A1 to denote the words for which projection on Σ o is a and that end with action a. Similarly, for any subset X ∈ 2 Q and any observable event

a ∈ Σ o , ∆ o (X, a) = {q ∈ Q | ∃q ∈ X, w ∈ [[a]
] A1 , q = δ(q, w)} denotes the set of states in which the system can be after the observation of a, knowing that the belief of the set of states was X ∈ 2 Q . The secret S is not opaque w.r.t. A 1 whenever there exists µ ∈ T r A1 (G) such that ∆ o (X o , µ) ⊆ S and the verification is reduced to a reachability problem as described in [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF].

ATTACKERS WITH ADDITIONAL CAPABILITIES

The attacker A 1 is the standard notion of a passive observer that is only informed of a subset of the system's actions. However, this model gives very little discriminating power to attackers. In this section, we propose several models of attackers that can collect additional information along runs of the system.

Attacker 2: an input-aware attacker

Let us first define an attacker A 2 that is aware of all the input events it might execute at any time during a run of the system. We assume that the set of inputs that A 2 can observe at any instant is a set Σ ? ⊆ Σ o , and that this set of available inputs is returned instantaneously after each move as an answer γ, with γ ⊆ Σ ? . We still consider that some actions remain invisible to the attacker. Hence, after the execution of each action a of the system:

• if a ∈ Σ o , the attacker receives the pair (a, γ);

• if a ∈ Σ uo , the attacker receives the pair ( , γ).

Note that each time an event is triggered in the system, A 2 is now aware of this occurrence, which can be seen as a "tick" for the attacker whenever the event is not observable. Within this setting, O 2 = 2 Σ ? and the function obs A2 is given by

obs A2 (a, q) = (a, Γ ? (δ(q, a))) if a ∈ Σ o , ( , Γ ? (δ(q, a))) otherwise.
The map A 2 directly follows from the definition of obs A2 . Note that even if A 2 observes possible inputs in the current state, some ambiguity remains on the current state, and there can be two distinct states q, q of the system such that Γ ? (q) = Γ ? (q ). Meanwhile, based on this new notion of an attacker, we redefine the various notions introduced in the previous sections in the classical framework.

An observation of the attacker is now a sequence from

(Σ o ∪ { }) × 2 Σ ? * .
The set of observations of A 2 that can appear when observing runs of G is denoted by T r A2 (G). Given an observable trajectory µ ∈ T r A2 (G), the set of compatible sequences is given by:

[[ ]] A2 = { } and [[µ.(a, γ)]] A 2 =      {w ∈ [[µ]] A 2 .a ∩ L(G) | q 0 w → q ∧ Γ ? (q) = γ}, if a ∈ Σo; {w ∈ [[µ]] A 2 .σ ∩ L(G) | σ ∈ Σuo, q 0 w → q ∧ Γ ? (q) = γ} if a = .
Similar to the case of A 1 , the computation of the observer, starting from a subset of states X, can be defined inductively. Upon the arrival of a new observation (a, γ), the update of belief X by attacker A 2 is defined by the function δ A2 (X, (a, γ)):

• δ A2 (X, ( , γ)) = Γ ? (X , γ), where X = {q | ∃q ∈ X, a ∈ Σ uo , (q, a, q ) ∈ δ} • For every a ∈ Σ o , δ A2 (X, (a, γ)) = Γ ? (X , γ), where X = {q | ∃q ∈ X, (q, a, q ) ∈ δ}
Then, for a sequence of observations, we can define:

• ∆ A2 (X, ) = X, and • ∆ A2 (X, µ.(σ, γ)) = δ A2 (∆ A2 (X, µ), (σ, γ))
for every µ ∈ T r A2 (G) and observation (σ, γ).

Attacker 3: input-aware attacker upon observation

We now model a type of attacker A 3 who is aware of all allowed input events that are admissible only after an observable action a ∈ Σ o occurs. We still assume that inputs belong to Σ ? ⊆ Σ o , and that the set of all allowed inputs is revealed after each observed action. Unlike attacker A 2 , attacker A 3 does not update its belief when the system performs an unobservable move. Within this setting, O 3 = 2 Σ ? and the function obs A3 is given by:

obs A3 (a, q) = (a, Γ ? (δ(q, a))) if a ∈ Σ o otherwise.
The set of observations of A 3 that can appear during runs of G is defined as

T r A3 (G) ⊆ (Σ o ×2 Σ ? ) * . Each observation in T r A3 (G) is a sequence of the form (a 1 , γ 1 )(a 2 , γ 2 ) . . . ,
where each a i is an observable event and γ i ⊆ Σ ? corresponds to the set of input events that are admissible after the observation of the event a i in the state of the system reached after executing a i . Given an observation µ ∈ T r A3 (G), the set of compatible sequences is given by:

[[ ]] A3 = { } and for a ∈ Σ o [[µ.(a, γ)]] A3 = {w ∈ [[µ]] A3 .a ∩ L(G) | q 0 w → q ∧ Γ ? (q) = γ}.
The refinement of a state estimate X by an observation (a, γ) is given by δ A3 (X, (a, γ)) = Γ ? (X , γ), where

X = {q ∈ Q | ∃q ∈ X, ∃ρ = q -→ . . . q , l(ρ) = a}.
The state estimates of the attacker, starting from a set of states X, is recursively defined as follows:

• ∆ A3 (X, ) = X, and

• ∆ A3 (X, µ.(a, γ)) = δ A3 (∆ A3 (X, µ), (a, γ)), for µ ∈ T r A3 (G) and (a, γ) ∈ Σ o × 2 Σ ? .

Attacker 4: an attacker informed of input changes

The last model of a passive attacker is informally defined as follows: we assume that the attacker A 4 can continuously observe the possible inputs to the system, but is not aware of state changes. Hence, if two consecutive states q, q in a run have the same inputs, and the move from q to q produces no observable events, then A 4 is not aware of any state change.

For A 4 , we have O 4 = 2 Σ ? and obs A4 is

obs A 4 (a, q) = ( , Γ ? (δ(q, a))) , if a ∈ Σuo ∧ Γ ? (q) = Γ ? (δ(q, a)) , if a ∈ Σuo ∧ Γ ? (q) = Γ ? (δ(q, a)) (a, Γ ? (δ(q, a)), if a ∈ Σo.
The observations of A 4 look like observations of A 2 , but with the difference that A 2 obtains one pair (σ, γ) for each transition in a run. An observer Det A4 (G), its transition relation δ A4 and ∆ A4 can be built as for our previous attackers.

• δ A4 (X, ( , γ)) = Γ ? (X , γ), where X = {q | ∃ρ = q a1 -→ q 1 . . . a k -→ q k a k+1 -→ q , l(ρ) = ∧∀i ∈ 1..k, Γ ? (q) = Γ ? (q i ) ∧ Γ ? (q) = Γ ? (q )} • For every a ∈ Σ o , δ A4 (X, (a, γ)) = Γ ? (X , γ), where X = {q | ∃q ∈ X, (q, a, q ) ∈ δ}
Then, for a sequence of observations, we can define:

• ∆ A4 (X, ) = X, and

• ∆ A4 (X, µ.(σ, γ)) = δ A4 (∆ A4 (X, µ), (σ, γ))
for every µ ∈ T r A4 (G) and an observation (σ, γ).

Attacker 5: an active attacker

We consider a slightly different attacker, namely one that is active. More precisely, attacker A 5 learns whether an input is active only by trying to play it. This attacker can observe actions from Σ o , and also test whether an input is allowed at the current state by attempting to enter this input. If an input a is allowed at a state q, then the system moves to the next state δ(q, a). If the input is not allowed, then the system remains in state q and the attacker gets the information not a, indicating that the input was ineffective. We also consider that A 5 can only test inputs to the system from the subset Σ att ⊆ Σ ? ∩ Σ o .

To reflect the fact that an input is not fireable in a state we introduce a new alphabet Σ not ? = {not σ|σ ∈ Σ ? }. In this setting, the alphabet of observed facts O 5 is given by

O 5 = Σ o ∪ Σ not ? , whereas the function obs A5 is obs A5 (a, q) =      , if a ∈ Σ uo (a, ), if a ∈ Σ o \ Σ att (a, a), if a ∈ Σ att ∩ Γ ? (q) (a, not a), if a ∈ Σ att ∧ a ∈ Γ ? (q). The set of observations is then defined as T r A5 (G) ⊆ (Σ o × (Σ o ∪ Σ not ? ∪ ))
* , while the transition relation of Det A5 (G) is:

δ A5 (X, (a, γ)) =              {q ∈ Q | ∃ρ = q -→ . . . q , l(ρ) = a, if a ∈ Σ o \Σ att ∧ γ = {q ∈ Q | ∃q ∈ X, (q, a, q ) ∈ δ}, if a ∈ Σ att ∧ γ = a {q ∈ X | q , (q, a, q ) ∈ δ}, if a ∈ Σ att ∧ γ = not a.
As it was for the other attackers, the transition relation of observer Det A5 (G) extends to words with ∆ A5 (X, µ.(a, γ)) = δ A5 (∆ A5 (X, µ), (a, γ)).

Comparing attackers

We can extend Corollary 1 to all attackers: Proposition 2. For every A i , i ≤ 5, S is opaque w.r.t. G and

A i iff ∀µ ∈ T r Ai (G), ∆ Ai (X 0 , µ) ⊆ S.
Let us now compare the discriminating power of attackers. We will say that attacker A i is less discriminating than attacker A j , and write A i A j (with fixed alphabets Σ, Σ o , Σ att , Σ ? ) iff for every automaton G and every set S of secret states, S is opaque w.r.t A j implies that S is opaque w.r.t A i . Looking at the information collected by each type of attacker, we can state the following. Proposition 3. We have the following relationships between attackers:

• A 1 A 2 , A 1 A 3 , A 1 A 4 , and A 1 A 5 • A 3 A 2 , A 4 A 2 ,
and A 5 A 2 Obviously, A 1 is the weakest attacker, as it only observes occurrences of actions in Σ o , while all other observers have at least this information when an observable transition is executed. It might be surprising that A 5 , which is active, is less powerful than A 2 . Indeed, A 5 can not always test all inputs of the system at the current state to get the same information as A 2 , since each test may force the system to move to another state.

ENFORCING OPACITY

If a system is not opaque, then one might try to control the system (or to restrict its behavior) so that the secret becomes opaque. This is achieved by dynamically forbidding or disabling certain events. Henceforth, we attach a controller to the system. This controller is in charge of deciding which inputs are allowed to occur or enabled at each point of an execution. We assume that the controller can observe all the events of Σ, but cannot control all of them. Thus, Σ, the alphabet of the system, is partitioned into Σ c , the set of controllable events, and Σ uc , the set of uncontrollable events. We assume that the controller has full knowledge of the system. Further, the controller is belief-based, i.e., it bases its decisions on its state estimate. Definition 6. A controller is a function C : L(G) → 2 Σ that provides the set of actions that are enabled after a sequence u ∈ L(G), with the constraint that ∀u ∈ L(G), C(u) ∩ Σ uc = Γ(δ(q o , u)) ∩ Σ uc (controllers cannot disable uncontrollable events). Given a state q, let C v (q) denote the set of valid control policies in q, i.e., all sets c ⊆ Γ(q) that respect c ∩ Σ uc = Γ(q) ∩ Σ uc .

Intuitively, when a sequence u ends in a state q, then a controller for G can only use a policy in C v (q). A controller C can be encoded by an automaton

A C = (Q C , q 0 C , δ C , Σ, λ C )
, where Q C is a not-necessarily finite set of states, δ C is a deterministic transition relation, and λ C : Q C → 2 Σ associates each state with a set of enabled events. Definition 7. Let G be an automaton, and let C : L(G) → 2 Σ be a controller, described by its automaton

A C . Then G/C = (Q G/C , (q 0 , q 0 C ), Σ, δ G/C
) is the automaton obtained by taking the synchronous product of G with A C , inductively built as follows.

• The initial state is (q 0 , q 0 C ) • If (q, q C )∈Q G/C , δ(q, a) = q , a ∈ λ C (q C ) and δ(q C , a)

= q C , then ((q, q C ), a, (q , q C )) ∈ δ G/C , and (q , q C ) belongs to Q G/C .

One can notice that L(G/C) ⊆ L(G). A question that immediately arises: how is the knowledge of an attacker affected by control? We assume that attackers do not know the control applied to the system. Nevertheless, this does not mean that control does not affect observations. For instance, consider a situation where the current state is q, Γ(q) = {?a, ?b}, but the controller disables ?a at q. We consider that the attackers get information about the actual set of available actions, i.e., when some control is in use. An attacker will receive information of the form (e, {?b}) when the system enters state q, where e is either or an action name. Let X be the current state estimate of the attacker. It can be refined by the observation, but recall that some actions that are not feasible from current state might actually be forbidden by a controller. Hence we define Refact(X, γ) = X \ {q ∈ Q | ∃e ∈ γ, q , q e -→ q }. This refinement of state estimate removes from X all states from which actions from γ are not fireable. We can now define the control and synthesis problem:

Control Problem: Given a system G, a secret S, an attacker A that observes Σ o , and a controllable alphabet Σ c ⊆ Σ, is there a controller C such that S is opaque for A in G/C ? Synthesis Problem: Given a system G, an attacker A, and a secret S such that a controller with controllable alphabet Σ c ⊆ Σ exists to keep S opaque for A, synthesize a map

C : L(G) → 2 Σ such that S is opaque for A in G/C.
In the rest of this section we will show that for passive attackers A 1 , A 2 , A 3 and A 4 , controllers are indeed strategies in finite co-reachability games. Within these games, positional strategies are sufficient to win, yielding finiteness of controllers. Definition 8. A two-player arena with partial information is a tuple H = (V, v 0 , M, -→, O 0 , O 1 ), where V is a set of positions, partitioned into V 0 V 1 (depicting player 0 and player 1's nodes, respectively); v 0 is the initial node of the arena; -→⊆ V × M × V depicts moves in the arena; and O i : V → Ψ i , i ∈ {0, 1} are observation functions, mapping vertices to a finite arbitrary observation alphabet. This can be used to model partial knowledge on the current vertex of the arena. Player i has to choose a move from a node in V i . A two-player co-reachability game is given by an arena and a winning condition W in ⊆ V . Player 0 wins the game if it can prevent the game from reaching a position in W in.

A play in an arena is either a finite sequence π = v 0 .v 1 .v 2 . . . v k or an infinite one π = v 0 .v 1 .v 2 . . . v k . . . . We denote by π(j) the j th vertex of play π. A play π is winning for player 1 (and losing for player 0) with the co-reachability condition W in if there exists j such that π(j) ∈ W in. A strategy for player i is a map σ i : V * .V i → 2 Acti , where Act i is the set of moves of player i.

In particular, we require that

• for every play π = v 0 .v 1 . . . v k with v k ∈ V i , σ i (π) ⊆ Act(v k ), where Act(v k ) is the set of legal moves from node v k in the arena. • for every pair of plays π, π such that O i (π) = O i (π ), σ i (π) = σ i (π ) (i.

e., strategies are consistent with observations).

A play is consistent with strategy σ i iff for every π(j) ∈ V i , π(j + 1) ∈ σ i (π(0) . . . π(j)). Player i wins in position v iff it has a strategy σ i such that for every strategy σ 1-i of player 1 -i, all plays starting from v and consistent with strategies σ i , σ 1-i are winning for player i.

We will say that a two-player game is a game of perfect information iff ∀v ∈ V, O 1 (v) = O 2 (v) = {v}. Otherwise, the games are called games with partial information. It is known that perfect information games with (co)reachability, Büchi, or parity objectives are determined : from each vertex, one (and only one) player has a winning strategy. Further, perfect information games need only positional strategies [START_REF] Grädel | Automata Logics, and Infinite Games : A Guide to Current Research[END_REF]. It is known that players have a winning strategy in a partial information game iff they have a belief-based strategy (Chatterjee and Doyen, 2010). Consequently, to decide whether a game is winning for player i, it is sufficient to build an arena containing the representation of the knowledge that each player has of the possible current state of the system. Then, solving a full-information game on this arena allows for the computation of belief-based strategies.

We are now ready to define a game that allows us to solve the opacity control and synthesis problem for each type of attacker. As attackers can only rely on their beliefs to reach a state estimate that is contained in S, and do not know the current state of the system, this will be a partial information game. We begin with attackers of type A 2 .

A controller for attackers of type A 2

In this game, the controller is player 0, the rest of the system is the player 1, and the attacker of the system is used to determine a winning condition on states. It might seem strange a priori to consider the system as an opponent to the controller, and not to the attacker. The reason for this is that attackers are passive. Hence they cannot guide the system to play the best actions leading to information leakage. However, to ensure that a secret is preserved, one can assume that the system, even if not malevolent, will always play the worst choice with respect to secrecy.

Let G be a system over alphabet Σ, S ⊆ Q be a set of secret states, q 0 be an initial state, Σ o be the set of events observed by attacker A 2 , and Σ c be a set of controllable events. The arena for this opacity control and synthesis problem is defined as a tuple H G,S,A2 = (V, v 0 , M, -→ H , O 0 , O 1 ) where:

• V = V 0 ∪ V 1 is a set of nodes. We have V 1 = Q × 2 Q × 2 Σ
. This set of nodes denotes positions of player 1 (the system). V 1 contains nodes of the form (q, X, Σ ), where q is the current state of G, X is the attacker's estimate of the set of possible states according to its observations, and Σ ⊆ Σ is the last choice of the controller, i.e., a set of actions that the controller allows from state q. Similarly,

V 0 = Q × 2 Q × Σ is
the set of positions of player 0 (i.e., the controller). Every node (q, X, a) ∈ V 0 represents the next current state q and the next possible state estimate X after performing action a. The initial node of the game is node v 0 = (q 0 , {q 0 }, ) ∈ V 0 , i.e., the system starts from its initial node, the attacker has perfect knowledge of it, and it is then up to the controller to decide which actions are allowed from the initial state.

In this node, symbolizes the fact that no action has yet been performed by the system. • M = M 0 ∪ M 1 is the alphabet of the game, where M 0 = Σ × 2 Σ represents moves of the controller, which makes a choice between the admissible control policies, and M 1 = Σ represents moves of the system.

• O 0 (v) = O 1 (v) = v, i.e.,
⊆ (V 1 × M 1 × V 0 ) ∪ (V 0 × M 0 × V 1
) and are built as follows: i) For every

c i ∈ C v (q o ), (v 0 , c i , (q 0 , {q 0 }, c i )) is a move of → H . Note that (q 0 , {q 0 }), c i ) ∈ V 1 . ii) If ((q, X), c) is a node of V 1 ,
and a ∈ c is an action allowed by the controller (and, hence, allowed from q), then ((q, X, c), (δ(q, a), X, a)) ∈→ H .

iii) Given a node (q, X, a) ∈ V 0 , transition ((q, X, a), (a, c), (q, X , c)) ∈→ H for all c ∈ C v (q). Let γ = c ∩ Γ ? (δ(q, a)), and X O,a = ∆ o (X, a). Then we have X = Ref act(X O,a , γ), i.e., the attacker's knowledge is updated, and includes states that are reachable from X when observing a, and which allow inputs from γ. Note that as the attacker is not aware of c i , X is the only deduction that an attacker of type A 2 can do. (See Fig. 1) (q, X, c) δ(q, a), X, a) δ(q, a), X 1 , c 1

γ 1 = c 1 ∩ Γ ? (δ(q, a)) X 1 = Ref act(X 0,a , γ 1 ) δ(q, a), X 2 , c 2 a ∈ Σ ∩ c (a, c 2 ) (a, c 1 )
Fig. 1. A part of the arena for the opacity game Fig. 1 shows several possible types of moves in arena H. Nodes of the controller (player 0) are represented as circles, and nodes of player 1 as rectangles. In node (q, X, c), the system decides to fire action a ∈ Σ ∩ c. The system then moves to a position (δ(q, a), X, a) meaning that the system will move to position δ(q, a). From this node, the controller has to decide which actions will be fireable from the next state δ(q, a), which will impact what is observable by the attacker. In Fig. 1, the controller has two possible choices, namely c 1 and c 2 . After a choice of the controller the move is performed and the attacker is informed of the move. Following the definition of an attacker of type A 2 , the observation produced is of the form (e, γ), where e = if the action played by the system is unobservable, and e = a if the performed action is observable. Similarly, when control c i is chosen, the set of possible inputs that attacker A 2 can observe is γ = Γ ? (δ(q, a)) ∩ c i . The state estimate of the attacker is updated accordingly, i.e., upon the choice of control c i the state estimate becomes

X = Ref act(∆ o (X, a), γ).
The objective of the controller is to avoid states of the form (q, X, c), where X ⊆ S, i.e., player 1 wins if it can force the system to one of these states. This is a classic turnbased co-reachability game, where the controller needs to choose valid control policies that avoid positions where the attacker's knowledge is contained in S. It is wellknown that perfect information (co)-reachability games are positional and determined, and can be solved in linear time by computing an attractor for the set of bad states that player 0 wants to avoid. It remains to show that a controller for opacity exists iff there is a wining strategy in this reachability game. Theorem 1. Let G be an automaton, S be a secret, and A 2 be an attacker. Secret S can be made opaque by some controller C iff player 0 has a winning strategy in the co-reachability game over arena H G,S,A2 with winning condition

W in = Q × 2 S × 2 Σ .
Note that belief-based controllers are not the only possible controllers. Consider the automaton of Fig. 2, where Σ = {a, u, c} and Σ o = {a, c}. To avoid reaching secret state S, a controller can forbid action a when the difference between the number of as and cs is equal to k. Such a controller never computes the state estimate of an attacker, but yet is sufficient to guarantee opacity. As already mentioned, positional strategies for two-player games with perfect information are sufficient. It is hence sufficient to design strategies that associate a decision to each node of the arena. Recall, however, that our games are played on an arena that represents the attacker's knowledge. This gives us the following corollary.

q 0 q f q 1,1 q 2,1 q 1,1 q 2,1 q 1,k q 2,k

A controller for attackers of type A 3 and type A 4

The technique used in Theorem 1 for attackers of type A 2 can be easily adapted for attackers of type A 3 and A 4 , and the opacity enforcement game remains a perfect information reachability game. The construction of the arena is very similar: the major difference resides in how the attacker's state estimate is updated. With attacker A 3 , for instance, a move from node ((q, X), c) ∈ V 1 with action a leads to a node ((δ(q, a), X, a), as was the case for attacker A 2 . Moves from nodes of the controller (nodes of V 0 ) of the form (q, X, a) lead to nodes of the form (q, X, c) if a is unobservable, and otherwise to nodes of the form (q, X , c), where X =Refact(X o , c ∩ Γ ? (δ(q, a)) is an update of the knowledge of A 3 , with

X o = ∆ o (X, a). q 1 , X, c q 2 , X, a 1 q 2 , X, c 1 q 3 , X, a 2 q n-1 , X, c q n , X, a n q n , X 1 , c 1 q n , X 2 , c 2 q 2 , X, c 2 a 1 ∈ Σ uo (a 1 , c 1 ) a 2 ∈ Σ uo (a n , c 1 ) (a n , c n ) a n ∈ Σ o (a 1 , c 2 )
Fig. 3. Part of the arena for attacker A 3 For attacker A 4 , the knowledge update is performed as soon at the input set changes. From a node of the form (q, X, c) ∈ V 1 the system can choose an action a allowed by the control c, and move to a state (δ(q, a), X, a, q). Notice that the state that is left is remembered. From a node (q , X, a, q) ∈ V 0 when choosing a control c, one moves to node (q , X, c) if Γ(q) = Γ(q ) and a is unobservable, and to node (q , X , c) otherwise, where X is computed as for attackers of type A 2 and A 3 . Opacity enforcement games remain unchanged on this slightly-modified arena.

ENFORCEMENT WITH ACTIVE ATTACKERS

With an active attacker A 5 , the game setting changes. Since attackers are active, they can have a strategy to drive the system into configurations leaking the secret S.

In the previous games designed to solve opacity for passive attackers, the partial observation of such an attacker is only used to designate which nodes of the arena are losing states for the controller. Observation functions for this kind of game are perfect information functions. Active attacker A 5 , on the other hand, can take decisions, and is now one of the players in the arena, although it has only a partial information on the actual state of G. We assume that the attacker is one of the processes of the system, and owns a subset of actions Σ att ⊆ Σ o that are performed only by him. These inputs can be performed/tested by the attacker immediately after each observable action. Yet, in this setting, the rest of the system can still perform actions that help A 5 acquire further information. We will hence distinguish nodes where the system plays, and nodes where the attacker chooses to input something to the system. This setting forces us to consider a new type of game, namely, three-player games, as introduced in [START_REF] Chatterjee | Games with a weak adversary[END_REF].

Definition 9. A three-player game is a tuple H = (Q, q 0 , δ, O i,i∈1..3 , obs i,i∈1..3 ), where Q is a set of nodes, q 0 an initial node, and δ :

Q × A 1 × A 2 × A 3 → Q
is a deterministic function that gives the successor state δ(q, a 1 , a 2 , a 3 ) of q when players 1, 2, 3 concurrently play actions a 1 , a 2 , a 3 . The game is turn-based if for every state q and every triple in A 1 × A 2 × A 3 the next state depends only on the action chosen by one of the players. For every player, O i ⊆ 2 Q is a partition of the set of states, and obs i : Q → O i is the function that assigns to q the unique observation of player i that contains q. A winning reachability condition is a subset of states W in ⊆ Q. An observation-based strategy for player i is a map

σ i : Q × O * i → Q.
Given a game arena H and a winning condition W in, the three-player reachability problem is to decide if ∃σ 1 , ∀σ 2 , ∃σ 3 such that the play that satisfies strategies σ 1 , σ 2 , σ 3 visits W in at least once.

We define an arena

H active G = (V, v 0 , δ, O i , obs i ) as follows. The set of nodes V is partitioned into V = V 1 ∪ V 2 ∪ V 3 ,
where V 1 represents positions of the attacker A 5 , V 2 are positions of the controller, and V 3 are positions of the system.

V 1 = {(q, X, c, att) | X ∈ 2 Q , C ∈ 2 Σ } V 2 = {(q, X, a, q ) | q, q ∈ Q, X ∈ 2 Q , a ∈ Σ} V 3 = {(q, X, c, sys) | X ∈ 2 Q , C ∈ 2 Σ }
We set v 0 = (q 0 , {q 0 }, , q 0 ) ∈ V 2 , i.e., the controller starts (as no action is played yet, the third component of the node is simply ). The transition relation δ is then computed as follows: the game allows only moves from V 1 to V 2 , from V 3 to V 2 and V 1 and from V 2 to V 3 . It is turn based, i.e., for every node n ∈ V i , δ(n, a 1 , a 2 , a 3 ) only depends on a i .

There exists a move from (q, X, c, sys) ∈ V 3 to (q, X, c, att) ∈ V 1 if Γ ? (q) ∩ c = ∅ (if we consider that Γ ? (q) ⊆ Σ o )2 . This move models the situation where the system does not perform an action, some inputs are feasible, and the system lets the attacker test them. There exists a move from (q, X, c, sys) ∈ V 3 to (q, X, a, δ(q, a)) ∈ V 2 if a ∈ c. This move models the system's decision to perform an action. Right after this decision, upon reaching the destination state, the controller has to take a control decision for inputs in Σ c . As with games that have attackers of type A 2 and A 3 , knowledge of A 5 is not updated by this move, which allows the controller to choose the next control decision.

A move from (q, X, c, att) ∈ V 1 to (q, X, a, δ(q, a)) ∈ V 2 exists if a ∈ c ∩ Γ ? (q). This move models input to the system performed by the attacker, and the consequences of this input (i.e., a state change). There exists a move from (q, X, c, att) ∈ V 1 to (q, X , c, sys) ∈ V 2 if a ∈ c ∩ Γ ? (q), with X = X \ {q ∈ X | a ∈ Γ ? (q)} if a ∈ Σ uc , and X = X, otherwise. Let us detail the computation of X . Node (q, X, c, att) is an attacker node, i.e., from this node, an attacker may want to test an input to the system to refine its estimate of the system's state. If this input ?a fails, then it is either because this input is not feasible from the current state, or because it was disabled by the controller. If the input is controllable, an attacker cannot distinguish between a state q f such that ?a ∈ Γ ? (q f ) and a state q a such that ?a ∈ Γ(q a ) but ?a ∈ c. If the attacker estimates that the system can be in state X before testing ?a, and subsequently learns that this input is not feasible, then its knowledge remains unchanged. On the other hand, if the input does not succeed, and ?a is not controllable, then X can be refined, since the current state of the system is necessarily a state q with ?a ∈ Γ(q). The controller allows initial moves from node v 0 to every node of the form (q 0 , c, sys) where Γ(q 0 ) ∩ Σ uc ⊆ c ⊆ Γ(q 0 ). All moves from a control node of the form n = (q, X, a, q ) ∈ V 2 , with a ∈ Σ o , are moves to nodes of the system of the form (q , X, c, sys) ∈ V 3 , with c ∈ 2 Σ . Notice that the knowledge of the attacker is not updated. This models the fact that unobservable moves do not bring information to the attacker. All moves from a control node of the form n = (q, X, a, q ), with a ∈ Σ o are moves of the form (q , X , c, sys) ∈ S 3 , with c ∈ 2 Σ , and X = ∆ o (X, a). The knowledge of the attacker is updated only according to the observation of action a, whereas for attacker A 5 , the observation of allowed inputs is performed actively, i.e., via a test made by the attacker.

We can now define the observation functions. The controller (player 2) has perfect knowledge of the system's state, so we define O 2 (n) = n for every node of the system. The system (player 3) also has perfect information on the current node of the system, so O 3 (n) = n. The attacker only has partial information, i.e., if n = (q, X, x, sys), then O 2 (n) = X. Thus, the attacker cannot differentiate states containing the same state estimate. Lastly, the winning condition is

W in S = {n | O 2 (n) ⊆ S}.
q, X, c, sys q, X, a, δ(q, a) q , X 1 , c 1 , sys q , X 1 , c 1 , att q , X 2 , c 2 , sys

a ∈ Σ o (a, c 2 ) (a, c 1 )
Fig. 4. An arena for the opacity game with an active attacker A 5 . States of the attacker are represented as red rectangles, states of the controller are green circles, and states of the system are blue rectangles.

Theorem 2. Let G be an automaton and S be a secret. The opacity of S w.r.t. an active attacker A 5 can be enforced by a belief-based controller iff player 2 has a winning strategy σ 2 against all strategies σ 1 , σ 3 of players 1 and 3 in the three-player reachability game over arena H active G with winning condition W in S .

In their most general form, three-player games of partial information are undecidable [START_REF] Reif | Universal games of incomplete information[END_REF], but [START_REF] Chatterjee | Games with a weak adversary[END_REF] showed that three-player games are decidable when player 1 is less informed than player 2. This is the case in our setting, as the attacker only has partial information on the current location in the arena, while players 2 and 3 have perfect knowledge of it. More precisely, [START_REF] Chatterjee | Games with a weak adversary[END_REF] show that threeplayer games are 2-EXPTIME complete, in general. The main idea of their proof is to show a reduction from a three-player game to an exponentially larger partial information two-player game with the same objective. Since partial information two-player games can be solved in EXPTIME, this yields the 2-EXPTIME upper bound for complexity of three-player games in general. A remark in Chatterjee and Doyen ( 2014) is particularly interesting: if player 2 has perfect information on the game, then the decision procedure is only in EXPTIME. We can even avoid an additional exponential blowup, as explained in the following corollary. Corollary 5. Given an automaton G, a set of secret states S and an active attacker A 5 , deciding existence of a controller ensuring opacity of G wrt active attacker A 5 can be solved in EXPTIME.

CONCLUSION

We have proposed a unified setting for opacity with passive and active attackers. For all attackers, opacity enforcement can be brought back to a partial-information game.

Related work : Opacity can be seen as the opposite of diagnosis problems. In diagnosis [START_REF] Sampath | Diagnosability of discrete event systems[END_REF], the question of interest is whether fault occurrences can be detected with partial observation of a running system. This question boils down to checking that there exists no pair of observationally-equivalent runs, one of which is faulty, the other one that is not. Ensuring diagnosability is a desirable property of a system. The goal of opacity, on the other hand, is to prevent an attacker from gaining certainty about properties of executed runs by making such runs observationally equivalent to a run that does not possess the property of interest. From an algorithmic point of view, techniques to ensure diagnosability consist of verifying the absence of pairs of runs, which can be done in polynomial time on the self-product of the specification. A contrario, to verify opacity we need to check properties of a whole equivalence class for traces, and not only a pair of runs. This requires modeling the complete knowledge of an attacker, and immediately yields an exponential blowup.

Opacity has been addressed in several settings since the work of [START_REF] Bryans | Opacity generalised to transition systems[END_REF] and [START_REF] Badouel | Concurrent secrets[END_REF]. Our approach does not only consist of checking whether opacity holds, but also provides the means to control a system in such a way that observed traces are not sufficient to decide whether the current state of the system is a secret one. Another enforcement technique was proposed by [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF]. This approach consists of dynamically changing the observation of an attacker using masks that hide a subset of transition labels that would otherwise be seen by the attacker. In this setting, the behavior of the system remains unchanged, but the control dynamically changes the way the system is observed. Our approach differs, as we forbid some behaviors. In fact, the approaches are orthogonal: one can easily design a system that is opaque with the help of masks, and not with control (e.g., when all events are uncontrollable). Conversely, one can easily design a system where masks are useless but where control can make a system opaque (for instance, when masks cannot reduce the set of observable events). Another technique to guarantee opacity is to allow systems to produce fictitious events as in [START_REF] Wu | Synthesis of insertion functions for enforcement of opacity security properties[END_REF]. This technique is orthogonal to our setting but it should possible to model games where an "active" systems that can insert dummy observations.

Future work: This work can be extended in several ways. First of all, it should be straightforward to consider enforcement of opacity for regular properties. Indeed, as soon as runs satisfying a property P are recognized by an automaton A P , enforcing opacity of runs of G satisfying P simply means enforcing state-based opacity in G × A P .

Other open questions deal with the power of attackers. So far, we have considered that the attacker is alone, and can observe and interact with the system. An interesting question is whether this setting can be extended to a coalition of players that run distributed attacks. We assumed that controllers of the system had full knowledge of the current state of the system. This allowed us to recast opacity control in a game setting with perfect observation for the controller. Now, if the controller is a particular component of the system, and observes only a subset of actions performed and has only partial information on the current global state of the system, the setting for enforcement questions changes. For passive attackers, the enforcement games become two-player games with partial information, which are exponentially harder to solve than perfect information games. In an active setting, opacity enforcement becomes a three-player game with partial information. Such games are usually undecidable [START_REF] Peterson | Multiple-person alternation[END_REF], but there is still a chance that opacity enforcement problems can be recast in a decidable setting of [START_REF] Chatterjee | Games with a weak adversary[END_REF].

Fig. 2 .

 2 Fig. 2. An automaton G that admits simple controllers Corollary 3. For an alphabet of fixed size, enforcement of opacity for an attacker of type A 2 is in EXPTIME.

Corollary 4 .

 4 Finite state (belief-based) controllers are sufficient to ensure opacity. Opacity controllers are of size in O(|G|.2 |G| ). There exist automata of size in O(n) in which opacity is ensured only by controllers of size in O(n.2 n ).

  both players have perfect knowledge of the game's positions.• Moves of the arena are a subset → H

The approaches in this paper work with sets of possible initial states, allowing attackers to start from beliefs that are not singletons.

Otherwise, we should write Γ ? (q) ∩ c ∩ Σo = ∅