# Partially-Observable Security Games for Automating Attack-Defense Analysis

Narges Khakpour<EMAIL_ADDRESS>School of Computing, Newcastle
UniversityNewcastle upon TyneUK Department of Computer Science and Media
Technology, Linnaeus UniversityVäxjöSweden and  David Parker
<EMAIL_ADDRESS>Department of Computer Science, Oxford
UniversityOxfordUK

###### Abstract.

Network systems often contain vulnerabilities that remain unfixed in a network
for various reasons, such as the lack of a patch or knowledge to fix them.
With the presence of such residual vulnerabilities, the network administrator
should properly react to the malicious activities or proactively prevent them,
by applying suitable countermeasures that minimize the likelihood of an attack
by the attacker. In this paper, we propose a stochastic game-theoretic
approach for analyzing network security and synthesizing defense strategies to
protect a network. To support analysis under partial observation, where some
of the attacker’s activities are unobservable or undetectable by the defender,
we construct a one-sided partially observable security game and transform it
into a perfect game for further analysis. We prove that this transformation is
sound for a sub-class of security games and a subset of properties specified
in the logic rPATL. We implement a prototype that fully automates our approach
and evaluate it by conducting experiments on a real-life network.

##  1\. Introduction

In today’s increasingly complex networked environments, many vulnerabilities
still remain in the system after being discovered because of, for example, the
lack of a patch or knowledge to fix them, cost factors or organizational
preferences for availability and usability over security (Wang et al., 2008).
Furthermore, hosts and services are frequently added and changed in a complex
network, introducing new vulnerabilities and opportunities for attackers to
exploit the system (Yuan et al., 2014); a user may connect a new device to or
disconnect it from an internal network, bringing new vulnerabilities or
facilitating the exploitation of existing ones. In such dynamic and uncertain
environments, traditional offline and manual methods to analyze
vulnerabilities and defend a network become inadequate. _Enhancing the defense
capabilities for network security by employing online and semi-automatic
mechanisms has become essential._

Threat modeling is a common technique used to specify, discover and reason
about security weaknesses and vulnerabilities (Kordy et al., 2013; Hong et
al., 2017; Ramos et al., 2017; Ou et al., 2005). It uses models to represent
the strategies employed by attackers/defenders to attack/defend a system. A
wide range of models and languages has been proposed for threat modeling and
analysis (see (Hong et al., 2017; Widełet al., 2019; Kordy et al., 2013) for a
survey). Attack graph-based (Sheyner et al., 2002) and attack tree-based
(Weiss, 1991) approaches are among the most common ones. Different formal
methods have been already used for threat modeling and analysis, e.g. Petri-
nets (see (Kordy et al., 2013) for a survey), timed automata (Gadyatskaya et
al., 2016) and situation calculus (Samarji et al., 2013). _While attack trees
have received a lot of attention in the past, the construction of attack trees
is often done manually or semi-automatically, which is a serious shortcoming
when developing automated online analysis techniques_. In contrast, attack
graphs can be generated fully automatically using formal approaches, such as
model checking (Sheyner et al., 2002) or logic-based reasoning (Ou et al.,
2005), which makes them a suitable candidate for automated analysis.

The opposing objectives and dependent strategies of network attack and defense
are very well-suited to game theoretic approaches, which allow us to model the
interactions between the attacker and the defender. Game theory has already
been applied to analyze network security in different research communities in
recent years (Durkota et al., 2015; Chowdhary et al., 2019; Aslanyan et al.,
2016) (see (Manshaei et al., 2013) for a survey). For instance, Aslayan et al.
(Aslanyan et al., 2016) propose an approach for formal analysis of attack-
defense trees using a stochastic two-player game and probabilistic model
checking techniques. _However, most of the research achievements in this area
are based on the hypothesis that the two sides of players have full
observation of the opponent’s moves, which is unrealistic in practice._ This
is because it is not always possible to observe all the attacker’s activities:
many vulnerabilities and malicious activities cannot be detected due to, for
example, the high overhead of monitoring, expensive security controls or
ineffective security mechanisms.

To address the above challenges, we propose a stochastic game-theoretic
approach for the analysis of attack-defense scenarios under partial
observation to synthesize defense strategies automatically. We build on
stochastic modeling and verification with games (Chen et al., 2013), which
provide formal assurance about systems that operate in uncertain environments.
A (turn-based) stochastic multi-player game is a model in which each state is
controlled by one of a set of players. In each state, the controlling player
decides on the action to be performed in that state with a probability, i.e.
the probability captures the stochastic behavior and uncertainty. A strategy
is the choices made by a player to execute an action in each state controlled
by that player (based on the history). Strategy synthesis is used to generate
a strategy for the players under which the game satisfies a formally specified
property.

In this paper, we first automatically generate a logical attack graph, which
is a type of attack graph that shows different strategies that can be taken by
an attacker to reach its goal. We formalize the vulnerabilities
specifications, network scanning results and system configurations
automatically using Horn clauses and use MulVAL (Multihost, multistage
Vulnerability Analysis) (Ou et al., 2005) to generate an attack graph. We then
define the semantics of attack graphs in terms of Symbolic Markov Decision
Processes. A defense is specified using a set of rules, triggered as a
reaction to an attack, or a preventive action to stop potential future
attacks. A _fully observable_ (also called _perfect_) stochastic two-player
boolean game is constructed from the semantics of the attacker and the
defender’s behavior. A perfect game is a game where each of the players has
full observation of the other players’ actions. We specify the properties to
be checked using the temporal logic rPATL (Probabilistic ATL with Rewards)
(Chen et al., 2013) and employ the verification and strategy synthesis
techniques for this logic provided by the PRISM-games tool (Kwiatkowska et
al., 2017) to analyze a network and synthesize defense strategies. Our
approach is summarized in Fig. 1.

Figure 1. Our Overall Approach for Automated Attack Analysis and Defense
Synthesis

To support reasoning under partial observation, we define a partially
observable one-sided security game (PO-security game) that provides partial
observation of the attacker’s behavior. We assume, on the other hand, that the
attacker has full observation of the defender’s actions. This type of game,
where one player has full observation and the other player has partial
observation, is called a _one-sided partially observable game_ (Chatterjee et
al., 2013b). Observe that, if the defender wins in this setting where the game
is one-sided, then it will also win in a setting where the attacker has only
partial observation (Chatterjee and Doyen, 2014).

While the formal verification community has studied analysis under partial
observation and presented (theoretical) results, e.g. (Chatterjee et al.,
2013a; Chatterjee and Doyen, 2014; Cassez et al., 2007; Behrmann et al.,
2007), progress on developing practical methods on stochastic games under
partial observation has been very limited. We are not aware of any practical
method or tool for analyzing partially observable games. To be able to analyze
a PO-security game, we transform it into a perfect game and use PRISM-games to
analyze the perfect security game. We prove that this transformation is sound
for a subclass of security games called ODT (Observable Defense Triggers)
security games and a subset of rPATL properties (called observable step-
unbounded defense objectives), in the sense that a synthesized strategy for
the defender in the resulting perfect security game is a valid strategy for
the defender in the original PO-security game. We implement a prototype to
support and automate the proposed approach and evaluate our approach by
applying it to a real-life case study. Our experimental results show that the
transformation of a PO-security game improves the performance of our analysis
significantly and can also be used as a promising state space reduction
technique to handle large attack graphs.

The contributions of this paper are: (i) automatically constructing a boolean
security game model from an attack graph; (ii) introducing partially
observable security games and an approach for their efficient analysis; (iii)
automating our approach and applying it to a real-life case study.

The paper is organized as follows. Section 2 presents preliminaries on
stochastic games. Formalization of attacks graphs is explained in Section 3.
Section 4 constructs a fully observable security game and Section 5 discusses
PO-security games. Section 6 introduces the soundness theorems of the
approach. We present the evaluation in Section 7, discuss related work in
Section 8 and conclude in Section 9.

##  2\. Preliminaries

In this section, we briefly review probabilistic model checking and strategy
synthesis for stochastic games, proposed in (Chen et al., 2013; Simaitis,
2014). We also cover the simpler model of Markov Decision Processes, needed
for our modeling approach.

###  2.1. Markov Decision Process

Let $\mathbb{P}_{X}$ be the set of all discrete probability distribution
functions over the set $X$, ${V}=\langle{v}_{1},\ldots,{v}_{n}\rangle$ be a
vector of variables, $\mathcal{D}_{{v}_{i}}$ be the domain of a variable
${v}_{i}$, and $\mathcal{D}_{{V}}=\prod_{i=1}^{n}\mathcal{D}_{{v}_{i}}$. A
_valuation_ $\vec{\nu}$ of ${V}$ is a tuple
$\langle\vec{\nu}_{1},\ldots,\vec{\nu}_{n}\rangle\in\mathcal{D}_{V}$, and we
denote the value of ${v}_{i}$ in $\vec{\nu}$ by $\vec{\nu}({v}_{i})$, $1\leq
i\leq n$.

###### Definition 0 (Symbolic Markov Decision Process).

A _Symbolic Markov Decision Process_ (SMDP) is a tuple
${\mathrm{M}}=\langle{V},\vec{\nu}_{0},\Sigma,\delta\rangle$ where
${V}=\langle{v}_{1},\dots,{v}_{n}\rangle$ is a tuple of variables,
$\vec{\nu}_{0}\in\mathcal{D}_{{V}}$ gives the initial conditions on the
variables, $\Sigma$ is a finite non-empty set of actions, and $\delta$ is a
finite set of probabilistic transitions
$\langle\phi,\sigma,\mathcal{P}_{U}\rangle$ where
$\phi\,{\subseteq}\,\mathcal{D}_{{V}}$ is a predicate on ${V}$ which guards
the transition, $\sigma{\in}\Sigma$ is the transition action,
$\mathcal{P}_{U}{\in}\mathbb{P}_{U}$ is a discrete probability distribution
function over the set $U$ and $U$ is a set of update functions of the form
$u:\mathcal{D}_{V}\mapsto\mathcal{D}_{{V}}$ defined as a set of assignments.

Initially, ${\mathrm{M}}$ is in its initial state. A transition is fired if
its guard is satisfied and, when fired, the variables are updated with the
probabilities corresponding to its update functions. The semantics of a SMDP
is defined in terms of a Markov Decision Process (MDP):

###### Definition 0 (Markov Decision Process).

Let ${\mathrm{M}}=\langle{V},\vec{\nu}_{0},\Sigma,\delta\rangle$ be a SMDP.
The semantics of ${\mathrm{M}}$ is an MDP ${\overline{{\mathrm{M}}}}=\langle
V,S,s_{0},\Sigma,\overline{\delta}\rangle$ where $S\subseteq\mathcal{D}_{V}$
is a set of states, $s_{0}=\vec{\nu}_{0}$ is the initial state and
$\overline{\delta}:S\times\Sigma\to\mathbb{P}_{S}$ is a (partial) transition
function defined as follows:

$\begin{array}[]{lll}\overline{\delta}=\\{\langle\langle
s,\sigma\rangle,f(U,s)\rangle~{}|~{}\exists\delta=\langle\phi,\sigma,\mathcal{P}_{U}\rangle\in\delta,s\models\phi\\}\\\
f(U,s)=\begin{cases}\langle t,p\rangle&u\in U,t=u(s),p=\mathcal{P}_{U}(u)\\\
\textnormal{undef}&\textnormal{otherwise}\\\ \end{cases}\end{array}$

###  2.2. Stochastic Games

###### Definition 0 (Two-Player Stochastic Game).

Let
${\overline{{\mathrm{M}}_{1}}}=\langle{V}_{1},S_{1},s_{1,0},\Sigma_{1},\overline{\delta}_{1}\rangle$
and
${\overline{{\mathrm{M}}_{2}}}=\langle{V}_{2},S_{2},s_{2,0},\Sigma_{2},\overline{\delta}_{2}\rangle$
be two MDPs specifying two players’ behavior. A (turn-based) stochastic two-
player game is a tuple $\mathcal{G}=\langle
P,V,S,s_{0},\Sigma,\mathsf{sch},\Delta\rangle$ where $P=\\{1,2\\}$ is the set
of players, $V$ is a vector of state variables over $V_{1}\cup
V_{2}\cup\\{t\\}$, $S\subseteq\mathcal{D}_{{V}}$ is the set of states, $s_{0}$
is the initial state, $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ is the set of actions,
$\mathsf{sch}:S\to P$ is a scheduler and
$\Delta=\\{\langle\langle\vec{\nu},\sigma\rangle,\mathcal{P}_{S}\rangle\\}$ is
a (partial) transition function defined in the below.

Let $\vec{\nu}_{\downarrow_{{V}_{i}}}$ be the projection of $\vec{\nu}$ on the
variables in ${V}_{i}$, $\vec{\nu}\uparrow_{V_{i}}x$ be the updated
$\vec{\nu}$ with $V_{i}$ to $x$, and
$\overline{\delta}{}(x,\sigma)(x^{\prime})$ (similarly for
$\Delta{}(x,\sigma)(x^{\prime})$) represent the probability of a transition
from the state $x$ to the state $x^{\prime}$ with the action $\sigma$. The
probability of a transition from $\mathcal{P}_{S}$ from the state $\vec{\nu}$
with the active player $i$ to a state $\vec{\nu}^{\prime}$ by performing the
action $\sigma$ is:

$\begin{array}[]{lll}&\mathcal{P}_{S}(\vec{\nu}^{\prime})=\begin{cases}p&\vec{\nu}_{\downarrow_{\\{t\\}}}=i~{}~{}\wedge\phi\\\
0&\textnormal{otherwise}\end{cases}\end{array}$

where $~{}\phi=\exists
x.~{}\overline{\delta}_{i}{}(\vec{\nu}_{\downarrow_{V_{i}}},\sigma)(x)=p~{}\wedge\vec{\nu}^{\prime}=\vec{\nu}\uparrow_{V_{i}}x\uparrow_{\\{t\\}}\mathsf{sch}(\vec{\nu}).$

The transition relation in Definition 3 informally states that a state with
active player $i$ is updated to a new state $\vec{\nu}^{\prime}$ in which the
active player’s state $\vec{\nu}_{\downarrow_{V_{i}}}$ is updated to $x$ with
probability $p$, the other player’s local substate remains unmodified and the
active player is updated according to the scheduler function. We represent the
game by ${\overline{{\mathrm{M}}_{1}}}~{}||~{}{\overline{{\mathrm{M}}_{2}}}$
and partition the game’s states into sets $S_{1}$ and $S_{2}$, controlled by
each of the two players. Furthermore, $\Sigma(s)$ denotes the actions that can
be performed in state $s\in S$. We also annotate games with _reward
structures_ $\xi:\Sigma\rightarrow\mathbb{R}_{\geq 0}$, which can be used to
model rewards or costs.

###  2.3. Strategy Synthesis and Model Checking

Given an objective $\psi$ and a game $\mathcal{G}$, the goal of strategy
synthesis is to synthesize strategies for (coalitions of) players to be able
to win the game. A strategy informally determines the optimal action that
should be performed by the coalition in each state to achieve its objective.
The objective $\psi$ is specified using the temporal logic rPATL
(probabilistic alternating-time temporal logic with rewards). This logic
allows us to express quantitative properties of the games, e.g., to ensure
that the probability of an event occurrence meets some thresholds (for
example: “can the defender protect the network in a way that the probability
of the system being compromised by the attacker is less than 0.1?”). rPATL is
a branching-time logic and contains state formulas $\phi$ and path formulas
$\psi$. The syntax is given by the following grammar:

$\displaystyle\phi$ $\displaystyle::=$
$\displaystyle\top~{}|~{}\alpha~{}|~{}\neg\phi~{}|~{}\phi\wedge\phi~{}|~{}\langle\\!\langle{C}\rangle\\!\rangle\mathsf{P}_{\bowtie~{}\\!\\!p}[\psi]~{}|~{}\langle\\!\langle{C}\rangle\\!\rangle\mathsf{R}^{r}_{\bowtie~{}\\!\\!x}[\mathsf{F}\phi]$
$\displaystyle\psi$ $\displaystyle::=$
$\displaystyle\mathsf{X}\,\phi~{}|~{}\phi_{1}\mathsf{U}^{\leq
k}\phi_{2}~{}|~{}\phi_{1}\mathsf{U}\phi_{2}$

where $\alpha$ is a proposition, $C$ is a coalition of players,
$\bowtie\,\in\\{<,\leq,>,\geq\\}$, $p\in[0,1]$, $x\in\mathbb{R}$,
$k\in\mathbb{N}$ and $r$ is a reward structure. The operators $\mathsf{X}$
(”next”), $\mathsf{U}^{\leq k}$ (”bounded until”), $\mathsf{U}$ (”until”) and
$\mathsf{F}$ (”eventually”) are the standard temporal operators. Informally,
$\langle\\!\langle{C}\rangle\\!\rangle\mathsf{P}_{\bowtie p}[\psi]$ states
that the coalition $C$ has a strategy to ensure that the path formula $\psi$
will be satisfied with a probability meeting the bound $\bowtie p$, regardless
of the strategies of other players. Similarly,
$\langle\\!\langle{C}\rangle\\!\rangle\mathsf{R}_{\bowtie x}[\mathsf{F}\phi]$
means that $C$ has a strategy guaranteeing that the expected reward $r$
accumulated until $\phi$ satisfies $\bowtie x$.

We write $s\models\phi$ to indicate that the state $s$ of $\mathcal{G}$ with
the reward structure $r$ satisfies the formula $\phi$, and write
$\mathcal{G}\models\phi$, if $s_{0}\models\phi$. Further,
$\mathsf{Sat}(\phi)=\\{s\in S~{}|~{}s\models\phi\\}$ defines the set of states
satisfying $\phi$. The semantics of rPATL is defined over games (See Appendix
A) and it is supported by the probabilistic model checking and strategy
synthesis tool PRISM-games (Kwiatkowska et al., 2017). The goal of strategy
synthesis is to synthesize an optimal strategy for a coalition of players to
ensure satisfaction of an objective, regardless of the opponent’s strategy.

##  3\.  Formalized Attack Graphs

Attack Model. We use Horn clauses to specify attack models, as done in (Ou et
al., 2005). We represent a predicate by $\phi(t_{0},\ldots,t_{n})$ where a
term $t_{i}$, $0\leq i\leq n$ is either a constant or a variable. A rule $r$
defined on predicates is of the form

$\phi_{0}(t_{0,0},\ldots,t_{0,m_{0}}),\ldots,\phi_{k}(t_{k,0},\ldots,t_{k,m_{k}})\vdash\psi(t^{\prime}_{0},\ldots,t^{\prime}_{n})$

that informally states, if for all $0\leq j\leq k$, the predicate $\phi_{j}$
holds, then $\psi$ will hold. The left hand side of this rule is called the
_body_ and $\psi$ is called the _head_. A rule is safe if and only if the
variables occurring in the head also appear in the body. A predicate is
_primitive_ if it does not appear in the head of any rule with a non-empty
body. Otherwise, it is called a _derived_ predicate. A safe rule with an empty
body represents a primitive proposition.

An attack model specifies the system configurations, vulnerabilities and
attack actions that lead to exploitation of vulnerabilities. We define an
attack model by a triple
$spec=\langle{\mathcal{C}},{\mathcal{H}},{\mathcal{R}}\rangle$, consisting of
(i) the _primitive capabilities_ ${\mathcal{C}}$ that is a set of primitive
predicates, (ii) the _derived capabilities_ ${\mathcal{H}}$ that is a set of
derived predicates and ${\mathcal{H}}\cap{\mathcal{C}}=\emptyset$, and (iii) a
set of action rules ${\mathcal{R}}$ specified in terms of safe rules.

###### Example 0.

The following rule expresses illegal access to a file by exploiting the
vulnerability
CVE-2018-1000028111https://nvd.nist.gov/vuln/detail/CVE-2018-1000028,

$\begin{array}[]{l}\mathsf{accessService(host,fs,ptcl,port)},\\\
\mathsf{nfsExportInfo(fs,dir,ar,host)},\\\ \mathsf{execCode(host,service)},\\\
\mathsf{nfsConfiguration(fs,dir,"rootsquash")},\\\
\mathsf{vulExists(fs,\texttt{'CVE-2018-1000028'},mountd)}\vdash\mathsf{illegalAccessToFile(fs,write,ex)}.\end{array}$

where constants and variables respectively start with a capital and a small
letter. This action (a Horn clause) states that if (i) a machine
$\mathsf{host}$ has access to a service provided by a file server
$\mathsf{fs}$ with the protocol $\mathsf{ptcl}$ on the port $\mathsf{port}$,
(the primitive predicate
$\footnotesize\mathsf{accessService(host,fs,ptcl,port)}\in{\mathcal{C}}$),
(ii) the file server $\mathsf{fs}$ exports $\mathsf{dir}$ with the access
right $\mathsf{ar}$ to the machine $\mathsf{host}$ with the option
$\mathsf{rootsqush}$ (the predicates $\mathsf{nfsConfiguration}$ and
$\mathsf{nfsExportInfo}$), and (iii) the file server has the vulnerability
CVE-2018-1000028 (the predicate $\mathsf{vulExists}$), then the attacker can
gain a write access to the file system on the file server (the predicate
$\mathsf{illegalAccessToFile}$.).

Attack Graph. An attack goal can vary from compromising a specific machine by
the attacker to taking the whole network down. Given an attack model and a
specific attack goal expressed as a derived predicate, we generate a graph,
called an attack graph using MulVAL (Ou et al., 2005), that is a reasoning
system for modeling and reasoning about the interaction of software bugs with
system and network configurations (see Fig. 1).

An attack graph shows various strategies that can be taken by an attacker to
reach its goal. An attack graph consists of three types of nodes: (a)
_condition nodes_ , shown by rectangles, that correspond to primitive
capabilities, (b) _derived nodes_ represented by diamonds and are associated
with derived capabilities, and (c) _ellipse nodes_ associated to applying
rules in the attack model, i.e., a rule node connects a set of condition
and/or derived nodes (the rule’s body) to a derived node (the rule’s head).
Fig. 2 shows an attack graph where the table presents the labels of derived
and condition nodes as predicates. When the prerequisites of a rule in the
attack graph are satisfied, it is activated and leads to holding its
consequence with a probability. The label of a node is of the form
$(\mathsf{id},\phi,p)$ where $\mathsf{id}$ is the node identifier and $p$ is
the probability of reaching that node. If the node is a condition or a derived
node, $\phi$ is a proposition, otherwise, it shows the rule name. For
readability, we show the labels of the derived and fact nodes in the table.

We rely on the method proposed in (Wang et al., 2008) to calculate the
probability of applying an action rule. This method introduces AGP that is a
metric to express the probability that a specific node in the attack graph is
reached during an attack. It first associates a score to fact nodes (usually
1.0) and rule nodes that represents the likelihood of an attacker exploiting
the exploit, given that all prerequisite conditions are satisfied. We use the
scores provided by Common Vulnerability Scoring System
(CVSS222https://www.first.org/cvss/) to initialize the scores. CVSS is a
vulnerability database that provides different scores to measure the severity
of vulnerabilities. This approach, also provides cumulative scores (i.e., AGP)
that corresponds to the likelihood of an attacker reaching an exploit or
condition in the attack graph from an entry point, i.e., it considers the
causality among attack steps.

###### Definition 0 (Attack Graph).

Let $\beta$ be an attack goal,
$\mathrm{specA}=\langle{\mathcal{C}},{\mathcal{H}},{\mathcal{R}}\rangle$ be an
attack model, $\bar{{\mathcal{C}}}\subseteq{\mathcal{R}}$ show the set of
instantiated primitive capabilities (i.e., a set of propositions),
$\bar{{\mathcal{H}}}\subseteq{\mathcal{R}}$ be the set of instantiated derived
capabilities in ${\mathcal{R}}$, and $\bar{{\mathcal{R}}}$ be the set of
instantiated rules. An attack graph is formally defined as a connected graph
${G=\langle N,E\rangle}$ where
$N=\bar{{\mathcal{C}}}\cup\bar{{\mathcal{H}}}\cup\bar{{{\mathcal{R}}}}$,
$E\subseteq((\bar{{\mathcal{C}}}\cup\bar{{\mathcal{H}}})\times\bar{{{\mathcal{R}}}})\cup(\bar{{{\mathcal{R}}}}\times\bar{{\mathcal{H}}})$,
and for all $r\in\bar{{{\mathcal{R}}}}$, $|\mathsf{succ}(r)|=1$, and there is
a rule $r^{\prime}\in{\mathcal{R}}$ and a substitution $X$, such that
$\mathsf{body}(r^{\prime}[X])=\underset{\phi_{i}\in\mathsf{pred}(r)}{\bigwedge}{\phi_{i}}$
and $\mathsf{head}(r^{\prime}[X])=\mathsf{succ}(r)$ where $r{[X]}$
instantiates the variables of $r$ according to $X$, the function
$\mathsf{pred}(a)$ gives the predecessors of a node (i.e.,
$\\{\mathsf{snd}(x)|~{}(x,a)\in E\\}$ and $\mathsf{snd(x)}$ returns the second
element of the tuple $x$), and $\mathsf{succ}(a)$ returns the successors of a
node (i.e., $\\{\mathsf{snd}(x)~{}|~{}(a,x)\in E\\}$).

Figure 2. An Attack Graph

##  4\. Fully-Observable Security Games

We construct a perfect (fully observable) two-player stochastic security game
between the attacker and the defender, where the attacker goal is to gain a
specific capability and the defender tries to prevent the attacker from
achieving that capability. In such a turn-based stochastic game, one player
independently chooses an action in every round and a player’s action is fully
observable by the opponent, i.e., the attacker and the defender have perfect
observation of each other’s moves.

Security Game Assumptions. We make the following assumptions in our security
games:

  * •

The security game consists of one attacker and a single defender, i.e., the
attackers attacking the network in a collaborative way are considered as a
single attacker.

  * •

The attacker’s goal is to obtain as many capabilities as possible, and the
defender’s goal is to prevent the attacker from acquiring more capabilities,
and to revoke the attacker’s capabilities. The defender does not attack the
attacker.

  * •

If an attacker obtains a capability, it will hold it until it gets revoked by
the opponent, e.g., if the attacker gains a root privilege on a host, then it
will keep that capability until this right is revoked by the defender.

  * •

An attacker tries an action if it can result in gaining new capabilities,
e.g., if the attacker obtains access to a service provided by a specific host
through exploiting a sequence of vulnerabilities, then they will not try to
perform the same sequence of exploitations again, as it will lead to acquiring
no new capability.

  * •

The defender has the ability to check and observe the consequences of
(observable) attacks immediately, i.e., we rely on intrusion exploitation
systems and intrusion detection systems to detect and report (some of) the
attacks immediately.

Attacker Behavior. The attacker usually tries various strategies
simultaneously, and if a strategy fails or is defended by the opponent, then
she will try a new strategy. For instance, in the attack graph shown in Fig.
2, the attacker may first try to directly access the http service on the
machine $\mathsf{plycent03}$ to reach this machine (i.e., the path via the
rule node 11). However, if the defender blocks the http service (i.e., by
disallowing the node 12 and blocking the path via the rule node 11), then the
attacker may try another strategy by tampering the code memory of the host
$\mathsf{plycent02}$ and access $\mathsf{plycent03}$ via $\mathsf{plycent02}$
(the attack path via the nodes 8 and 5).

To be able to model the changing strategies of the attacker in the semantics,
we denote the state of an attacker by the set of its current achieved
capabilities. Given an attack graph, we construct a SDMP using Definition 1
(i.e., AttackGraph_SDMP Transformer module in Fig. 1).

###### Definition 0 (Attacker Behavior).

Let
$G=\langle\bar{{\mathcal{C}}}\cup\bar{{\mathcal{H}}}\cup\bar{{{\mathcal{R}}}},E\rangle$
be an attack graph produced from the attack model
$\mathrm{specA}=\langle{\mathcal{C}},{\mathcal{H}},{\mathcal{R}}\rangle$. Let
${p:{\mathcal{R}}\to[0,1]}$ be a function that denotes the probability of
successfully applying a rule $r\in{\mathcal{R}}$. The semantics of $G$ is
defined as the SDMP
$\mathrm{AT}=\langle{V}_{A},\vec{\nu}_{A,0},\bar{{{\mathcal{R}}}},\Delta_{A}\rangle$
where ${V}_{A}$ is a vector of boolean variables defined on
${\bar{{\mathcal{H}}}}\cup{\bar{{\mathcal{C}}}}$,
$\vec{\nu}_{A,0}=\underset{\phi\in\bar{{\mathcal{C}}}}{\bigwedge}\phi\wedge\underset{\phi\in{\bar{{\mathcal{H}}}}}{\bigwedge}\neg\phi$
shows the initial conditions on the variables, and for each rule
$r\in\bar{{{\mathcal{R}}}}$ , a transition $\langle\neg
e\wedge\underset{\phi_{i}\in\mathsf{pred}(r)}{\bigwedge}\phi_{i},r,\mathcal{P}_{U}\rangle\in\Delta_{A}$
is defined where $e$ corresponds to the r’s successor, and

$\begin{array}[]{l}U=\\{\emptyset,u\\}~{},~{}u=\\{e\mapsto\top\\}~{},{}\\\
\mathcal{P}_{U}(u)=p(r)~{},~{}\mathcal{P}_{U}(\emptyset)=1-p(r).\end{array}$

A state variable of an attacker is a boolean variable corresponding to either
an instantiated primitive or an instantiated derived capability and indicates
whether the attacker holds that capability or not. Initially the attacker only
holds the primitive capabilities in $\bar{{\mathcal{C}}}$ and has no derived
capability from $\bar{{\mathcal{H}}}$. A transition corresponds to performing
an action by the attacker by applying a rule $r$, and when it is triggered
(i.e., the rule prerequisites hold and its consequence $e$ does not hold), the
attacker’s gains the new capability $e$ with the probability $p(r)$.

###### Example 0.

The attacker’s behavior in Fig. 2 contains four rule nodes, each is translated
to a symbolic transition. For instance, the rule node 2 is translated to the
transition $\langle\phi,{\mathsf{remote\\_DOS}},\mathcal{P}_{U}\rangle$ where

$\phi={\begin{array}[]{l}{\mathsf{misuseAction\\_overusecpu}}\wedge{\mathsf{netAccess\\_plycent03\\_tcp\\_22}}\wedge\\\
{\mathsf{networkServiceInfo\\_plycent03\\_\\_centos7\\_5}}\wedge\\\
{\mathsf{vulExists\\_plycent03\\_cve\\_2018\\_5390\\_cen}}\wedge\\\
\neg{\mathsf{systemDown\\_plycent03}}\\\ \end{array}}$

$\hskip
7.22743pt\small\mathcal{P}_{U}(\\{{\mathsf{systemDown\\_plycent03}}\mapsto\top\\})=0.74\hskip
36.135ptand\hskip 36.135pt\mathcal{P}_{U}(\emptyset)=0.26.$

Defender Behavior. The choices of each player strictly depend on the moves of
the other, i.e., their capabilities and rights may change as a consequence of
the opponent’s moves. For instance, if an attacker gains full control over a
host as a consequence of a ransomware attack, the defender will have no access
to that host anymore. Similarly, if the defender changes the firewall
configurations to disallow a service access on the victim, the attacker may
change its strategy to attack the victim. Hence, the decision of an attacker
to choose a possible attack to an asset should consider the potential
countermeasures of the defender to defend it, and vice versa. The
countermeasure chosen by the defender to be applied should consider the
attacks performed by the attacker and the potential countermeasures that can
be applied in future.

We define two types of defense: _reactive defense_ and _proactive defense_.
Reactive defenses are usually performed as a reaction to an attack while a
proactive defense is a preventive action performed to prevent future malicious
activities. An example of a reactive defense is updating the firewall rules to
deny the attacker’s access to a service, when a malicious activity is detected
by an intrusion detection system. Performing regular vulnerability scans in
some critical nodes to detect and fix potential weaknesses, proactively
patching applications and monitoring critical security controls are considered
as some examples of proactive defenses.

The defenses performed by the defender are defined as a reaction to gaining
new capabilities by the attacker, to either revoke them or prevent the
attacker from achieving specific capabilities in future.

###### Definition 0 (Defender Behavior).

Let $\mathrm{AT}=\langle{V}_{A},\vec{\nu}_{A,0},\Sigma_{A},\Delta_{A}\rangle$
be the behavior of an attacker, and ${V}_{AD}\subseteq{V}_{A}$ be the set of
defense-triggering capabilities of the attacker. The behavior of the defender
is defined as
$\mathrm{DE}=\langle{V}_{D},\vec{\nu}_{D,0},\Sigma_{D},\Delta_{D}\rangle$
where ${V}_{AD}\subseteq{V}_{D}$, ${\vec{\nu}_{D,0}}$ implies
$\vec{\nu}_{A,0}$, and $\Sigma_{D}\cap\Sigma_{A}=\emptyset$.

The defender’s state variables includes the defense-triggering state variables
of the attacker in addition to some extra internal variables. A defense-
triggering variable is a rule consequence that can lead to a reaction by the
defender. The actions of the attacker and the defender are disjoint.

###### Example 0.

A reactive defense to the capability of executing a code with the root
privilege by the attacker on the machine $\mathsf{plycent02}$ is to patch the
vulnerability $\mathsf{cve}$-$\mathsf{2018}$-$\mathsf{7566}$ (the rule node 8
in Fig. 2). This defense is specified as a transition
$\langle\phi,{\mathsf{patch\\_vul\\_2018\\_7566}},\mathcal{P}_{U}\rangle$
where,

${\begin{array}[]{l}\phi={\mathsf{exeCode\\_plycent02\\_root}}\wedge{\mathsf{vulExists\\_plycent02\\_vul\\_2018\\_7566}}\\\
u=\\{{\mathsf{exeCode\\_plycent02\\_root}}\mapsto\bot;\\\
\quad\quad\quad{\mathsf{vulExists\\_plycent02\\_vul\\_2018\\_7566}}\mapsto\bot\\}\end{array}}$

$\mathcal{P}_{U}(u)=0.85\hskip 36.135ptand\hskip
36.135pt\mathcal{P}_{U}(\emptyset)=0.15.$

Security Game. Given the behavior of the attacker and the defender specified
in terms of SDMP and a scheduler $\mathsf{sch}$, we construct a security game
$\mathcal{G}=\langle\\{A,D\\},V,S_{A}\cup
S_{D},s_{0},\Sigma_{D}\cup\Sigma_{A},\mathsf{sch},\Delta\rangle$ according to
Definition 3 where $\\{A,D\\}$ is the set of players, $S_{A}$ is the set of
states controlled by the attacker and $S_{D}$ is the set of states controlled
by the defender (the _Game_ module in Fig. 1). This security game is
deterministic, i.e., for each action $\sigma\in\Sigma$, there is at most one
probabilistic transition from each state. The security game can be associated
with reward structures associating rewards or costs to the states or
transitions.

We use the probabilistic model checker PRISM-games to verify various classes
of properties for a single player or for both players, e.g., the likelihood or
the costs of achieving a specific capability or goal by the attacker. The
ultimate goal is to keep the attacker away from its targets where a target can
be an intermediate target or a final one, e.g., controlling a specific host
and using it as a platform to access the sensitive information on another
victim. PRISM-games can also synthesize a strategy $\Gamma:S\to\Sigma$ that
identifies an optimal action to be performed in a state by the player
controlling that state. We use strategy synthesis to construct defense
strategies for protecting the system from attacks.

##  5\. One-Sided Partially-Observable Security Games

In a perfect stochastic game, in every round, one player independently chooses
an action which is fully observable by the opponent, i.e., the player has a
full knowledge of the opponent’s capabilities. Most security games also make
the hypothesis of perfect observation (Durkota et al., 2015; Chowdhary et al.,
2019), i.e., the players have full observation of the game state and the
opponent’s actions, while this is not a realistic assumption in practice. For
instance, the attacker can carry out various attacks in a multi-stage attack
to reach its final goal, from a social engineering attack to comprising a host
to use as a platform to launch the final attack. However, not all the
attacker’s steps are observable by the defender, nor all attacks are trivially
detectable, i.e., detecting some of the malicious activities and
differentiating them from normal operations can be very hard or expensive.

We assume that the attacker has full observation while the defender has
partial observation. This type of games, where one player has full observation
and the other player has partial observation, is called _one-sided partially
observable game_ (Chatterjee et al., 2013b). Observe that if the defender wins
in this settings where the game is one-sided, then it will win in a setting
where the attacker has partial observation (Chatterjee and Doyen, 2014).
Analogously, if the attacker cannot win in this setting, it cannot win in a
setting where the defender has full observation. We define a partially
observable stochastic two-player security game as follows:

###### Definition 0 (One-Sided Partially-Observable Security Game).

Let $P=\\{A,D\\}$, $i\in P$ and
${\mathrm{M}}_{i}=\langle{V}_{i},\vec{\nu}_{i,0},\Sigma_{i},\delta_{i}\rangle$
be two SMDPs representing the behavior of the attacker and the defender. A
(turn-based) stochastic two-player PO security game is a tuple
$\mathcal{G}=\langle
P,{V},S,{\mathsf{Obs}},s_{0},\Sigma,\mathsf{sch},\Delta{}\rangle$ where ${V}$
is a vector defined over ${V}_{A}\cup{V}_{D}\cup\\{t\\}$,
$S\subseteq\mathcal{D}_{{V}}$ is the set of states and
${\mathsf{Obs}}:\mathcal{D}_{{V}}\to\mathcal{D}_{{V}_{D}}$ is a function that
defines the observation of the defender in a state. The initial state is
$s_{0}$ such that $s_{0}\models\vec{\nu}_{A,0}$ and
${\mathsf{Obs}}(s_{0})\models\vec{\nu}_{D,0}$,
$\Sigma=\Sigma_{A}\cup\Sigma_{D}$ and $\mathsf{sch}:S\to P$ is the scheduler.
The transition $\Delta{}:S\times\Sigma\to\mathbb{P}_{U}$ is a (partial)
transition function defined as follows, where $\mathsf{up(u,\sigma)}$ is an
update function:

$\begin{array}[]{lll}\Delta=\\{\langle\langle
s,\sigma\rangle,f(U,s,\sigma)\rangle~{}|~{}\exists\delta=\langle\phi,\sigma,\mathcal{P}_{U}\rangle\in\delta_{A}~{}\wedge~{}s\models\phi\vee\\\
\hskip
72.26999pt~{}\exists\delta=\langle\phi,\sigma,\mathcal{P}_{U}\rangle\in\delta_{D}~{}\wedge~{}{\mathsf{Obs}}(s)\models\phi\\}\\\
f(U,s,\sigma)=\begin{cases}\langle{\mathsf{up}(u,\sigma)(s)},p\rangle&u\in
U,p=\mathcal{P}_{U}(u)\\\ \textnormal{undef}&\textnormal{otherwise}\\\
\end{cases}\end{array}$

To handle the problem of partial observation in security games, we partition
the actions of the attacker into two sets of _observable_ and _unobservable_
actions and the defender can only observe the observable actions of the
attacker and their consequences. An action of the attacker is applying an
action rule to obtain a new derived capability; if the action is observable,
the defender can also observe the newly obtained capability. For instance, the
network traffic can be easily monitored to find direct network accesses
between hosts (See Fig. 2), while it’s impossible to detect a DoS attack if
the host is not equipped with a powerful IDS. Therefore, we define the game
state as $V=\langle v_{A,0},\ldots,v_{A,n},v_{D,0},\ldots,v_{D,m},t\rangle$ in
this paper where ${V}_{A}=\langle v_{A,0},\ldots,v_{A,n}\rangle$ is the
attacker’s state, ${V}_{D}=\langle v_{D,0},\ldots,v_{D,m}\rangle$ is the
defender’s state and $t$ represents the active player. The defender’s
observation in a game state $\vec{\nu}$ is defined as:

(1)
${\mathsf{Obs}}(\vec{\nu})=\langle\vec{\nu}(v_{D,0}),\ldots,\vec{\nu}(v_{D,m}),t\rangle.$

Note that ${V}_{AD}$ is duplicated in ${V}$. Let $\overrightarrow{u}$ be a
function that applies the updates of the variables in ${V}_{AD}$ by $u$ to the
sub-states of both players. The function $\mathsf{up}(u,\sigma)$ applies the
update of an unobservable action locally only to the attacker’s sub-state.
Otherwise, the updates should be applied to the both players’ sub-states:

(2)
$\displaystyle\mathsf{up}(u,\sigma)=\begin{cases}u&\sigma\notin\Sigma_{O}\cup\Sigma_{D}\\\
\overrightarrow{u}&\textnormal{otherwise}\\\ \end{cases}$

Analyzing a Partially Observable Security Game. To analyze a PO security game,
we transform it to a perfect security game and analyze the perfect game
instead. As mentioned above, if a derived capability is obtained due to
performing an observable action, it becomes also observable to the defender,
otherwise, the update cannot be observed by the defender. If the defender
knows the possible consequences of his observation, he can guess the next
observable actions by the attacker. To this end, we need to obtain the sets of
observable prerequisites of an observable action $\sigma$, that can lead to
performing $\sigma$ via applying a sequence of unobservable actions, and
consequently, achieving an observable derived capability by the attacker. For
instance, assume that the defender cannot detect a memory tampering attack by
the attacker, i.e., the rule node 8 in Fig. 2 becomes unobservable. This means
that it will not be possible to detect whether the attacker can run a code
with the root privilege on plycent02 or not (node 7). However, the defender
knows that if the attacker holds the observable capabilities of the nodes 9,
10 and 6, then it can finally perform the action in node 5, i.e., the
observable prerequisites of the rule 5 will become $\\{6,9,10\\}$.

There might be several sets of observable prerequisites that can result in
performing an observable action. For example, let’s assume that a multi-hop
access by the attacker be unobservable, i.e., the action rule node 5 in Fig. 2
becomes unobservable. The observable prerequisites of the action rule node 2
will be two distinct sets of observable capabilities of $\\{14,15,4,3\\}$ and
$\\{14,15,6,7,3\\}$. The node 4 can be achieved either via applying the
observable rule 11 (i.e., that requires $\\{12,13\\}$) or via the unobservable
rule 5 (i.e., that requires $\\{6,7\\}$). Since, the node 11 is observable,
then the node 4 will become observable too via the path through the node 11;
while the same node cannot observed, if the attacker takes the path via the
unobservable node 5.

Algorithm 1 returns the _distinct sets of observable prerequisites_ (DOP) of a
action rule node $r$, where
$G=\langle\bar{{\mathcal{C}}}\cup\bar{{\mathcal{H}}}\cup\bar{{{\mathcal{R}}}},E\rangle$
is an attack graph and, $\Sigma_{O}\subseteq\bar{{{\mathcal{R}}}}$ is the set
of observable actions. To obtain the DOP of $r$, it first obtains the DOP of
all its prerequisites. If a perquisite is a basic capability, then its DOP
contains only itself. If it’s a derived capability $n$, its DOP will be the
union of the DOPs of all possible rules $r^{\prime}$ that lead to it
immediately (i.e., their consequence is $n$). If $r^{\prime}$ is observable
then $\\{n\\}$ is its only DOP, and, otherwise $r^{\prime}$’s DOP will be
obtained by invoking the algorithm in a recursive way. The final $r$’s DOP
will be a set of sets where each set contains one element of the DOP from each
of r’s prerequisite.

Input: An action rule node $r\in\bar{{{\mathcal{R}}}}$ and the visited nodes
$V$.

Output: Set of distinct observable pre-requisities leading to $r$

$\mathsf{DOPs}=\\{\\}$;

for  _all $n\in\mathsf{pred}(r)$_ do

if  _$n\in\bar{{\mathcal{C}}}$_ then

$\mathsf{DOPs}=\mathsf{DOPs}\cup\\{\\{n\\}\\}$;

end if

else

for  _all $r^{\prime}\in\mathsf{pred}(n)\backslash V$_ do

if  _$r^{\prime}\in\Sigma_{O}$_ then

$\mathsf{DOPs}=\mathsf{DOPs}\cup\\{\\{n\\}\\}$;

end if

else

$\mathsf{DOPs}=\mathsf{DOPs}\cup\\{\mathsf{doPrequisites}(r^{\prime},V\cup\\{r\\})\\}$;

end if

end for

end if

end for

/* $\mathsf{DOPs}=\\{D_{1},\ldots,D_{k}\\}$: DOPs of $r$’s prerequisites */

return $\underset{1\leq i\leq k,e_{1}\in D_{1},\ldots,e_{k}\in
D_{k}}{\bigcup}e_{i}$

Algorithm 1 $\mathsf{doPrequisites}(r,V)$

###### Definition 0 (Attacker’s Observable Behavior).

Let
$G=\langle\bar{{\mathcal{C}}}\cup\bar{{\mathcal{H}}}\cup\bar{{{\mathcal{R}}}},E\rangle$
be an attack graph produced from the attack model
$\mathrm{specA}=\langle{\mathcal{C}},{\mathcal{H}},{\mathcal{R}}\rangle$. Let
$\Sigma_{O}\subseteq\bar{{{\mathcal{R}}}}$ be a set of observable actions and
${p:{\mathcal{R}}\to[0,1]}$ be a function that returns the probability of
successfully applying a rule $r\in{\mathcal{R}}$. The observable behavior of
$G$ is defined as
$[\mathrm{AT}]=\langle{V}_{O},\vec{\nu}_{{O},0},\Sigma_{{O}},\delta_{O}\rangle$
where ${V}_{O}$ is a vector of variables defined on a subset of
${\bar{{\mathcal{C}}}}\cup{\bar{{\mathcal{H}}}}$,
$\vec{\nu}_{0}=\underset{\phi\in\bar{{\mathcal{C}}}}{\bigwedge}\phi\wedge\underset{\phi\in{\bar{{\mathcal{H}}}\cap{V}_{{O}}}}{\bigwedge}\neg\phi$
shows the initial conditions on the variables. For each rule $r\in\Sigma_{O}$
and each of its distinct set of observable prerequisites
$\mathsf{dop}\in\mathsf{doPrequisites}(r,\\{\\})$, a transition $\langle\neg
e\wedge\underset{\phi\in\mathsf{dop}}{\bigwedge}\phi,\mathsf{act(dop)},\mathcal{P}_{U}\rangle\in\delta_{O}$
is defined where $\mathsf{act(dop)}$ assigns an action label in $\Sigma_{O}$
to $\mathsf{dop}$, $e$ corresponds to $\mathsf{succ}(r)$,
$U=\\{\emptyset,u\\}$, $u=\\{e\mapsto\top\\}$, and

$\begin{array}[]{l}\mathcal{P}_{U}(u)=\underset{r_{i}\in\mathsf{dop}}{\prod}p(r_{i}),~{}\mathcal{P}_{U}(\emptyset)=1-\mathcal{P}_{U}(u).\end{array}$

Further, the reward structure for the attacker’s actions is defined as
$\xi^{\prime}(r)=\underset{r_{i}\in\mathsf{dop}}{\sum}\xi(r_{i})$.

The SMDP in the above definition hides the unobservable actions and only
considers their impact on performing observable actions. For each observable
action rule $r$, it finds its DOP, and for each element $\mathsf{dop}$ of the
ODP, adds a new transition whose guard is the conjunction of all the
observable capabilities in $\mathsf{dop}$ as well as the negation of $r$’s
consequence. The action of this transition will set the $r$’s consequence and
its probability is the product of all the action rules’ probabilities along
the path, i.e., this path can be taken if all the actions along this path can
be performed successfully.

###### Example 0.

Let all the rule nodes in Fig. 2 be unobservable, apart from the rule 2. Let
$\phi_{n}$ denote the proposition associated with the node $n$. The graph in
Fig. 2 is translated into two symbolic transitions. One of the transitions is
$\langle\phi_{14}\wedge\phi_{15}\wedge\phi_{12}\wedge\phi_{13}\wedge\phi_{3}\wedge\neg\phi_{1},\mathtt{path0},\mathcal{P}_{U}\rangle$
where $U=\\{\\{\phi_{1}\mapsto\top\\},\emptyset\\}$,
$\mathcal{P}_{U}(\\{\phi_{1}\mapsto\top\\})=0.74*0.92=0.68$ and
$\mathcal{P}_{U}(\emptyset)=0.32$. The other one is defined similarly.

We use the attacker’s behavior constructed in Definition 2 to build a fully-
observable security game and analyze it instead of directly analyzing the PO
security games constructed using the functions ${\mathsf{Obs}}$ and
$\mathsf{up}$ defined in Equation 1 and Equation 2. Let ${V}^{\prime}_{AD}$ be
the attacker’s copy of ${V}_{AD}$ (i.e., the set of common variables of the
attacker and the defender). The scheduler of the perfect game is defined as
follows where $\mathsf{sch}$ is the scheduler of the original PO security
game:

(3)
$\mathsf{sch}^{\prime}(\vec{\nu})=\mathsf{sch}(\vec{\nu}_{\downarrow_{({V}_{{O}}\backslash{V}^{\prime}_{AD})\cup{V}_{D}\cup\\{t\\}}}).$

The scheduler of a state $\vec{\nu}$ is defined as the value returned by the
original scheduler $\mathsf{sch}$ for the corresponding state of $\vec{\nu}$
in the original game, that is basically a projection on the state variables of
the attacker, the defender and the variable $t$.

##  6\. Soundness

We define an Observable Defense Triggering security game (_ODT security game_)
as the following:

###### Definition 0.

An _ODT security game_ is a PO security game in which all the defense-
triggering capabilities of the attacker are observable, i.e., $V_{AD}\subseteq
V_{O}$.

We prove that the transformation of an ODT security game, constructed using
Definition 1 and the functions ${\mathsf{Obs}}$ and $\mathsf{up}$ defined in
Equation 1 and Equation 2 to a perfect security is sound. Since some of the
attackers actions are aggregated into one action, some information about the
attacker behavior will be missing in the ODT game. For instance, the number of
steps taken by an attacker in the original game cannot be the same as that of
ODT game. Hence, it’s not always possible to reason about properties that
include the number of steps. The same goes for the operator $X$, as a next
state in the original game cannot always be mapped to a state in the ODT game.

###### Definition 0.

A formula $\phi$ is an observable step-unbounded defense objective, if (i) it
is defined over ${V}_{O}\cup{V}_{D}$ (i.e., it contains no unobservable
variable), (ii) it contains no $\mathsf{X}$ or $\mathsf{U}^{k}$ operators, and
(iii) in any sub-formula ${\ll{C}\gg}\mathsf{P}_{\bowtie~{}p}[\psi]$,
$C\subseteq\\{D\\}$.

We prove that an observable step-unbounded defense objective $\phi$ holds by
an ODT security game defined in Definition 1, if and only if it is satisfied
by a perfect game with the attacker behavior obtained using Definition 2.

###### Theorem 3.

Let $\mathcal{G}$ be a one-sided partially observable security game and
$[\mathcal{G}]$ be its transformation to a perfect game. For any observable
step-unbounded defense objective $\phi$, $\mathcal{G}\models\phi$ if and only
if $[\mathcal{G}]\models\phi$.

Proof. See Appendix B.We prove that PRISM-games will synthesize the same
strategies for the defender in $\mathcal{G}$ and $[\mathcal{G}]$:

###### Theorem 4.

For an observable step-unbounded defense objective $\ll
D\gg\mathsf{P}_{\bowtie q}[\psi]$ or $\ll D\gg\mathsf{R}_{\bowtie
q}[\mathsf{F}\phi]$, PRISM-games synthesizes the same winning strategies for
the defender in $\mathcal{G}$ and $[\mathcal{G}]$.

Proof. See Appendix C.

##  7\. Evaluation

###  7.1. Implementation

We implemented a prototype in Java and Python to support our approach whose
architecture is shown in Fig. 1. This prototype automatically (i) generates an
attack model from the network security scanning results, (ii) generates its
attack graph using MulVAL, and (iii) transforms it to an SMDP (the PRISM-games
input format). The defender’s behavior is generated in a semi-automatic way.
Given an rPATL formula and the formalized behavior of the attacker and
defender, the tool uses PRISM-games to perform attack-defense analysis and
generate defense strategies.

###  7.2. Security Analysis

Case Study Overview. To evaluate our approach, we designed an attack scenario
against a network with the topology shown in Fig. 3. The network consists of
three zones: the internet, a demilitarized zone (DMZ) that is accessible to
the internet and contains the hosts shown to the right of the router in the
figure, and a protected zone that contains the critical services and
information in the system. This network contains a router firewall that
controls the traffic in the network. Each host in the network has a specific
purpose: plycent01 is an internet-facing frontend server that acts as an
endpoint that exports the services provided by the protected zone to the
internet. plyrhel01 acts as a proxy server between the demilitarized and
protected zones and is responsible for data and request synchronization and
transfer between plycent01 and the application server plycent03. The host
plycent02 is the database server that hosts all data required for the system
to function. Table 1 summarizes the services and vulnerabilities present of
each network host. Table 2 shows the description, and consequences of
exploitation for each vulnerability in the system, according to the CVSS
database.

Figure 3. The network topology and attack steps

The attacker is located in the internet and can access the web pages served by
the http server hosted in plycent01. S/he first compromises playcent01’s web
server by exploiting the vulnerability cve-2018-1273, which enables remote
code execution on the vulnerable host. Since remote code execution has been
gained on plycent01, the attack continues by gaining root privileges on
plycent01 using the vulnerability cve-2017-13215 (Step1). To gain access to
the protected zone, the attacker employs cve-2018-1000120, i.e., a buffer
overflow vulnerability, in the CURL utility used to coordinate information
between plycent01 and plyrhel01, which allows the attacker to obtain the
permission of code execution on plyrhel01 (Step2). plycent3 can then be
reached by plyrhel01 via the vulnerable ssh service running on it.
cve-2018-7566 is exploited on this vulnerable service to gain root privileges
on plycent03 (Step3). The host plycent02 is required to allow database access
to plycen03 in order to be able to store and retrieve information in its
database. The PostgresSQL database hosted on it, however, is improperly
configured and allows unauthenticated, unregulated access to any user that can
connect to it. Therefore, the attacker can exploit that by performing
malicious queries against the database (Step 4). Malicious database queries
can tamper with or delete critical information, or waste time with queries
specifically crafted to do so. A DoS attack can hence be performed in two
ways: either by removing the information requested by other parts of the
system, or by queuing specifically crafted queries that are irrelevant to the
system functional goals.

Table 1. Services and Vulnerabilities of the Hosts Host | Services | Vulnerabilities
---|---|---
plyrhel01 | http | cve-2018-1000120
http proxy | cve-2018-1273
ssh | None
plycent01 | http | cve-2018-1273
(Linux kernel) | cve-2017-13215
plycent02 | postgress | Improper Authentication
ssh | None
plycent03 | ssh | cve-2018-7566
http | cve-2018-1273
Table 2. Description of Vulnerabilities Vulnerability |  Description |  Consequence(s) |  Exp. Score |  Imp. Score
---|---|---|---|---
cve-2018-1000120 |  A buffer overflow exists in CURL in the FTP URL handling. |  Remote Code Execution |  3.9 |  5.9
cve-2017-13215 |  Buggy implementation of symmetric key encryption allows control of kernel space code. |  Privilege Escalation |  1.8 |  5.9
cve-2018-1273 |  Incorrect sanitization of special characters allows code injection. |  Remote Code Execution |  3.9 |  5.9
cve-2018-7566 |  Buffer overflow in the Linux kernel |  Memory Tampering, Authentication Bypass |  1.8 |  5.9

Attacker Behavior. In this scenario, the goal is to launch a DoS attack on the
web server plycent02. We set the attack goal to dos(plycent02) and run MulVAL
to generate the attack graph showing attack scenarios that can lead to this
target goal. The attack graph consists of 50 nodes in total and 18 attack
steps. To obtain the probability of attacker actions, we use the security
metric AGP provided by MulVA. This metric expresses the probability that a
specific node in the attack graph will be reached during an attack that is a
cumulative score. As an input, we need to provide the base score of each
attack step (i.e., rule nodes) that states what is the probability of
successfully performing an attack step, given that all of its prerequisites
are satisfied.

To this end, we use the _exploitability score_ provided by CVSS to measure the
probability of successful exploitation of a specific vulnerability. This
metric considers the four aspects of (a) attack vector (the context by which
the exploitation is possible), (b) attack complexity, (c) privileges required
to succeed, and (d) whether this attack requires interaction with the user or
not. For the other types of attack steps that don’t exploit a vulnerability
and are usually ordinary activities such as using a service etc, we defer to
expert knowledge to set their values properly. In this case study, we set the
score for this kind of activities to 0.8, meaning it is more likely the attack
step is successful. Given the base scores, MulVAL generates the AGP metric for
each rule node automatically according to the approach introduced in (Wang et
al., 2008).

We define two reward structures modeling attack/defense costs: (i)
$\mathsf{aCosts}$, that models the costs of an attack step for the attacker,
and (ii) $\mathsf{dCosts}$, that captures the cost of defense in addition to
the damages that an attacker can cause to the network due to a successful
attack step. To estimate the costs in $\mathsf{aCosts}$, we considered several
factors including the time required to perform the attack, ease of
exploitation and required tools and requirements to perform the attack. To
estimate the damage of an attack step (costs imposed to the defender), we use
the impact score provided by the CVSS database as well as the business
security preferences. Impact score quantifies the outcome that an attacker can
achieve as a result of exploiting the vulnerability. Table 2 presents the
exploitability score (in the range of [0..4]) and impact scores (in the range
of [0..6]) of the vulnerabilities in our case study.

Defender behavior. The countermeasures that we consider in this attack
scenario include stopping a service, limiting access to a service or patching
the vulnerabilities. The costs of such actions depend on many factors,
including the criticality of a service, the availability and difficulty of
patching the vulnerability, the cost incurred to the organization if the
system is not online for a certain period of time, the cost of information
leakage or tampering etc.

We considered three cases of systems that can be developed with the topology
presented in Fig. 3: a tax system, an image hosting system and a hotel booking
system. Each system has its own requirements and preferences in terms of
availability of services and the confidentiality and integrity of the
information. For the tax system, the integrity of information and the
availability of the system when in operation is of the utmost importance, and
therefore the cost of taking any service down is very high. Patching on the
other hand is of minor importance. In the image hosting system, availability
is important but integrity and confidentiality are not the main concerns. All
three aspects of availability, confidentiality and integrity are associated
with some loss of revenue in the hotel booking system, and are then important.
The cost of a defense varies from 0 to 500.

Results. In PRISM-games, it is possible to compute the minimum or maximum
probability of satisfying a property $\psi$ that can be guaranteed by a
coalition $C$
($\langle\\!\langle{C}\rangle\\!\rangle\mathsf{P_{opt}}~{}[\psi]$,
$\mathsf{opt}\in\\{min,max\\}$). The maximum or minimum reward can also be
computed similarly. We checked several properties for each game:

  * P1

What is the minimum cost (defense cost and damages caused by the attacker) to
defend against the attack and block it:
$\langle\\!\langle{\mathsf{def}}\rangle\\!\rangle\mathsf{R}^{\mathsf{dCosts}}_{\mathsf{min}}~{}[\mathsf{F}~{}\mathsf{attackerBlocked}]$.

  * P2

What is the maximum cost for the attacker to launch a DoS attack against the
web server plycent02:
$\langle\\!\langle{\mathsf{def}}\rangle\\!\rangle\mathsf{R}^{\mathsf{aCosts}}_{\mathsf{max}}~{}[\mathsf{F}~{}\mathsf{DoS(plycent02)}]$.

  * P3

What is the maximum probability that the defender blocks the attack, i.e.,

$\langle\\!\langle{\mathsf{def}}\rangle\\!\rangle\mathsf{P_{max}}~{}[\mathsf{F}~{}\mathsf{attackerBlocked}].$

  * P4

What is the minimum probability that the attacker achieves its final goal,
i.e.,

$\langle\\!\langle{\mathsf{att}}\rangle\\!\rangle\mathsf{P_{min}}~{}[\mathsf{F}~{}\mathsf{DoS(plycent02)}].$

Table 3. Results Scheduler | Model Size | Property | Case | Result
---|---|---|---|---
2-actions |  | P1 | Tax System | 732
| Image Hosting | 732
| Hotel Reservation | 732
17.6K/47k | P2 | - | 572
| P3 | - | 0.31
| P4 | - | 0.3
4-actions |  | P1 | Tax System | 277
| Image Hosting | 266
| Hotel Reservation | 318
47K/121k | P2 | - | 671
| P3 | - | 0.67
| P4 | - | 0.39
6-actions |  | P1 | Tax System | 205
| Image Hosting | 185
| Hotel Reservation | 245
97K/242K | P2 | - | 711
| P3 | - | 0.68
| P4 | - | 0.4

We carried out experiments with different schedulers. The attacker performs 14
different types of actions in total and we considered three different
schedulers that return the control to the defender after an action of a
specific type, e.g., when a suspicious log-in happens or traffic is observed.
Table 3 shows the analysis results. The first column shows the number of
attacker action types after which the control returns back to the defender.
The “Model Size”’ column indicates the number of states and transitions of the
security game and “Case”’ shows the corresponding case study.

The analysis results show that, with an increase in the number of actions to
which the defender can react, the size of model increases. This is expected,
as more transitions from the defender will be included in the model and this
will subsequently lead to increasing the state space. In addition, the minimum
cost (attacker damage as well as the defense costs) imposed on the system
decreases with an increase in the number of attacker actions to react to,
e.g., the minimum cost to defend against the attack in the tax system changes
from 732 units to 205 when the number of actions with a defense reaction
changes from 2 actions to 6. This is because the defender has a better chance
of applying an effective countermeasure if control is returned to it more
often. Furthermore, the minimum cost for the attacker to reach its final goal
slightly increases, as with an increase in the defense actions, it might
become more challenging for the attacker to reach its goal and need to try
different scenarios to succeed. Similarly, the probability the defender
succeeds in blocking the attack increases, e.g., from 0.31 with two action
types to 0.68 for the case of 6 action types.

When a property is verified by PRISM-games, it can synthesize a strategy that
specifies an action to be performed in a state so that the property is
satisfied. There are 12 types of defense actions in this case study in total.
For the property P1 under a 2-action scheduler, 11, 10 and 9 types of actions
exist in the strategy for the tax system, the image hosting and the hotel
reservation systems, respectively. The strategy synthesized for the tax system
includes patching cve-2018-1000120 in plyrhel01, while patching this
vulnerability is not recommended for the other two cases. The vulnerability
cve-2018-7566 of the ssh service in plycent03 is not patched in the strategy
synthesized for the hotel reservation system. This could be because blocking
ssh traffic from plyrhel01 to plycent03 is cheaper than patching this
vulnerability here. We believe that an in-depth interpretation of results
requires techniques to synthesize invariants for the states under which a
specific action is suggested, and unfortunately this cannot be done manually
for games with thousands of states like ours.

###  7.3. Performance Analysis

To evaluate the performance of our approach, we conducted some experiments on
a real-life network. This network consists of sixteen hosts offering different
services. We scanned the hosts and identified 155 types of vulnerabilities
that are all reported during the period of 2017-2018 to the CVSS database. All
experiments were run on a machine with a 2.9 GHz Intel Core i7 CPU and 16 GB
RAM, running MacOS Catalina. We conducted experiments with different sets of
observation, vulnerabilities, defense strategies and objectives on a real-life
case study. To test the implementation of our prototype, we ran around 1241
different experiments.

The size of the game model depends on the size of the attack graph and the
number and complexity of defenses. The size of attack graph depends on the
complexity of attack and the number of potential vulnerabilities exploited to
achieve the attack goal, i.e., the number of potential attack scenarios and
their complexity. This does not necessarily depend on the size of network,
i.e., achieving an attack goal in a larger network could be simpler, as it may
contain fewer vulnerabilities but which are severe and lead to more privileges
being gained in fewer steps. As shown in Fig. 4, the size of the attack graph
(i.e., the number of graph nodes) increases with an increase in the number of
vulnerabilities used to achieve a goal.

Moreover, the size of the game model depends on the size of attack graph as
well as the defenses. _Defense strength_ shows the percentage of possible
defenses applied in the system. With an increase in the size of attack graph
and the defense strength, the number of states and transitions increase
accordingly, as illustrated in Fig. 6. In this figure, the color is used to
show the number of states, and the marker size denotes the number of
transitions in the associated point. For the larger attack graphs with large
defense strength, we encountered the state explosion problem. Fig. 5(b) shows
the model checking time of four different properties based on the number of
the model states. The marker size denotes the number of transitions in the
corresponding point. The model checking time was between a few millisecond for
the smaller models to $\sim$120 seconds for a model with $\sim
1.4{\times}10^{6}$ states, and often increases with an increase in the size of
the model.

Figure 4. Attack graph size vs number of exploited vulnerabilities.

(a) Model Size vs Partial observation

(b) Model Checking Time

Figure 5. Model size and verification time

The color shows the number of states in the interval of $(0,1.4*10^{6})$, and
the size of point indicates the number of transitions in the interval of
$(0,14.5*10^{6})$

Figure 6. Defense strength, attack graph size, and the game size.

In another set of experiments, we studied the effect of the defense strength
on the attack cost (i.e., the cost for the attacker to successfully achieve
its goal). As shown in Fig. 7, the minimum attack cost often increases with an
increase in the defense strength. Note that the attack cost depends on other
factors such as which defenses are applied, when and where they are applied
etc. For instance, the attack cost for the goal expr5 with the defense
strength of 90% is less than that of 75%. The reason is that the selected
countermeasures in the 90% case altogether performed weaker compared to the
case of 75%, as they do not block a cheaper attack path prevented by the
countermeasures of the case of 75%.

The number of transitions of a security game under perfect and partial
observation for six different experiments is presented in Fig. 5(a). The
x-axis shows the experiment ID and the y-axis shows the sum of the number of
transitions and states for different observations. In these experiments, the
types of attacker actions was between nine and sixteen types. We run each
experiment under five different observations, including full observation
(Observable) and $n$ unobservable actions, $1\leq n\leq 4$. In this figure,
$n-$Unobservable means that $n$ actions of the attacker have become
unobservable. We considered those actions that are harder to be certainly
associated to a malicious activity as unobservable actions.

Figure 7. Minimum attack cost vs defense strength.

In some experiments, while the number of state variables remained fixed
(because the consequences of unobservable actions were partially observable,
i.e., neither fully observable nor partially observable), the model size was
reduced significantly. With an increase in the number of unobservable actions,
the number of transitions has been reduced accordingly. For instance, in the
experiment 5, the model size for the case of full observation is $\sim$9.7M,
while it reduces to $\sim$6.2M, $\sim$2.9M, $\sim$1.5, and 0.6M respectively
for 1 to 4 unobservable actions. Our experiments show that this transformation
can be used as a state reduction technique to tackle the complexity of large-
scale attack graphs. We can transform a perfect security game with a large
state space to a smaller game, in which some of the sub-scenarios that do not
trigger any defense are abstracted away by being considered as a single step.
This leads to a more abstract game where the internal details of the
attacker’s behavior are hidden and only their interactions with the defender
are taken into account.

###  7.4. Discussion

Scalability of the approach depends mainly on the number of vulnerabilities
that exist in the network and their dependency degree. The more
vulnerabilities in the network that can be chained, the larger the game would
be. Our results show that it’s possible to analyze a real-life network within
a reasonable time, however, the approach may not scale for large networks with
dozens of vulnerabilities. A solution to this problem is extending the
approach to support modular analysis to handle scalability.

Furthermore, the verification results are often usable by the user, however,
it’s not generally always possible for the end user to comprehend synthesis
analysis results due to the large state space of games. Our primary goal was
to automate defense. Hence, we are integrating our approach in an online
monitor with self-protection capabilities to either apply the defenses
automatically, or guide the administrator to enforce proper countermeasures at
runtime. Accuracy of some parameters such as attack probabilities is an
important factor to achieve reasonable results. The online monitor enables us
enhance the approach at runtime to improve the accuracy of parameters based on
the attacker’s behavior.

The assumption that all defense-triggering capabilities of the attacker are
observable can be theoretically restrictive, yet a realistic and necessary
constraint, as it’s impossible to react to an invisible action. If a game
ideally needs reacting to an unobservable action, we can modify the game into
a similar game with a slightly different defender behavior. One option is to
move the defenses of unobservable capabilities to an earlier observable step.
This means that the defender should react earlier that can sometimes become
more expensive. The other option is to remove such defenses completely, as
it’s not anyhow feasible to react in such cases. Observe that the results
won’t be wrong, but they might be less optimal.

Another limitation of our approach is that it protects the system against
known attacks, and zero-day vulnerabilities/attacks cannot be handled by this
approach. We plan to enhance it with online attack scenario extraction to be
able to handle unknown attacks. Moreover, the expressiveness of the properties
is restricted, as the next and bounded operators are not supported. We believe
this subset of rPATL is still reasonable, because we can check important
reachability properties, as shown in the experiments.

##  8\. Related Work

Games In Security. The authors in (Durkota et al., 2015) proposed a game-
theoretic approach for network hardening problem where the attacker plan is
represented as an attack graph and the defender seeks an optimal solution to
deploy honeypots into the network to deceive the attacker. A two-player
strategic game based on an extension of attack trees was constructed in
(Bistarelli et al., 2007), where the defender wants to protect the system by
buying countermeasures and the attacker tries to exploit the vulnerabilities
and gain some profit. The game is solved by finding the Nash equilibria, with
the goal of finding the most promising attack/defense’s actions. Chowdhary et
al. (Chowdhary et al., 2019) uses attack graphs to build a zero-sum stochastic
Markov game between the attacker and the defender to help the admin apply
countermeasures in a cloud network. None of the above approaches supports
partial observations. In contrast to (Durkota et al., 2015; Chowdhary et al.,
2019) that are application-specific, our approach can be applied to any type
of networks and defenses. Our experiments show that our approach is faster
than (Durkota et al., 2015): we analyze a network with $\sim$53
vulnerabilities in $<1$s while (Durkota et al., 2015) requires $1s<t<1000s$
for the analysis of a network with 8 types of vulnerabilities.

In (Aslanyan et al., 2016), an extension of attack/defense trees with the
temporal ordering of actions is used to build a two-player stochastic game
between the attacker and the defender. They use probabilistic model checking
techniques to formally verify security properties of the attack-defense
scenarios, and synthesize strategies for attackers or defenders using PRISM-
games. A similar approach is taken in (Eisentraut and Kretinsky, 2019), but
with some relaxed model assumptions and some additional optimizations.
Gadyatskay et al. define a stochastic timed semantics for attack-defense trees
in terms of a network of timed automata in (Gadyatskaya et al., 2016). They
use the UPPAAL model checker to perform a quantitative analysis and find
attacker parameters that minimize cost. In contrast to (Aslanyan et al., 2016;
Eisentraut and Kretinsky, 2019; Gadyatskaya et al., 2016), we use attack
graphs that can be generated fully automatically and we support partial
observation, while automatic construction of attack trees is still a major
challenge despite the recent efforts (Widełet al., 2019). Our security game is
boolean which makes it more scalable for analysis of realistic network
systems, as confirmed by our experiments results.

Analysis under Partial Observation. Partially observable Markov decision
processes (POMDPs) extend MDPs with partial observability and have many
applications in fields such as AI, scheduling and planning (e.g., (Patil et
al., 2014; Grady et al., 2015; Jagannathan et al., 2013; Winterer et al.,
2017)). The formal verification community has studied POMDPs and presented
theoretical results, e.g., (Chatterjee et al., 2013a; Chatterjee and Doyen,
2014), however, progress on developing practical methods has been limited.
Norman et al. presented an approach for verification and control of a real-
time extension of POMDPs called partially observable probabilistic time
automata (POPTAs) (Norman et al., 2017). Properties are specified using a
probabilistic temporal logic and techniques are proposed to either verify the
property or to synthesize a controller for the model to enforce it. Model
checking of both POMDPs and POPTAs is implemented in PRISM.

In(Winterer et al., 2017), the problem of motion planning, that is often
modeled as a POMDP, is reduced to a two-player stochastic game and solved
using PRISM-games. Also relevant is the recent extension of PRISM-games to
concurrent stochastic games (Kwiatkowska et al., 2018), which provides an
alternative way to model concurrent decision making in a probabilistic
setting. Finally, the problem of controller synthesis for timed games under
state-based partial observation has been studied in (Cassez et al., 2007) and
implemented in UPPAAL-TIGA(Behrmann et al., 2007). We are not aware of any
practical solution for stochastic games under partial observation.

Threat Modeling and Analysis. Threat modeling and analysis focuses on using
models to describe, analyze and discover security problems of a system (Kordy
et al., 2013; Ou et al., 2005; Widełet al., 2019). Such techniques are usually
provided with quantitative analysis methods to perform security risk
assessment, which enables us to understand the attack consequences better and
plan more effective countermeasures to defend against attacks. Quantitative
analysis in threat models, for the purpose of risk assessment, is often
performed based on measuring the security risk of a system using a few
security metrics (Ramos et al., 2017). Attack trees and graphs, including
their different variants, are well-established and commonly-used techniques
for security modeling. Widel et al. (Widełet al., 2019) survey the application
of formal methods on interpretation, semi-automatic construction and
quantitative analysis of attack trees. Several variants of attack graphs have
been introduced in the literature, e.g., vulnerability cause graphs (Ardi et
al., 2006), Bayesian attack graph (Marcel Frigault, 2008) and compromise
graphs (McQueen et al., 2006). Formal methods have been used to generate
attack graphs, e.g., Sheyner et al. (Sheyner et al., 2002; Jha et al., 2002)
use model checking techniques to generate attack graphs. Khakpour et al.
(Khakpour et al., 2019) proposed an approach using attack graphs to control
the system behavior in a more secure way.

##  9\. Conclusions

In this paper, we proposed a game-theoretic approach for the analysis of
attack graphs under partial observation. We automatically constructed a two-
player security game from an attack graph and the defender’s behavior and used
PRISM-games to analyze the game and synthesize strategies for the players. To
support defense under partial observation, we introduced one-sided partially
observable security games and presented an algorithm to transform them to
perfect games. We have proven the soundness of our algorithm for ODT security
games and a sub-set of objectives. To support the approach, we developed a
prototype and conducted some experiments to evaluate it. Our experiments show
that the transformation algorithm can be used as a suitable state reduction
technique to handle large-scale attack graphs. We are currently integrating
our approach in a self-protection engine to support online defense. We plan to
extend our experiments to study the impact of different factors on the
effectiveness of a defense.

_Acknowledgment_ The first author was supported by the Swedish Knowledge
Foundation (No. 20160186).

## References

  * (1)
  * Ardi et al. (2006) Shanai Ardi, David Byers, and Nahid Shahmehri. 2006.  Towards a Structured Unified Process for Software Security. In _Proceedings of the 2006 International Workshop on Software Engineering for Secure Systems_ (Shanghai, China) _(SESS ’06)_. ACM, New York, NY, USA, 3–10.  https://doi.org/10.1145/1137627.1137630
  * Aslanyan et al. (2016) Zaruhi Aslanyan, Flemming Nielson, and David Parker. 2016\.  Quantitative Verification and Synthesis of Attack-Defence Scenarios. In _IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016_. 105–119.  https://doi.org/10.1109/CSF.2016.15
  * Behrmann et al. (2007) Gerd Behrmann, Agnes Cougnard, Alexandre David, Emmanuel Fleury, Kim G Larsen, and Didier Lime. 2007.  UPPAAL TIGA user-manual.  _Aalborg University_ (2007).
  * Bistarelli et al. (2007) Stefano Bistarelli, Marco Dall’Aglio, and Pamela Peretti. 2007\.  Strategic Games on Defense Trees. In _Formal Aspects in Security and Trust_ , Theo Dimitrakos, Fabio Martinelli, Peter Y. A. Ryan, and Steve Schneider (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–15.
  * Cassez et al. (2007) Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, and Jean-François Raskin. 2007\.  Timed Control with Observation Based and Stuttering Invariant Strategies. In _Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings_. 192–206.  https://doi.org/10.1007/978-3-540-75596-8_15
  * Chatterjee et al. (2013a) Krishnendu Chatterjee, Martin Chmelik, and Mathieu Tracol. 2013a.  What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives. In _Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy_. 165–180.  https://doi.org/10.4230/LIPIcs.CSL.2013.165
  * Chatterjee and Doyen (2014) Krishnendu Chatterjee and Laurent Doyen. 2014.  Partial-Observation Stochastic Games: How to Win when Belief Fails.  _ACM Trans. Comput. Log._ 15, 2 (2014), 16:1–16:44.  https://doi.org/10.1145/2579821
  * Chatterjee et al. (2013b) Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2013b.  A survey of partial-observation stochastic parity games.  _Formal Methods in System Design_ 43, 2 (2013), 268–284.  https://doi.org/10.1007/s10703-012-0164-2
  * Chen et al. (2013) T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. 2013.  Automatic Verification of Competitive Stochastic Systems.  _Formal Methods in System Design_ 43, 1 (2013), 61–92.
  * Chowdhary et al. (2019) Ankur Chowdhary, Sailik Sengupta, Adel Alshamrani, Dijiang Huang, and Abdulhakim Sabur. 2019\.  Adaptive MTD Security using Markov Game Modeling. In _International Conference on Computing, Networking and Communications, ICNC 2019, Honolulu, HI, USA, February 18-21, 2019_. 577–581.  https://doi.org/10.1109/ICCNC.2019.8685647
  * Condon (1992) Anne Condon. 1992\.  The Complexity of Stochastic Games.  _Inf. Comput._ 96, 2 (1992), 203–224.  https://doi.org/10.1016/0890-5401(92)90048-K
  * Durkota et al. (2015) Karel Durkota, Viliam Lisý, Branislav Bosanský, and Christopher Kiekintveld. 2015.  Optimal Network Security Hardening Using Attack Graph Games. In _Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015_. 526–532.  http://ijcai.org/Abstract/15/080
  * Eisentraut and Kretinsky (2019) Julia Eisentraut and Jan Kretinsky. 2019.  Expected Cost Analysis of Attack-Defense Trees. In _Proc. 17th International Conference on Quantitative Evaluation of Systems (QEST’19)_ _(LNCS, Vol. 11785)_. Springer, 203–221.
  * Gadyatskaya et al. (2016) Olga Gadyatskaya, René Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay, Mads Chr. Olesen, and Danny Bøgsted Poulsen. 2016\.  Modelling Attack-defense Trees Using Timed Automata. In _Formal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings_. 35–50.  https://doi.org/10.1007/978-3-319-44878-7_3
  * Grady et al. (2015) Devin K. Grady, Mark Moll, and Lydia E. Kavraki. 2015\.  Extending the Applicability of POMDP Solutions to Robotic Tasks.  _IEEE Trans. Robotics_ 31, 4 (2015), 948–961.  https://doi.org/10.1109/TRO.2015.2441511
  * Hong et al. (2017) Jin B. Hong, Dong Seong Kim, Chun-Jen Chung, and Dijiang Huang. 2017.  A survey on the usability and practical applications of Graphical Security Models.  _Computer Science Review_ 26 (2017), 1 – 16.  https://doi.org/10.1016/j.cosrev.2017.09.001
  * Jagannathan et al. (2013) Krishna P. Jagannathan, Shie Mannor, Ishai Menache, and Eytan Modiano. 2013.  A State Action Frequency Approach to Throughput Maximization over Uncertain Wireless Channels.  _Internet Mathematics_ 9, 2-3 (2013), 136–160.  https://doi.org/10.1080/15427951.2011.601934
  * Jha et al. (2002) Somesh Jha, Oleg Sheyner, and Jeannette Wing. 2002.  Two formal analyses of attack graphs. In _Proceedings 15th IEEE Computer Security Foundations Workshop. CSFW-15_. IEEE, 49–63.
  * Khakpour et al. (2019) Narges Khakpour, Charilaos Skandylas, Goran Saman Nariman, and Danny Weyns. 2019.  Towards secure architecture-based adaptations. In _Proceedings of the 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS@ICSE 2019, Montreal, QC, Canada, May 25-31, 2019_. 114–125.  https://doi.org/10.1109/SEAMS.2019.00023
  * Kordy et al. (2013) Barbara Kordy, Ludovic PiÃštre-CambacÃ©dÃšs, and Patrick Schweitzer. 2013\.  DAG-Based Attack and Defense Modeling: Don’t Miss the Forest for the Attack Trees.  _Computer Science Review_ 13 (03 2013).  https://doi.org/10.1016/j.cosrev.2014.07.001
  * Kwiatkowska et al. (2018) M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. 2018\.  Automated Verification of Concurrent Stochastic Games. In _Proc. 15th International Conference on Quantitative Evaluation of SysTems (QEST’18)_ _(LNCS, Vol. 11024)_. Springer, 223–239.
  * Kwiatkowska et al. (2017) Marta Kwiatkowska, David Parker, and Clemens Wiltsche. 2017\.  PRISM-games: Verification and Strategy Synthesis for Stochastic Multi-player Games with Multiple Objectives.  _International Journal on Software Tools for Technology Transfer_ 20, 2 (2017), 195–210.
  * Manshaei et al. (2013) Mohammad Hossein Manshaei, Quanyan Zhu, Tansu Alpcan, Tamer Basar, and Jean-Pierre Hubaux. 2013\.  Game theory meets network security and privacy.  _ACM Comput. Surv._ 45, 3 (2013), 25:1–25:39.  https://doi.org/10.1145/2480741.2480742
  * Marcel Frigault (2008) Lingyu Wang Marcel Frigault. 2008\.  Measuring Network Security Using Bayesian Network-Based Attack Graphs. In _2008 32nd Annual IEEE International Computer Software and Applications Conference_. 698–703.  https://doi.org/10.1109/COMPSAC.2008.88
  * McQueen et al. (2006) Miles A. McQueen, Wayne F. Boyer, Mark A. Flynn, and George A. Beitel. 2006.  Quantitative Cyber Risk Reduction Estimation Methodology for a Small SCADA Control System. In _Proceedings of the 39th Annual Hawaii International Conference on System Sciences (HICSS’06)_ , Vol. 9. 226–226.  https://doi.org/10.1109/HICSS.2006.405
  * Norman et al. (2017) Gethin Norman, David Parker, and Xueyi Zou. 2017.  Verification and control of partially observable probabilistic systems.  _Real-Time Systems_ 53, 3 (2017), 354–402.  https://doi.org/10.1007/s11241-017-9269-4
  * Ou et al. (2005) Xinming Ou, Sudhakar Govindavajhala, and Andrew W. Appel. 2005\.  MulVAL: A Logic-based Network Security Analyzer. In _Proceedings of the 14th Conference on USENIX Security Symposium - Volume 14_ (Baltimore, MD) _(SSYM’05)_. USENIX Association, Berkeley, CA, USA, 8–8.  http://dl.acm.org/citation.cfm?id=1251398.1251406
  * Patil et al. (2014) Sachin Patil, Gregory Kahn, Michael Laskey, John Schulman, Ken Goldberg, and Pieter Abbeel. 2014\.  Scaling up Gaussian Belief Space Planning Through Covariance-Free Trajectory Optimization and Automatic Differentiation. In _Algorithmic Foundations of Robotics XI - Selected Contributions of the Eleventh International Workshop on the Algorithmic Foundations of Robotics, WAFR 2014, 3-5 August 2014, Boğaziçi University, İstanbul, Turkey_. 515–533.  https://doi.org/10.1007/978-3-319-16595-0_30
  * Ramos et al. (2017) Alex Ramos, Marcella Lazar, Raimir H. Filho, and Joel J. P. C. Rodrigues. 2017.  Model-Based Quantitative Network Security Metrics: A Survey.  _IEEE Communications Surveys Tutorials_ 19, 4 (Fourthquarter 2017), 2704–2734.  https://doi.org/10.1109/COMST.2017.2745505
  * Samarji et al. (2013) Layal Samarji, Frédéric Cuppens, Nora Cuppens-Boulahia, Wael Kanoun, and Samuel Dubus. 2013.  Situation calculus and graph based defensive modeling of simultaneous attacks.  In _Cyberspace safety and security_. Springer, 132–150.
  * Sheyner et al. (2002) Oleg Sheyner, Joshua Haines, Somesh Jha, Richard Lippmann, and Jeannette M Wing. 2002.  Automated generation and analysis of attack graphs. In _Proceedings 2002 IEEE Symposium on Security and Privacy_. IEEE, 273–284.
  * Simaitis (2014) A. Simaitis. 2014\.  _Automatic Verication of Competitive Stochastic Systems_.  Ph. D. Dissertation. Department of Computer Science, University of Oxford.
  * van Leeuwen (1990) Jan van Leeuwen (Ed.). 1990\.  _Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics_.  Elsevier and MIT Press.  https://www.sciencedirect.com/book/9780444880741/formal-models-and-semantics
  * Wang et al. (2008) Lingyu Wang, Tania Islam, Tao Long, Anoop Singhal, and Sushil Jajodia. 2008.  An Attack Graph-Based Probabilistic Security Metric. In _Data and Applications Security XXII, 22nd Annual IFIP WG 11.3 Working Conference on Data and Applications Security, London, UK, July 13-16, 2008, Proceedings_. 283–296.  https://doi.org/10.1007/978-3-540-70567-3_22
  * Weiss (1991) Jonathan D Weiss. 1991\.  A system security engineering process. In _Proceedings of the 14th National Computer Security Conference_ , Vol. 249. 572–581.
  * Widełet al. (2019) Wojciech Wideł, Maxime Audinot, Barbara Fila, and Sophie Pinchinat. 2019.  Beyond 2014: Formal Methods for Attack Tree–based Security Modeling.  _ACM Comput. Surv._ 52, 4, Article 75 (Aug. 2019), 36 pages.  https://doi.org/10.1145/3331524
  * Winterer et al. (2017) Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, and Bernd Becker. 2017.  Motion planning under partial observability using game-based abstraction. In _56th IEEE Annual Conference on Decision and Control, CDC 2017, Melbourne, Australia, December 12-15, 2017_. 2201–2208.  https://doi.org/10.1109/CDC.2017.8263971
  * Yuan et al. (2014) Eric Yuan, Naeem Esfahani, and Sam Malek. 2014\.  A Systematic Survey of Self-Protecting Software Systems.  _ACM Trans. Auton. Adapt. Syst._ 8, 4, Article 17 (Jan. 2014), 41 pages.  https://doi.org/10.1145/2555611

## Appendix

###  A. rPATL Semantics

A path of $\mathcal{G}$ is a possibly infinite sequence
$\pi=s_{0}\sigma_{0}s_{1}\sigma_{1}\ldots$ where ${s_{i}\in S}$,
${\sigma_{i}\in\Sigma}$, $\Delta(s_{i},a_{i})(s_{i+1})>0$, for all $0\leq
i(\leq n)$. A suffix of $\pi$ starting from the $i$-th state is denoted by
$\pi_{i}=s_{i}a_{i}\ldots$. A strategy $\gamma_{i}$ for a player ${i\in P}$
(or a coalition of players) is a function
${\gamma_{i}:(S\times\Sigma)^{*}S_{i}\to\mathbb{P}_{\Sigma}}$ that assigns a
probability distribution $\gamma_{i}(\pi.s)$ over actions $\Sigma(s)$ from a
state $s$ with a history of $\pi$ (Simaitis, 2014). A strategy is memoryless
if it does not depend on the history, i.e., for all paths $\pi$ and
$\pi^{\prime}$, $\gamma_{i}(\pi.s)=\gamma_{i}(\pi^{\prime}.s)$. A strategy
profile consists of the strategies of all players, i.e.,
$\gamma=\gamma_{1},\gamma_{2}$. By following the strategy $\gamma_{i}$,
whenever the history of a game played on $\mathcal{G}$ is $\pi.s$ where $s\in
S_{i}$, the player $i$ chooses the next move according to the probability
distribution $\gamma_{i}(\pi.s)$. We denote the set of strategies of the
player $i$ by $\Gamma_{i}$. The behavior of a game under a given strategy
profile is probabilistic, and we can define the probability measure
$\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}$ over its (infinite)
paths from a state $s$. We use
$\mathbb{E}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}(Y)$ to denote the expected
value of a random variable $Y$ with respect to
$\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}$.

###### Definition 0 (rPATL Semantics (Chen et al., 2013)).

The semantics of a state formula $\phi$ is defined inductively for each state
$s$ of $\mathcal{G}$ as follows:

$\begin{array}[]{rll}s\models\top&&s\models\alpha\Leftrightarrow{\alpha\in\mathcal{L}(s)}\\\
s\models\neg\phi&\Leftrightarrow&s\not\models\phi\\\
s\models\phi_{1}\wedge\phi_{2}&\Leftrightarrow&s\models\phi_{1}\wedge
s\models\phi_{2}\\\
s\models{\langle\\!\langle{C}\rangle\\!\rangle}\mathsf{P}_{\bowtie\,p}[\psi]&\Leftrightarrow&\exists\gamma_{1}\in\Gamma_{C}\textnormal{
such that }\forall\gamma_{2}\in\Gamma_{P\backslash C}\\\
&&\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}(\psi)\bowtie p\\\
s\models{\langle\\!\langle{C}\rangle\\!\rangle}\mathsf{R}_{\bowtie\,x}[\mathsf{F}\phi]&\Leftrightarrow&\exists\gamma_{1}\in\Gamma_{C}\textnormal{
such that }\forall\gamma_{2}\in\Gamma_{P\backslash C}\\\
&&\mathbb{E}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}[rew(r,\mathsf{F}\phi)]\bowtie
x\\\ \\\ \end{array}$

where $\mathcal{L}(s)$ returns the set of propositions that hold in the state
$s$ and
$\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}(\psi)=\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}(\\{\pi~{}|~{}\pi\models\psi\\})$
is a path probability measure and, informally, gives the probability of
satisfying the formula $\psi$ in the state $s$ under the strategy profile
$\gamma_{1},\gamma_{2}$, where, for path $\pi$:

$\begin{array}[]{rll}\pi\models\mathsf{X}\psi&\Leftrightarrow&\pi_{1}\models\psi\\\
\pi\models\psi_{1}\mathsf{U}^{\leq
k}\psi_{2}&\Leftrightarrow&\pi_{i}\models\psi_{2}\textnormal{ for some }i\leq
k\textnormal{ and }\pi_{j}\models\psi_{1}\\\ &&\textnormal{ for }0\leq j<i\\\
\pi\models\psi_{1}\mathsf{U}\psi_{2}&\Leftrightarrow&\psi_{1}\mathsf{U}^{\leq
k}\psi_{2}\textnormal{ for some }k\in\mathbb{N}\end{array}$

We use $\mathit{rew}(r,\mathsf{F}\phi)$ to denote the random variable that
maps any infinite path to the sum of rewards $r$ accumulated until a state in
$\mathsf{Sat}(\phi)$ is reached, or $\infty$ if no such state is reached.

Let ${\mathrm{opt}_{s}=\max}$ if $s\in S_{C}$ (i.e., it’s a state of a player
from the coalition $C$) and ${\mathrm{opt}_{s}=\min}$ otherwise. The
probability measure of the next operator is defined as
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\mathsf{X}\phi)=\underset{a\in{\Sigma(s)}}{\mathrm{opt}_{s}}~{}\underset{s^{\prime}\in\mathsf{Sat}(\phi)}{\sum}\Delta(s,a)s^{\prime}$.
The probabilities for $\mathsf{U}^{\leq k}$ are defined recursively:

(4) $\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\phi_{1}\mathsf{U}^{\leq
k}\phi_{2})=\begin{cases}1&s\in\mathsf{Sat}(\phi_{2})\\\
0&s\notin(\mathsf{Sat}(\phi_{1})\cup\mathsf{Sat}(\phi_{2}))\\\
0&k=0,s\in\mathsf{Sat}(\phi_{1})\backslash\mathsf{Sat}(\phi_{2})\\\
Y&\text{otherwise}\end{cases}$

where
$Y=\underset{a\in{\Sigma(s)}}{\mathrm{opt}_{s}}~{}\underset{s^{\prime}\in
S}{\sum}\Delta(s,a)(s^{\prime})\times\mathrm{Pr}^{\max,\min}_{\mathcal{G},s^{\prime}}(\phi_{1}\mathsf{U}^{\leq
k-1}\phi_{2})$. The unbounded case is computed via value iteration (Condon,
1992):

$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\phi_{1}\mathsf{U}\phi_{2})=\lim_{k\to\infty}\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\phi_{1}\mathsf{U}^{\leq
k}\phi_{2})$

Lastly, expected rewards
$\mathbb{E}^{\max,\min}_{\mathcal{G},s}(\mathsf{F}\phi)$ are computed
similarly, via value iteration, but using a two-step process that first
computes an upper bound and then converges from above (Chen et al., 2013).

The model checking algorithm of rPATL works based on labeling each state $s$
with the formulas that hold in that state, i.e., $\mathsf{Sat}(s)$, in a
recursive way. Model checking of properties reduces to computation of optimal
probabilities on the game $\mathcal{G}$. For example, if
${\bowtie\in\\{\geq,>\\}}$, then
${s\models{\ll{\\{1\\}}\gg}\mathsf{P}_{\bowtie~{}q}[\psi]\Leftrightarrow\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)~{}\bowtie~{}q}$
where
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)\overset{\mathrm{def}}{=}\underset{{\gamma_{1}\in\Gamma_{1}}}{\sup}\underset{{\gamma_{2}\in\Gamma_{2}}}{\inf}\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}(\psi)$,
i.e., the player $1$ follows the most promising strategies to succeed while
the opponent uses a strategy that is more likely led to failing $\psi$.

###  B. Proof of Theorem 3

Theorem 3 follows from Lemma 6 and Theorem 3.

We use the following notations in this section:

  * •

$G$ is an arbitrary attack graph,

  * •

$\mathrm{AT}=\langle{V}_{A},\vec{\nu}_{A,0},\bar{{{\mathcal{R}}}},\delta_{A}\rangle$
defines the semantics of $G$ according to Definition 1.

  * •

$\Sigma_{{O}}\subseteq\Sigma_{A}$ is the set of attacker’s observable actions.

  * •

$[\mathrm{AT}]=\langle{V}_{O},\vec{\nu}_{{O},0},\Sigma_{{O}},\delta_{O}\rangle$
is a SMDP that specifies the semantics of the PO-attacker’s behavior under the
partial observation $\Sigma_{{O}}$ obtained using Definition 2.

  * •

$\mathrm{DE}=\langle{V}_{D},\vec{\nu}_{D,0},\Sigma_{D},\delta_{D}\rangle$ is
an arbitrary defender.

  * •

${{{\overline{\mathrm{AT}}}}}$, ${\overline{\mathrm{DE}}}$ and
${\overline{[\mathrm{AT}]}}$ are the MDPs that respectively describe the
semantics of $\mathrm{AT}$, $\mathrm{DE}$ and $[\mathrm{AT}]$.

  * •

$\mathcal{G}=\langle\\{A,D\\},V,S_{A}\cup
S_{D},{\mathsf{Obs}},s_{0},\Sigma,\mathsf{sch},\Delta\rangle$ denotes the PO
security game
${{{\overline{\mathrm{AT}}}}}~{}||~{}{{\overline{\mathrm{DE}}}}{}$ constructed
using the functions ${\mathsf{Obs}}$ and $\mathsf{up}$ in Equation 1 and
Equation 2.

  * •

$[\mathcal{G}]=\langle\\{A,D\\},{V}^{\prime},S^{\prime}_{A}\cup
S^{\prime}_{D},s^{\prime}_{0},\Sigma^{\prime},\mathsf{sch},\Delta^{\prime}\rangle$
represents the perfect game
$[{{\overline{\mathrm{AT}}}}]~{}||~{}{{\overline{\mathrm{DE}}}}$.

  * •

$V_{AD}=V_{A}\cap V_{D}$ is the set of attacker’s defense-triggering
capabilities stored in the defender’s state, and $V^{\prime}_{AD}$ is the
attacker’s copy of the same variables in the PO security game.

We first show that $\mathcal{G}$ and $[\mathcal{G}]$ are weak bisimilar (van
Leeuwen, 1990). Let $s=_{V}s^{\prime}$ be a notation used to denote that the
variables of $V$ have the same values in the states $s$ and $s^{\prime}$,
i.e., the projections of $s$ and $s^{\prime}$ on the variables $V$ are
identical. Let $\Delta{}$ be a (concrete) transition relation. We define the
relation $\overset{}{\Longrightarrow}$ as follows:

  * •

$s\overset{\tau}{\Longrightarrow}s$,

  * •

$s\overset{\tau}{\Longrightarrow}s^{\prime}$ if $\Delta{}(s,a)s^{\prime}>0$
and $a\notin\Sigma_{{O}}$, and

  * •

$s\overset{\top}{\Longrightarrow}s^{\prime\prime}$ if
$s\overset{\tau}{\Longrightarrow}s^{\prime}$,
$\Delta{}(s^{\prime},a)s^{\prime\prime}>0$ and $a\in\Sigma_{{O}}$.

###### Definition 0 (Weak Bisimulation).

Let $\mathcal{G}=\langle\\{A,D\\},V,S,s_{0},\Sigma,\mathsf{sch},\Delta\rangle$
and
$\mathcal{G}^{\prime}=\langle\\{A,D\\},V^{\prime},S^{\prime},s^{\prime}_{0},\Sigma^{\prime},\mathsf{sch}^{\prime},\Delta^{\prime}\rangle$
be two two-player games. A relation $R\subseteq S\times S^{\prime}$ is a weak
bisimulation relation, iff for all $(s,s^{\prime})\in R$, ${s=_{V\cap
V^{\prime}}s^{\prime}}$ and $s\overset{\top}{\Longrightarrow}t$ implies that
there exists a state $t^{\prime}\in S^{\prime}$ such that
$s^{\prime}\overset{\top}{\Longrightarrow}t^{\prime}$ and $(t,t^{\prime})\in
R$ and vice versa. We say $\mathcal{G}$ and $\mathcal{G}^{\prime}$ are weak
bisimilar, denoted by $\mathcal{G}\sim\mathcal{G}^{\prime}$, if and only if
there exists a weak bisimulation relation $R\subseteq S\times S^{\prime}$ such
that $(s_{0},s^{\prime}_{0})\in R$.

###### Theorem 3 (Weak Bisimulation of Security Games).

The ODT security game ${\mathcal{G}}$ and its transformation to the perfect
security game $[\mathcal{G}]$ are weak bisimilar, i.e., there is a relation
$R\subseteq S\times S^{\prime}$ that is a witnessing weak bisimulation
relation where $S=S_{A}\cup S_{D}$ and $S^{\prime}=S^{\prime}_{A}\cup
S^{\prime}_{D}$..

Proof. To prove this theorem, we should find a relation $R\subseteq S\times
S^{\prime}$ that is a witnessing weak bisimulation relation where $S=S_{A}\cup
S_{D}$ and $S^{\prime}=S^{\prime}_{A}\cup S^{\prime}_{D}$. We will show that
the following relation is a witnessing weak bisimulation relation and
$(s_{0},s^{\prime}_{0})\in R$:

$R=\\{\langle
s,s^{\prime}\rangle~{}|~{}s\downarrow_{({V}_{O}\backslash{V}^{\prime}_{AD})\cup{V}_{D}\cup\\{t\\}}=s^{\prime}\\}.$

This relation groups the states in which the defender’s observations are the
same, i.e., the local part of the attacker’s state (i.e.,
${V}_{O}\backslash{V}^{\prime}_{AD}$), the defender’s substate and the
scheduler’s substates in the ODT security game should be identical to those of
the perfect game’s state.

We should show that this candidate relation is a weak bisimulation relation.
Consider two states $s$ and $s^{\prime}$ where $\langle s,s^{\prime}\rangle\in
R$. According to the definition of $R$, the current active player of $s$ and
$s^{\prime}$ should be the same (i.e., $t$ has an identical value in $s$ and
$s^{\prime}$according to $R$). Two cases can happen:

Case i If $s\in S_{D}$, since ${V}_{AD}\subseteq{V}_{O}$ (from Definition 1),
the same transitions of the defender will be enabled in both games according
to Definition 3, Definition 3, Definition 1 and Equation 1. Since the
defender’s state in $s$ and $s^{\prime}$ are identical according to $R$, the
updates by the defender (i.e., to the variables $V_{D}$ and $V_{O}$) will be
the same according to Equation 2, Definition 3 and Definition 1, i.e., the
target states $t$ and $t^{\prime}$ will be in the relation $R$ too.

Case ii If $s\in S_{A}$, let $s\overset{\top}{\Longrightarrow}\gamma$, i.e.,
$s\overset{\sigma_{0}}{\rightarrow}s_{0}\ldots
s_{n}\overset{\sigma_{n}}{\rightarrow}\gamma$ where $\sigma_{n}\in\Sigma_{O}$
and $\sigma_{i}\notin\Sigma_{O}$, $0\leq i<n$. According to Definition 1, an
attacker tries an action, if it leads to gaining a new capability. This means
that this sequence leads to updating the consequences of each one of the
actions in the sequence, i.e., $e_{i}\mapsto\top,0\leq i\leq n$ where $e_{i}$
is the consequence capability of $\sigma_{i}$. According to Equation 2,
$e_{i}$’s will be updated in the attacker’s substate of $\gamma$ where $0\leq
i\leq n$, while only $e_{n}$ is updated in the $\gamma$’s defender’s substate.

It is trivial to show that this sequence corresponds to a transition with a

$\mathsf{dop}=\underset{c_{i}\in\mathsf{pred}(\sigma_{i}),0\leq i\leq
n,c_{i}\notin\\{e_{0},\ldots,e_{n}\\}}{\bigcup}c_{i}$ in the perfect game
$[\mathcal{G}]$ according to Definition 2 and Definition 3. This transition
will lead to a state $\gamma^{\prime}$ in which $e_{n}$ will be set, i.e.,
$e_{n}\mapsto\top$. Hence, the projection of $\gamma$ on the union of the
attacker’s local substate, the defender’s state and the scheduler (according
to Equation 3) will be identical to $\gamma^{\prime}$, i.e.,
$\gamma\downarrow_{({V}_{O}\backslash{V}_{AD})\cup{V}_{D}\cup\\{t\\}}=\gamma^{\prime}$
and $\langle\gamma,\gamma^{\prime}\rangle\in R$. The other direction is proven
similarly. From Definition 1, Definition 2, Definition 3, Definition 1 and
Equation 1, it is concluded that the defender’s observations are identical in
the initial states of both games, i.e., $\langle
s_{0},s^{\prime}_{0}\rangle\in R$.

Since a two-player security game is a zero-sum game, i.e., the players have
opposite objectives, an objective can be specified in terms of a single-player
strategies and ${\bowtie\in\\{\geq,>\\}}$ using the equivalences defined on
rPATL formulas (Simaitis, 2014). Hence, we focus on the maximization
strategies in the proof, i.e., $\bowtie\in\\{>,\geq\\}$.

###### Lemma 0.

Let $\pi=s_{1}a_{1}s_{2}\ldots a_{n-1}s_{n}$ be an attacker’s _maximal
unobservable path_ in an ODT security game, i.e.,
$s_{1}\overset{\top}{\Longrightarrow}s_{n}$. Let $\phi$ be an observable step-
unbounded defense objective. The formula $s_{j}\in\mathsf{Sat}(\phi)$ implies
$s_{j+1}\in\mathsf{Sat}(\phi)$, for all $1\leq j<n-1$.

Proof. The proof is done by structural induction on $\phi$.
Base Case According to Definition 1, each transition by the attacker leads to
setting a derived capability, i.e., it only gains a new unobservable
capability $e_{j}$ in each transition. Hence,

(5) $\mathcal{L}(s_{j+1})=\mathcal{L}(s_{j})\cup\\{e_{j}\\},1\leq j<n-1.$

where $e_{j}\in{V}_{A}\backslash{V}_{O}$. Since $\phi$ is a proposition
defined over ${V}_{O}\cup{V}_{D}$ according to Definition 2, it follows that
$s_{j}\in\mathsf{Sat}(\phi)$ implies $s_{j+1}\in\mathsf{Sat}(\phi)$, $1\leq
j\leq n$ based on Equation 5.
Inductive Step. If the formula is of the form $\neg\phi$ or
$\phi_{1}\wedge\phi_{2}$, the conclusion is trivially followed from the
inductive step hypothesis and the fact that if two formulas hold in a state,
their conjunction and negations will hold too. If it’s of the form ${\ll
C\gg\mathsf{P}_{\leq~{}q}[\phi_{1}\mathsf{U}\phi_{2}]}$, from the monotonocity
property of the value iteration (Condon, 1992), the formula
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j}}(\phi_{1}\mathsf{U}\phi_{2})\leq\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j+1}}(\phi_{1}\mathsf{U}\phi_{2})$
holds. Hence,
$q\leq\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j}}(\phi_{1}\mathsf{U}\phi_{2})$
implies
$q\leq\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j+1}}(\phi_{1}\mathsf{U}\phi_{2})$,
and subsequently according to the semantics of rPATL,
$s_{j}\in\mathsf{Sat}({\ll
C\gg\mathsf{P}_{\leq~{}q}[\phi_{1}\mathsf{U}\phi_{2}]})$ implies
$s_{j+1}\in\mathsf{Sat}{{(\ll
C\gg\mathsf{P}_{\leq~{}q}[\phi_{1}\mathsf{U}\phi_{2}]})}$.

###### Lemma 0.

Let $\Pi$ show the set of all attacker’s maximal unobservable paths from
${s_{1}\in S_{A}}$, $\phi_{1}$ and $\phi_{2}$ be two arbitrary observable
step-unbounded defense formulas and $s_{1}\in\mathsf{Sat}(\phi_{1})$ and
$s_{1}\notin\mathsf{Sat}(\phi_{2})$. It holds
${\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{1}}(\phi_{1}\mathsf{U}\phi_{2})=\underset{\pi\in\Pi,\pi=s_{1}a_{1}s_{2}\ldots
a_{n-1}s_{n}}{\min}~{}\overset{\Rightarrow}{\Delta}(\pi)}$ where

$\begin{array}[]{ll}\overset{\Rightarrow}{\Delta}(\pi)=&\Delta(s_{1},a_{1})(s_{2})\times\ldots\times\Delta(s_{n-1},a_{n-1})s_{n}\times\\\
&\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{n}}(\phi_{1}\mathsf{U}\phi_{2}).\end{array}$

Proof. From Lemma 4, it follows that $s_{1}\in\mathsf{Sat}(\phi_{1})$ implies
$s_{j}\in\mathsf{Sat}(\phi_{1})$, $1<j\leq n$ for all the traces $\pi\in\Pi$.
Hence, since $\phi_{1}\mathsf{U}\phi_{2}$ is an observable step-unbounded
defense objective formula (i.e., it does not change defender’s variables), it
is trivial to show that the fourth case of Equation 4 will hold for all the
states $s_{j}$ (excluding their last states) of the $\Pi$’s traces (with
$k=\infty$), $1<j\leq n$ and for all traces $\pi\in\Pi$. From the hypothesis
${V}_{AD}\subseteq{V}_{O}$ and Definition 1 (the attacker gains a new
capability in each attempt), we can conclude that there will be no loop in the
unobservable states, i.e., all traces in $\Pi$ will be finite. Therefore, the
conclusion is obviously followed from the definition of Equation 4 where
$opt=\min$.

###### Lemma 0.

Let $\phi$ be an observable step-unbounded defense objective. For any
arbitrary states $s\in S_{A}\cup S_{D}$ and $s^{\prime}\in S^{\prime}_{A}\cup
S^{\prime}_{D}$ that are weak bisimilar, i.e., $(s,s^{\prime})\in R$ where $R$
is a witnessing bisimulation relation between $\mathcal{G}$ and
$[\mathcal{G}]$. The formula $\mathcal{G},s\models\phi$ holds if and only if
$[\mathcal{G}],s^{\prime}\models\phi$ holds.

Proof. We prove this lemma by induction on the number of path operators in
$\phi$.
Base Case The formula $\phi$ is a propositional formula on
${V}_{O}\cup{V}_{D}$. From the definition of the witnessing relation (See the
proof of Theorem 3), we can conclude that $\phi\in\mathcal{L}(s)$ if and only
if $\phi\in\mathcal{L}(s^{\prime})$, i.e., $\mathcal{G},s\models\phi$ holds if
and only if $[\mathcal{G}],s^{\prime}\models\phi$ holds.
Inductive Step Assume that the conclusion holds for all the formulas
$\phi_{i}$ with $i$ operators of $\mathsf{P}$, $0\leq i\leq n$. We should
prove it for $n+1$, i.e., it should hold for all formulas $\phi_{m}$ with $m$
operators of $\mathsf{P}$, $0\leq m\leq n+1$. If $0\leq m\leq n$, the
conclusion follows from the inductive step hypothesis. For the case of
$m=n+1$, we perform a case analysis on $\phi_{m}$ (i.e., $\phi_{n+1}$). (Case
a) If $\phi_{m}=\neg\phi$, the proof is trivial. (Case b) If
$\phi_{m}=\phi_{i}\wedge\phi_{j}$ where $i+j=n+1$, (i) if $i\neq 0$ and $j\neq
0$, it trivially follows from the inductive step hypothesis and the fact that
if two formulas hold in a state, their conjunction holds as well, and (i) if
$i=0$ or $j=0$, then the proof is reduced to proving
${\ll{C}\gg}\mathsf{P}_{\bowtie~{}q}[\psi]$ or
${\langle\\!\langle{C}\rangle\\!\rangle}\mathsf{R}_{\bowtie\,x}[\mathsf{F}\phi]$
similar to Case c and d.

(Case c) If ${\ll{C}\gg}\mathsf{P}_{\bowtie~{}q}[\psi]$, since this formula
has $n+1$ number of path operators, it follows that the formula $\psi$ should
have $n$ path operators. As $\psi$ is an observable step-unbounded defense
objective, $\psi=\phi_{1}\mathsf{U}\phi_{2}$. We first prove the left-to-right
direction of this equivalence, i.e.,
${\mathcal{G},s\models\phi\implies[\mathcal{G}],s^{\prime}\models\phi}$. Since
$\mathcal{G},s\models{\ll{C}\gg}\mathsf{P}_{\bowtie~{}q}[\psi]$, this means
that there is at least a path $\pi=sa_{0}s_{0}a_{1}\ldots s_{n}$ in
$\mathcal{G}$ that follows a winning strategy and leads in satisfying this
property, i.e.,
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)=\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\\{\pi\\})$,
$q\bowtie\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\\{\pi\\})$ and
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)$.
We should show that there is a path $\pi^{\prime}$ in $[\mathcal{G}]$ such
that
$\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\\{\pi^{\prime}\\})$,
${(s,s^{\prime})\in R}$ and
$q\bowtie\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)$. We prove
this by induction on the number of $a_{i}$’s in $\pi$.

  * •

Base Case If $\pi=s$, we show that $\pi^{\prime}=s^{\prime}$. According to the
first inductive step hypothesis, $s=_{{V}_{O}\cup{V}_{D}}s^{\prime}$
(witnessing bisimulation relation) and Lemma 4, one of the first three cases
in Equation 4 should hold in both $s$ and $s^{\prime}$. Hence,
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)$
and subsequently $[\mathcal{G}],s^{\prime}\models\phi$ holds.

  * •

Inductive Step Let for all paths $\pi_{k}$ with the $k$ number of actions
where
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)=\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\\{\pi\\})$,
there is a path $\pi^{\prime}$ such that
$\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\\{\pi^{\prime}\\})$,
$q\bowtie\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)$ and
$[\mathcal{G}],s^{\prime}\models\phi$ holds. We should prove this for
$\pi_{k+1}=sa_{0}s_{0}a_{1}\ldots s_{k+1}$. Two cases can happen.

Case i If $s\in S_{D}$: Let $\pi_{0}=s_{0}a_{1}\ldots s_{k+1}$. Based on
Equation 4 and ${0<k}$, it is clear that
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{0}}(\psi)=\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{0}}(\\{\pi_{0}\\})$,
$q\bowtie\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{0}}(\psi)$ and
$\mathcal{G},s_{0}\models\phi$. From the inductive step hypothesis, there is a
path $\pi_{0}^{\prime}=s^{\prime}_{0}a^{\prime}_{1}\ldots s^{\prime}_{j}$ such
that $(s_{0},s^{\prime}_{0})\in R$,
${q\bowtie\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}_{0}}(\psi)}$ and
$[\mathcal{G}],s^{\prime}_{0}\models\phi$. From the definition of witnessing
bisimulation relation and the disjointness of the attacker and the defender’s
actions, it follows $s\in S_{D}\Leftrightarrow s^{\prime}\in S^{\prime}_{D}$
where $(s,s^{\prime})\in R$. According to the first inductive step hypothesis,
$s\in\mathsf{Sat}(\phi_{1})$ if and only if
$s^{\prime}\in\mathsf{Sat}(\phi_{1})$. Similarly for $\phi_{2}$. Hence, the
same case of Equation 4 holds for the states of $s$ and $s^{\prime}$, i.e.,
the fourth case. The outgoing transitions from $s$ and $s^{\prime}$ are the
same in the both games, as the defender is same in both games. Hence, we can
conclude from the inductive step hypothesis
($\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{0}}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}_{0}}(\psi)$),
the definition of weak bisimulation relation and Equation 4 that
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)={\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)}$,
i.e., $[\mathcal{G}],s^{\prime}\models\phi$

Case ii If ${s\in S_{A}}$: According to Lemma 5, there is a path
$\omega_{0}=s_{0}a_{0}s_{1}\ldots a_{j-1}s_{j}$ such that
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)=\underset{0\leq
i<j}{\Pi}\Delta(s_{i},a_{i})s_{i+1}\times\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j}}(\psi)$,
i.e., $\pi_{k+1}=\omega_{0}\omega_{1}$ and
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j}}(\psi)=\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j}}(\\{\omega_{1}\\})$.
From the inductive step hypothesis, it follows that there is a path
$\omega^{\prime}_{1}=s^{\prime}_{j}a_{j}\ldots$ such that
$\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}_{j}}(\psi)=\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{j}}(\\{\omega^{\prime}\\})$.
Since ${(s_{0},s^{\prime}_{0})\in R}$,
$\pi^{\prime}=s^{\prime}_{0}a\omega^{\prime}_{1}$ is a path of
$[\mathcal{G}]$. According to Algorithm 1, it follows that
$\Delta(s^{\prime}_{0},a)s^{\prime}_{j}=\underset{0\leq
i<j}{\Pi}\Delta(s_{i},a_{i})s_{i+1}$, i.e.,
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{0}}(\\{\pi\\})=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}_{0}}(\\{\pi^{\prime}\\})$,
and subsequently
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s_{0}}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}_{0}}(\psi)$
and $[\mathcal{G}],s_{0}^{\prime}\models\phi$.

The proof from right-to-left is done similarly.

(Case d) If
${\langle\\!\langle{C}\rangle\\!\rangle}\mathsf{R}_{\bowtie\,x}[\mathsf{F}\phi]$,
the proof is similar to that of
${\langle\\!\langle{C}\rangle\\!\rangle}\mathsf{P}_{\bowtie\,x}[\psi]$. Note
that the semantics of the $\mathsf{R}$ operator is defined based on
$\mathrm{Pr}^{\gamma_{1},\gamma_{2}}_{\mathcal{G},s}$ and the accumulated
reward of a path.

###  C. Proof of Theorem 4

Proof. A wining strategy is a function $\gamma:S_{D}\to\mathcal{P}_{S}$ that
determines the next move in each defender’s state $s$ based on its
observation. Let
$T=\\{t\in\Delta(s)~{}|~{}\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)\leq\mathrm{Pr}^{\max,\min}_{\mathcal{G},t}(\psi)\\}$.
Then, $\gamma(s)=[t_{1}\mapsto 1/n,t_{2}\mapsto 1/n,\ldots,t_{n}\mapsto 1/n]$
if $T\neq\emptyset$, otherwise, $\gamma(s)=[s_{1}\mapsto 1/m,s_{2}\mapsto
1/m,\ldots,s_{m}\mapsto 1/m]$ where $\Delta(s)=\\{s_{1},\ldots,s_{m}\\}$.
Informally, as long as the property holds, the defender will take the most
promising states that more likely lead to holding the property $\psi$. As soon
as the property is violated or satisfied, then it can randomly move. As shown
in Theorem 3, for any state $s\in S_{D}$,
$\mathrm{Pr}^{\max,\min}_{\mathcal{G},s}(\psi)=\mathrm{Pr}^{\max,\min}_{[\mathcal{G}],s^{\prime}}(\psi)$
where $(s,s^{\prime})\in R$. Hence, we can conclude that the synthesized
strategy will be identical in both cases, if the property is of the form
${\ll{C}\gg}\mathsf{P}_{\bowtie~{}q}[\psi]$. The proof for the case of
${\ll{C}\gg}\mathsf{R}_{\bowtie~{}q}[\mathsf{F}\phi]$ is similar.