We consider an extended version of sabotage games played over Attack Graphs. Such games are two-player zero-sum reachability games between an Attacker and a Defender. This latter player can erase particular subsets of edges of the Attack Graph. To reason about such games we introduce a variant of Sabotage Modal Logic (that we call Subset Sabotage Modal Logic) in which one modality quantifies over non-empty subset of edges. We show that we can characterize the existence of winning Attacker strategies by formulas of Subset Sabotage Modal Logic.
Graph under exam) and the former inhibits some attacks by erasing some subset of edges of the
Attack Graph itself. The goal of the Defender is to block the Attacker to reach some designated
states, while not blocking the entire system functionality. The kind of scenario that we have just
sketched is an example of extended sabotage game [
Our sabotage games differs from the one introduced by van Benthem because one of the player can erase an entire subset of edges of a given graph. To reason about such games, we introduce a variant of Sabotage Modal Logic that we call, for lack of wit, Subset Sabotage Modal Logic (SSML for short). The logic SSML is obtained by adding a modality ♦⊂ to the language of classical modal logic. The intended meaning of a formula ♦⊂ φ is “ ♦⊂ φ is true at a state s of a directed graph G iff φ is true at s in the graph G′ that is obtained from G by erasing a non-empty subset of its edges". We show that the model checking problem for SSML is decidable and that the existence of an Attacker winning strategy over an Attack Graph can be expressed by using an SSML formula.
In this section, we briefly present Sabotage Modal Logic (SML for short). Such logic was
proposed in 2005 by Van Benthem [
Given a sequence ρ, we denote is length as |ρ|, and its j + 1-th element as ρ j. For j ≤ | ρ|, let ρ≥ j be the suffix of ρ starting at ρ j and ρ≤ j the prefix ρ0 · · · ρ j of ρ. The empty sequence will be denoted by ϵ. Given a set of sequences X, we say that X is prefix-closed whenever given ρ ∈ X then ρ′ ∈ X for any prefix ρ′ of ρ. If X is a prefix-closed set of sequences, then ⟨X, ⊑⟩ is a tree where ⊑ denotes the prefix order. Accordingly, if X is finite, we will call leaves the ⊑-maximal elements of X. If G = ⟨V, E⟩ is a directed graph, a path is a sequence of vertices v0 · · · vn such that (vi, vi+1) ∈ E for all 0 ≤ i ≤ n − 1.
Given a non-empty set of atomic formulas, and a finite non-empty set Σ of labels, we define SML formulas by the following grammar:
φ ::= p | ⊥ | ¬φ | φ ∨ φ | ◇a φ | ♦a φ where p ∈ and a ∈ Σ. We define ⊤ ≐ ¬⊥. If φ and ψ are formulas, we define φ → ψ ≐ ¬φ ∨ ψ, ϕ ∧ ψ ≐ ¬(¬φ ∨ ¬ψ), □a ψ ≐ ¬ ◇a ¬φ and ■ a ≐ ¬ ♦a ¬φ.
We now define the structures that will serve as interpretation of SML-formulas. Definition 1. A rooted Kripke structure is a tuple M = ⟨S , s0, Σ, {Ra}a∈Σ, V⟩ where S is a nonempty set of states, s0 ∈ S is the initial state, Σ is a finite set of labels, {Ra}a∈Σ is a family of binary relations over the set of states such that there is one relation for each label in Σ; we will sometimes call elements of a binary relation edges. Finally, V : M → 2 is the evaluation function, assigning a set of atomic formulas to any state s ∈ S .
If M = ⟨S , s0, Σ, {Ra}a∈Σ, V⟩ is a Kripke structure and (s1, s2) ∈ Ra for some a ∈ Σ, we write M ∖ (s1, s2) to denote the Kripke structure obtained by erasing the pair (s1, s2) from the binary relation Ra.
The notion of satisfaction of a formula φ at a given state s of a Kripke structure M is inductively defined as follows (clauses for Boolean connectives are immediate and thus omitted): M, s |= ⊥ never M, s |= p iff p ∈ V(s) M, s |= ◇a φ iff there is a s′ ∈ S such that (s, s′) ∈ Ra and M, s′ |= φ.
M, s |= ♦a φ iff there is (s1, s2) ∈ Ra such that M ∖ (s1, s2), s |= φ We say that a formula φ is true in a rooted Kripke structure M (written M |= φ) iff φ is true at the initial state of M. As we can see from the above definition, the meaning of the ◇a -connective is the standard meaning in modal logic: a formula ◇a φ is true at a given state s of a Kripke structure whenever s is adjacent (with respect to an edge labeled by a) to a vertex s′ for which the property expressed by φ is true. The meaning of the ♦a -connective can be spelled out as follows: a formula ♦a φ is true at a given state s of a Kripke structure M whenever φ is true at s in the Kripke structure M′ that is obtained by erasing a pair (s′, s′′) from the relation Ra of M.
We conclude the section with the following theorem (the proof can be found in [
The term Attack Graph has been first introduced by Phillips and Swiler [
3. the Attacker’s profile (his capabilities, password knowledge, privileges etc.) and attack templates (Attacker’s atomic action, including preconditions and postconditions).
An attack path in the graph corresponds to a sequence of atomic attacks. Several works have
developed this approach, see e.g. [
An Attack Graph is said complete whenever the following condition holds: for every state q and for every atomic attack att, if the preconditions of the atomic attack hold in q, then there is an out coming edge from q labelled with att.
By abstracting all the data of the above discussion, one can see an Attack Graph as a directed graph togheter with a labeling of its vertices and edges. The labeling of vertices is used to specify which properties (the kind of properties mentionned in 1) are true at a certain vertex, while the edge labeling specifies the name of the attack action. We define an Attack Graph as follows. Definition 2. Suppose that the set contains an atomic proposition win. An Attack Graph is a tuple AG = ⟨S , s0, Σ, {Ra}a∈Σ, V, T ⟩ where: – ⟨S , s0, Σ, {Ra}a∈Σ, V⟩ is a rooted Kripke structure where the set S of states is finite and V(s) is non empty for any s ∈ S ; – T is a non-empty subset of S such that win ∈ V(s) for all s ∈ T .
The set T represents the set of target states of the Attacker.
Example 1. Consider the following scenario: an enterprise has a local area network (LAN) that features a Server, a Workstation and two databes A and B. The LAN also provided a Web Server. Internet’s access to the LAN are controlled by a firewall. Such scenario is decipted in Figure 1. Suppose that we know some vulnerabilities and that we have established that a malevolent user can make the attack listed in Table 1, e.g., by making att2 an Attacker can exploit a vulnerability related to the Server: as a precondition the Attacker needs to have root access to the Web Server and, as a postcondition, he will obtain root access to the Server. Then we can construct an
Attack Graph built from this set of atomic attacks and collecting possible attack paths as depicted in Figure 21. The Attacker’s initial state is a node in the Attack Graph. Let us suppose that the Attacker is in state s1 and wants to reach state s4. To get to this target, he can perform the sequences of atomic attacks att2, att4 or att3, att2, att4.
In the previous section, we saw that given a specific description of a system together with its vulnerabilities, we can generate a graph representing the dynamics of attacks that are possible over such system. Given a set of target states over such a graph, one can ask whether there is a path from an initial state to one of these target states, i.e., by reasoning over Attack Graphs, we can encode a security problem as a graph-reachability problem. Let us make one step more by adding a dynamic to such reachability problem. An Attack Graph represents a sequence of possible actions made by an Attacker to reach a specific goal. Let us add another character to this story, the Defender, whose objective is to counter the attack. Suppose that she has the power to dynamically deploy a predefined set of countermeasures: for instance by reconfiguring the firewall filtering rules, or patching some vulnerabilities, that is by removing one or several preconditions of an atomic attack. A given countermeasure c will prevent the Attacker from 1This Attack Graph is not complete w.r.t. our previous description, since some possible sequences of atomic attacks are not listed: for instance att1, att2, att3, att5 are not taken into account. longing a given attack att: deploying c is equivalent to removing all the edges in the Attack Graph labelled with att. In real situations, due to budget limitation or technical constraints, the set of available countermeasures may not cover all atomic attacks. Now that we have specified what is the Defender’s power, we can consider a turn based game between an Attacker and a Defender. Both players play on an Attack Graph ⟨S , s0, Σ, {Ra}a∈Σ, V, T ⟩. The Attacker’s goal is to reach one of the states in T , while the Defender’s goal is to prevent him from doing so. The Defender starts the game by selecting a certain countermeasure. By choosing such a countermeasure, she deletes a subset of edges of the Attack Graph. The Attacker take his turn and move from s0 to one of its successor along on the edges that have not being erased (if any). The game evolve following this pattern. The Attacker won if he can reach one of the states in T in a finite number of moves, otherwise the Defender wins.
Example 2. Consider again Figure 2. Suppose that the initial state is s1 and that the Defender has at her disposal a countermeasure c2 for attack att2, c4 for attack att4, and c5 for attack att5, but no one for the attacks att1 and att3 as reported in the last column of Table 1. The Defender starts the game by deploying countermeasure c3. The only edge of the Attack Graph labeled by att3 is the one going from s1 to s3; consequently, such edge is erased from the Attack Graph and the Attacker can only move to s2. The Defender takes again her turn and now deploys countermeasure c2. There are two edges that are labeled by att2 and both are erased from the Attack Graph. The Attacker moves from v2 to v4 and, since v4 is a target state, he wins the game.
There is a natural way to look at the games described above: at each round the Attacker can follow an edge from his current position in the given graph, but the Defender can choose a new graph (which is a subgraph of the current graph) missing a subset of edges. More precisely, the defender can choose to erase all edges that are labeled by the same atomic attack. Given a set of labels Σ, and an attack graph AG whose edges are labeled by members of Σ, a game that is played over AG in which the Defender can erase label that are in ∆ ⊆ Σ is called a ∆-game. A winning strategy for a ∆ game is called a ∆-winning strategy.
The games that we described in the previous section are nothing more than an insidious version
of sabotage games. In a sabotage game, one of the two players can delete an edge of the graph
when it is her turn to move. In our games, one of the two players can delete a subset of edges of
the graph when it is her turn to move. In [
More precisely, if M = ⟨S , so, Σ, {Ra}, V⟩ is a Kripke structure such that win ∈ V(s) for some s ∈ S and |S | = n ≥ 1 then M, so |= win ∨ λn− 1 if and only if there is an Attacker winning strategy for the sabotage game played over M. Such result is false in the case of the particular class of sabotage games that we have defined in the previous section, precisely because the Defender can erase at the same time all edges that are labeled by the same symbol at each step of the game. For instance, consider the following Attack Graph: s0 a a s1 s2 We can see that there is no {a}-winning strategy over M. If the Defender erases all the edges labeled with a, the Attacker would not be able to move from so to one of the winning states s1 or s2. On the contrary, the formula win ∨ λ2 = win ∨ (◇ ⊤ ∧ ■ ◇(λ1 ∨ win)) is true at so in M. This is because if the top-most a-edge is removed, the Attacker can pass from the lowermost edge to reach a winning state, and he can pass from the top-most one if the lower one is removed.
To speak about our particular games we introduce a variant of Sabotage Modal Logic. We call such variant of Sabotage Modal Logic, Subset Sabotage Modal Logic.
Definition 3. Given a non-empty set of atomic propositions and a finite non-empty set Σ of labels, formulas of Subset Sabotage Modal Logic (SSML, for short) are defined by the following grammar:
φ ::= p | ⊥ | ¬φ | φ ∨ φ | ◇a φ | ♦⊂a φ where p ∈ and a ∈ Σ. Given a rooted Kripke structure M = ⟨S , s0, Σ, {Ra}a∈Σ, V⟩, the definition of satisfaction of an SSML formula at a state s of a Kripke is defined inductively. Such definition is the same as SML for atomic proposition, negated formulas, disjunction and the diamond modality. It is defined as follows for the ♦⊂a -modality:
M, s |= ♦⊂a φ iff there is a non-empty subset E of Ra such that M ∖ E, s |= φ where M ∖ E denotes the structure M from which we have erased the subset E of edges. If φ is an SSML formula we define ■ ⊂a φ ≐ ¬ ♦⊂a ¬φ.
Remark 1. M, s |= ■ ⊂a φ if and only if for any non-empty subset E of Ra we have that M ∖ E, s |= φ, Ra included. This implies that if M, s |= ■ ⊂a φ then M ∖ Ra, s |= φ.
We now define the model checking problem for SSML. To show that the model checking problem for SSML is decidable, we reduce it to the model checking problem of SML. The idea of the proof is the following. We are considering a finite Kripke structure. As a consequence, any of its non-empty subset of edges is finite. We give a name ne to each edge e of M obtaining a Kripke structure M′. We remark that M |= ♦⊂a φ iff there is a finite, non-empty subset of edges {e1, . . . en} of Ra such that M ∖ {e1, . . . , en} |= φ. If φ is a SML formula then M′ |= ♦ne1 · · · ♦nen φ, that is M′ ∖ {ne1 , . . . nen } |= φ, where each nei is the name of edge ei. Thus, we need to give a translation from SSML-formulas to SML formulas. Such translation will be parametrized by Kripke structures, because we need to consider their subsets of edges.
Definition 4. Let M = ⟨S , so, Σ, {Ra}a∈Σ, V⟩ be a finite rooted Kripke structure. For all a ∈ Σ, let f : Ra → N be an injective function associating to each member e of Ra a natural number ne. We define the structure M ⊂ = ⟨S ⊂ , s⊂0 , Σ⊂ , {Ra}a∈Σ⊂ , V⊂ ⟩ as follows: – the set of states of M⊂ and its initial state are the same of M; – the set of labels Σ⊂ is ⋃︀a∈Σ{ne | e ∈ Ra}; – a pair of states (s, s′) ∈ Rne iff f (s, s′) = ne2; – the evaluation function V⊂ is V.
If E = {e1, . . . , ek} is a subset of edges of M and φ a formula, we write ♦nE φ as a shortcut for the formula ♦ne1 · · · ♦nek φ where each nei is the label corresponding to ei in M⊂ .
We define a function that maps an SSML formula φ to an SML formula (φ)⋆M. Such function takes as argument a Kripke Structure M and an SSML formula φ, and gives as result an SML formula (φ)⋆M. The function is defined on the structure of φ.
(p)⋆M (¬φ)⋆M ( ◇a φ)⋆M = = =
p ¬(φ)⋆M ⋁︀e∈Ra ◇ne (φ)⋆M
⋆ (⊥)M (φ ∨ ψ)⋆M ( ♦⊂a φ)⋆M = = =
⊥ (φ)⋆M ∨ (ψ)⋆M ⋁︀E∈2Ra∖∅ ( ♦nE (φ)⋆M)
Lemma 1. For any M = ⟨S , so, Σ, {Ra}a∈Σ, V⟩, for any SSML formula φ, for any state s ∈ S : M, s |= φ ⇐⇒
M⊂ , s |= (φ)⋆M From the above lemma and the fact the model checking problem is decidable for SML, we immediately deduce the following result.
Theorem 2. The model checking problem for SSML is decidable: if M = ⟨S , s0, σ, {Ra}a∈σ, V⟩ is a finite rooted Kripke Structure and φ an SSML formula, we can decide whether M |= φ or not.
It should be no surprise that we can express the existence of Attacker winning strategies for our games by using SSML: we have designed such logic with precisely this goal in mind.
Let AG = ⟨S , s0, {Ra}a∈Σ, V, T ⟩ be an Attack Graph and ∆ a non-empty subset of Σ. If φ is an SSML formula, we define the two SSML-formulas: ■ ⊂∆ φ ≐ ⋀︁ ■ ⊂a φ a∈∆ ◇ φ ≐ ⋁︁ ◇a φ a∈Σ 2This implies that each relation on M⊂ is either empty or a singleton.
A strategy is a plan of action. As it is logical, the plan is winning when it leads me to victory, whatever my opponent’s plan of action. Thus, a winning strategy can be expressed as an alternation of universally quantified sentences and existentially quantified sentences “for all actions of my opponent, there is an action that I can make that leads me to victory". Let us put ourselves in the villain’s shoes: suppose that we are the Attacker, and that, by playing, we have reached a certain state s of an Attack Graph AG. It is now Defender’s turn. If a have a winning strategy, I must be able to reach a successor state s′ of s in whatever subgraph AG′ of AG that is ∆-reachable from AG. Said differently, we must have that AG, s |= ■ ⊂∆ ◇ φ = ( ■ ⊂a ◇φ) ∧ · · · ∧ ( ■ ⊂b ◇ φ) for some formula φ that expresses the winning condition. Such formula is nothing but the SSML version of the one we have defined in 1.
n Definition 5 (Winning Formulas). The family {ψ∆}n∈N of Winning formulas is defined by induction on n as follows: ψn∆ = ⎨⎪⎪⎧win if n = 0 ⎪⎪⎩◇ ⊤ ∧ ■ ⊂∆ ◇(ψn∆− 1 ∨ win) otherwise (2) We provide the main result of our paper. Namely, that the existence of a winning Attacker ∆-strategy over an Attack Graph AG is equivalent to the truth of a winning formula over AG. The ⇒-direction of the theorem can be proved by induction on the size n of the Attack Graph. The ⇐-direction can be proved by contraposition.
Theorem 3. For any Attack Graph AG = ⟨S , s0, Σ, {Ra}a∈Σ, V, T ⟩ for any non-empty subset ∆ of Σ, if |S | = n, then AG, s0 |= win ∨ ψn∆− 1 iff there is a winning ∆-strategy over AG.
We have presented a natural class of two-player games over Attack Graphs. Such games are played by an Attacker and a Defender. The Attacker tries to reach some vertex of the Attack Graph while the Defender tries to prevent him from doing so. To do this, the Defender can eliminate subsets of graph arcs. Finally, we have introduced a variant of Sabotage Modal Logic, showed the the model checking problem for such logic is decidable and that we can express the existence of a winning strategies for our subset sabotage games by formulas of the logic.
The games we have described are perfect information games; both players know, at every point in the game, the location of the other player. This assumption is unrealistic: during a cyber attack, a possible Defender may not know what state an Attacker is in, and conversely, an Attacker may not be aware of changes made by the Defender to counter his attack. We would therefore like to extend our play model in order to include this type of imperfect information. From the Defender’s point of view this could be implemented as an equivalence class between Attack Graph states. From the Attacker’s point of view, on the other hand, we could think of a notion of weak bisimulation between Attack Graphs: the Attacker considers as equal two models that are bisimilar up to identification of some subset of arcs.
The model checking problem for SSML is decidable. However, we have not investigated the complexity of such problem (which must, however, be at least P-Space). We leave this investigation for future work. We suspect that a bisimulation notion for SSML logic can be obtained by slightly modifying the one for SML and that, at the same, a complete proof system for SSML can be obtained in terms of tableaux. In conclusion, we suspect that the satisfiability problem for SSML logic is undecidable. Indeed, the same problem is undecidable for SML and since our logic is SML in which we quantify over subset of arcs of a graph, our intuition tells us that the satisfiability problem for SSML can only be more di fficult than the one of SML.