# Threat Modelling and Beyond-Novel Approaches to Cyber Secure the Smart Energy System
## 7 Risk Analysis Using Formal Methods
### Formal Methods Overview  
Formal verification relies on a diverse set of mathematical and logical methods. These methods can be used to check different parts of a system, including the functional correctness of implementations, programming bugs, hardware Trojans, and security properties, and they can provide both a qualitative and quantitative analysis [63; 64; 65; 66]. A survey of probabilistic model checking, including the main probabilistic models, algorithms and abstraction techniques is given in [67], while more details can also be found in [68; 69]. In general, there are several different formalisms with difference in the notion of time. Those formalisms can be either non-deterministic or deterministic. When it comes to the notion of time, discrete-time models and continuous-time models have to be distinguished. The basic probabilistic model is the discrete-time Markov chain (DTMC), a deterministic model for discrete time. Its continuous version is called continuous-time Markov chain (CTMC). The Markov decision process (MDP) extends the discrete-time Markov chain with non-determinism. Similarly, its continuous version is called continuous-time Markov decision process (CTMDP). Originally, the MDP was \begin{table}
\begin{tabular}{l l c} \hline \hline
**Threat Id** & **Title** & **Expl. Prob.** \\ \hline
857 & Elevation by changing the execution flow in DCU & 0.57 \\
880 & Spoofing the in-house display external entity & 0.68 \\
903 & An adversary may block access to the application or API hosted on in-house display & 0.65 \\  & through a denial of service attack & \\ \hline \hline \end{tabular}
\end{table} 
Table 4: UC2 Exploitation probabilities. \begin{table}
\begin{tabular}{l l} \hline \hline
**Threat Id** & **Title** & **Expl. Prob.** \\ \hline
51 & Elevation by changing the execution flow in WAMS & 0.59 \\
187 & PQM may be subject to elevation of privilege using remote code execution & 0.59 \\
230 & Data flow MODBUS TCP IP secure is potentially interrupted & 0.75 \\
353 & Data flow IEEE C37.118 over IEC 61850-8-1 is potentially interrupted & 0.75 \\
478 & Data flow IEEE C37.118 over IEC 61850-8-1 is potentially interrupted & 0.75 \\
593 & Data flow MODBUS TCP IP secure is potentially interrupted & 0.75 \\
618 & Data flow IEC 60870-5-104 is potentially interrupted & 0.65 \\
621 & Elevation by changing the execution flow in RTU & 0.59 \\
640 & Data flowing sniffing across MODBUS TCP IP & 0.53 \\
647 & Elevation by changing the execution flow in PED & 0.57 \\
661 & Elevation by changing the execution flow in SCADA system & 0.64 \\
672 & Data flow IEC 60870-5-104 is potentially interrupted & 0.65 \\
686 & Elevation by changing the execution flow in RTU & 0.59 \\
1052 & Elevation by changing the execution flow in PMU & 0.59 \\
1057 & Data flow sniffing & 0.53 \\ \hline \hline \end{tabular}
\end{table} 
Table 5: UC3 Exploitation probabilities. introduced as probabilistic automata (PA). MDP and PA are very similar, with the small difference, that PA allows internal non-determinism, while MDP does not. Probabilistic timed automata (PTA) can be considered as MDP with clock variables. The final probabilistic model, Markov Automata (MA), is a generalization of interactive Markov chains and MDPs, and it is able to express discrete randomness. The selection of probabilistic model depends on the nature of modeled system and processes. There is a variety of formal verification tools available, covering different aspects. While classic verification gives answers to questions such as \"Will a given assertion ever be violated?\", and focus on _qualitative properties_, the evaluation of dependability aspects such as, e.g., reliability, availability and performance need a focus on _quantitative_ properties and models, including probabilistic behavior and real-time aspects [70]. An extensive overview of quantitative verification, including its different formalisms, modeling languages, properties and verification approaches is given in [70].