# Impact Analysis of Coordinated Cyber-Physical Attacks via Statistical Model Checking: A Case Study

Ruggero Lanotte, Massimo Merro, Nicola Zannone

► To cite this version:

Ruggero Lanotte, Massimo Merro, Nicola Zannone. Impact Analysis of Coordinated Cyber-Physical
Attacks via Statistical Model Checking: A Case Study. 43th International Conference on Formal
Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2023, Lisbon, Portugal.
pp.75-94, 10.1007/978-3-031-35355-0_6. hal-04731929

HAL Id: hal-04731929

https://inria.hal.science/hal-04731929v1

Submitted on 11 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
<figure><img src="image_3.png" /></figure>

# Impact Analysis of Coordinated Cyber-Physical Attacks via Statistical Model Checking: A Case Study

Ruggero Lanotte<fnref n="1" />, Massimo Merro<fnref n="2" />✉, and Nicola Zannone<fnref n="3" />

**Abstract.** *Cyber-Physical Systems* are exposed to *cyber-physical attacks*, i.e., security breaches in cyberspace that alter the underlying physical processes.

We use UPPAAL SMC to analyze a non-trivial coordinated multi-engine system equipped with both a tamperproof distributed intrusion detection system (IDS) and a tamperproof supervisor component to mitigate eventual loss of performance. We rely on *statistical model checking* to evaluate the impact of three *coordinated cyber-physical attacks* injecting malicious code in all controllers of the multi-engine system to compromise the performance of the whole system. Here, the coordination of the attackers is a necessary requirement to achieve the desired malicious goals. Our security analysis provides an estimate of both the *physical impact* of the attacks on the physical process of the system and the *effectiveness* of the IDS. We believe that by assessing the impact of attacks, system engineers may understand whether they have to develop more accurate impact metrics or focus on different invariants to enhance their IDSs in order to detect such attacks.

**Keywords:** Cyber-physical attack · Security analysis · Statistical model checking

## 1 Introduction

*Cyber-Physical Systems* (CPSs) integrate networking and distributed computing systems with physical processes. Applications include automation, smart cities, medical systems, agriculture, and in particular safety-critical applications such as electric power generation and distribution, nuclear power production, and water supply.

As industrial organizations are increasingly connecting their operational technology (OT) network with the corporate networks to improve business and operational efficiency, CPSs are more and more exposed to *cyber-physical attacks* [16], i.e., security threats in cyberspace that adversely affect the physical processes.

<footnote n="1">¹ Università dell'Insubria, Como, Italy
ruggero.lanotte@uninsubria.it</footnote>

<footnote n="2">² Università degli Studi di Verona, Verona, Italy
massimo.merro@univr.it.it</footnote>

<footnote n="3">³ Eindhoven University of Technology, Eindhoven, The Netherlands</footnote>
According to Gollmann et al. [10], the possible goals of cyber-physical attacks can be classified into three main groups: (i) equipment damage, such as over-stress of equipment, to reduce their expected life cycle, or violation of safety limits; (ii) production damage, in order to compromise product quality, product rate or operating costs; (iii) compliance violations, such as increasing of environmental pollution. To achieve these goals, cyber-physical attacks can tamper with both the physical and the cyber layer to bring the system into a state desired by the attacker. In particular, they may manipulate sensor measurements and/or actuator commands.

Recent years have seen the emergence of coordinated cyber-physical attacks, i.e., attacks that need to coordinate and possibly collaborate with each other via some (possibly) covert channel to achieve the desired malicious goals, involving different components of the target CPS. These attacks can cause more severe consequences than single cyber-physical attacks, such as disruption of the plant and cascading failures, and can mask manipulations of physical processes. Although a large body of research has investigated defense mechanisms to protect CPSs against (coordinated) cyber-physical attacks [13,35], there is still little understanding of the potential impact of such kind of attacks on the physical processes. In general, we believe that by assessing the impact of attacks on the physical process, system engineers may better understand whether they have to develop more accurate impact metrics [22, 24, 30, 32] or focus on different invariants to enhance their IDSs in order to detect such attacks, possibly at an early stage.

To perform a systematic impact assessment of cyber-physical attacks on CPSs, we need tool-supported methods for the safety verification of CPSs. One of the central problems in the safety verification of CPSs is the reachability problem: can an unsafe state be reached by an execution of the system (possibly under attack) starting from a given initial state? In general, the reachability problem for hybrid systems (and CPSs) is stubbornly undecidable; although decidability has been proven for specific classes of systems (see, e.g., [1, 14, 20]). However, even when decidable, the exhaustive verification of hybrid systems based on model checking techniques often relies on non-polynomial algorithms, leading to the well-known state explosion problem.

Statistical Model Checking (SMC) [25] is a technique combining model checking [7] with the classical Monte Carlo simulation [12], aiming at providing support for quantitative analysis, as well as addressing the size barrier, to allow the analysis of large models such as CPSs [8]. Unlike model checking, statistical model checking does not guarantee a 100% correct analysis but allows us to bind the error of the analysis. In this work, we apply UPPAAL SMC [9], the statistical extension of the UPPAAL model checker [3], to support the composition of timed and/or probabilistic automata.

In UPPAAL SMC, two statistical parameters $\alpha$ and $\epsilon$, lying in the real interval [0, 1], must be specified by the user to fix the maximum probability of false negatives and probabilistic uncertainty, respectively. The number of runs that the simulator must perform to guarantee the level of required precision depends on both $\alpha$ and $\epsilon$, and it is computed using ad-hoc statistical techniques [25]. UPPAAL SMC returns a confidence interval $[p-\epsilon, p+\epsilon]$, in which $p$ is the probability to satisfy the checked property.
**Contribution:** This work aims to investigate formal methodologies to statically analyze the impact of *coordinated cyber-physical attacks* on both the underlying physical process and invariant-based intrusion detection systems. In particular, we use UPPAAL SMC to analyze the *robustness* of a proposed non-trivial *coordinated multi-engine* system equipped with both a tamperproof distributed intrusion detection system (IDS) and a tamperproof supervisor component to mitigate the eventual loss of performance via load balancing. Each engine of the system is equipped with a cooling system to maintain the working temperature of the engine within a specific range. Each engine is also equipped with a local IDS that checks whether the activity of the cooling system is consistent with the engine temperature. Eventual violations of these safety invariants are notified to a central IDS, which tries to detect coordinated cyber-physical attacks targeting more engines at the same time.

We rely on *statistical model checking* as a methodology for achieving a security analysis of our coordinated multi-engine system. We have evaluated the *physical impact* [24,31] of three carefully chosen *coordinated cyber-physical attacks* injecting malicious code in all controllers of our multi-engine system to achieve *production damage* and/or *equipment damage*. We actually verified two families of *system invariants* of the system under attack: one focused on the runtime evolution of the physical-components of the CPS, and a second one focused on the effectiveness of the IDS in detecting the proposed attacks.

The verification of our multi-engine system under attack, i.e., the effectiveness of the distributed IDS and the physical impact of the attacks, was performed within a reasonable time, showing the potential for our analysis to handle the analysis of larger systems.

**Outline:** The remainder of the paper is structured as follows. Next section introduces our coordinated multi-engine system. Section 3 presents its implementation and verification in UPPAAL SMC, and Sect. 4 presents its security analysis. Finally, Sect. 5 discusses related work and concludes the paper by providing directions for future work.

## 2 A Coordinated and Refrigerated Multi-engine System

As a case study, we propose a *coordinated multi-engine system* consisting of *n* refrigerated engines, *Eng*<sup>i</sup>, interacting with both a supervisory component and a distributed IDS. The supervisory component aims to optimize the performance of the whole engine system, whereas the distributed IDS is devoted to detecting *coordinated attacks*, i.e., attacks that tamper with more than one component of the multi-engine system at the same time.

Each engine comprises a cooling system and is characterized by three system variables: (i) a physical variable *temp* recording the temperature of the engine, with initial value 95; (ii) a control variable *cool* indicating whether the cooling system is on or off, with initial value off; (iii) a control variable *speed* indicating the engine speed, with values ranging in the set {slow, half, full}; in normal conditions all engines run at half speed.
The runtime evolution of the temperature of each engine depends on the current state of the two control variables. When the cooling system is active (cool = on), the temperature decreases according to the differential equation $temp' = -r$, where r is uniformly chosen in one of the following real intervals: (a) [0.8, 1], if speed = slow; (b) [0.4, 0.5], if speed = half; (c) [0.2, 0.4], if speed = full. When the cooling system is inactive (cool = off), the temperature increases according to the differential equation $temp' = r$, where r is uniformly chosen in one of the following real intervals: (a) [0.1, 0.2], if speed = slow; (b) [0.3, 0.5], if speed = half; (c) [0.8, 1], if speed = full.

Each engine also comprises two *logical components*: a controller, *Ctrl*, and a *local intrusion detection system, L-IDS*. The controller maintains the temperature within a specific range by means of a cooling system. At each scan cycle, *Ctrl* checks the temperature of its engine. When the sensed temperature is above 100 degrees, the controller activates the cooling system; the cooling activity is maintained for 20 consecutive time instants. If the temperature is not above 100 degrees, the controller turns off the cooling system. In both cases, before restarting its scan cycle, the controller waits for instructions from the supervisor to change the speed of the engine.

The local IDS, *L-IDS*, is in charge of checking specific *system invariants* representing system anomalies. Specifically, the *L-IDS* checks whether: (i) the cooling system is active when the temperature is above 101 degrees and (ii) the cooling system is off when the temperature is below 80 degrees. If these invariants are violated, it triggers a warning signaling overheating or underheating at its engine. Note that, for the sake of simplicity, the intrusion detection system employed is quite basic; it is straightforward to extend it to support more informative tests on process variables and/or on control variables.

The multi-engine system comprises two centralized logical components: a *central IDS (C-IDS)* and a *Supervisor*. The *C-IDS* rises an alarm when at least two different *L-IDSs* signal the violation of their invariants. The Supervisor tries to *mitigate* the effects of system anomalies as follows: when an engine is overheating (resp. under-heating), it asks the associated controller to slow down the engine speed (resp. to run at FULL speed); then, the Supervisor requires an adjacent engine to run at FULL (resp. SLOW) speed to compensate the performance of the whole multi-engine system. When the overheating/under-heating anomaly is resolved, it asks the involved controllers to reset its engine at half power. Note that system engineers may require engines not involved in the compensation process (i.e., they are running at half speed) to run at FULL/LOW speed. However, requests for work compensation or speed changes may be accepted or not, depending on whether the engine receiving the request is in condition to run at the required speed; in particular, mitigation activities have priority over system engineers' requests. The pseudocode of all logical components is provided in Fig. 1 and Fig. 2.

A simulation of the temperature evolution of a multi-engine system composed by three engines is given in Fig. 3. Note that the different behavior of one engine in the first part of the graph is due to a LOW request of the system engineer. In
Ctrl: if (cooling == false)
{read temp(x);
  if (x > 100)
    {cooling := true;
      cnt := 0;
      write cool(on)}
  else {write cool(off)}
}
else
{
  cnt := cnt + 1;
  write cool(on);
  if (cnt == 5) {cooling := false}
};
receive instruction(z);
write speed(z);
goto Ctrl

L-IDS: read temp(t);
read cool(cooling);
if (t > 101 and cooling = off)
{send status_hot} //overheating warning
ELSEIF (t < 90 and cooling = on)
{send status_cold} //under-heating warning
ELSE
{send status_ok}; //temperature okay
goto L-IDS

<caption>Fig. 1. Local logical components</caption>

Sup: for each local IDS
{receive status of the associated controller};
read system engineers' requests for controllers;
for each controller c
{compute its speed, speed_c, according to
its status and engineers' requests};
for each controller c
{send instruction speed_c};
goto Sup

C-IDS: for each local IDS
{receive status of the associated controller};
if (there are at least 2 engines with warnings)
{snd alarm}
ELSEIF (there is only 1 warning)
{snd warning}
ELSE
{snd okay};
goto C-IDS

<figure><img src="image_4.png" /><figcaption>Fig. 3. Runtime evolution of the temperatures of the multi-engine system with three engines</figcaption></figure>

that time window the engine slows down, its temperatures grows more slowly, and, as a consequence, its cooling system becomes more effective in cooling down the temperature.
## 3 An Implementation in UPPAAL SMC

In this section, we model and verify in UPPAAL SMC [9] the coordinated multi-engine system, presented in Sect. 2, consisting of three engines. The UPPAAL SMC models of our system and the attacks discussed in the next section are available at the repository https://github.com/ruggerolanotte/multi-engine_system.

**UPPAAL Representation.** As other cyber-physical use cases presented in the literature (see related work in Sect. 5), we modeled the coordinated multi-engine system by making a clear distinction between *physical components* (physical process, sensors and actuators), *logical components* (controllers and IDSs), and *communication channels* between logical components and between logical components and physical devices (sensors and actuators). In particular, we modeled both the physical components and the logical components in terms of *parallel timed automata*.

The physical component, also called plant, consists of three automata parameterized on the *id* of the corresponding engine: (i) the _Engine_ automaton, shown in Fig. 4, governs the runtime evolution of the temperature, variable *temp*[id],

<figure><img src="image_5.png" /><figcaption>Fig. 4. UPPAAL model of the engine</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 5. UPPAAL models of the physical devices (sensors and actuators)</figcaption></figure>
<figure><img src="image_7.png" /><figcaption>Fig. 6. UPPAAL models of the local logical components (Ctrl and L-IDS).</figcaption></figure>

by means of a function *heating*(); similarly, a *cooling*() function models the presence of the cooling system; (ii) the _Sensor_ automaton (see the left-hand-side of Fig. 5) updates the temperature measurements used by the controller and the local IDS; (iii) the _Actuator_ automaton (see the right-hand-side of Fig. 5) handles the two actuators associated with the cooling system and the engine speed, respectively. The physical component also includes a small automaton to synchronize both the controllers and the local IDSs with measurements coming from _Sensor_ (via a synchronization channel _stable-signals_).

The logical component of our model is given in Fig. 6. It consists of two automata, _Ctrl_ and _L_IDS_, modeling the controller and the local intrusion detection system, respectively (again, they are parametric on the *id* of the associated engine). _Ctrl_ waits for stable measurements, via a synchronization channel _stable-signals_, that are recorded in the local variables (*ctrl_sens*[*id*] and *ids_sens*[*id*], respectively). On the other hand, _L_IDS_ determines the status of the cooling system (hot, cold, okay) and sends it to both centralized logical components, the *Supervisor* and the *C-IDS*.

The two centralized logical components *C-IDS* and *Supervisor* are modeled by the automata _C_IDS_ and _Supervisor_, respectively (see Fig. 7 and Fig. 8). Both automata wait for information on the status of each engine from the local intrusion detection systems. Then: (i) _C_IDS_ does intrusion detection against coordinated attackers; (ii) _Supervisor_ writes the instructions to the controllers, according to the performance policy described before, using the function *decide_speed instr*().

We simulate system engineers' activities through an additional automaton modeling their requests to change the speed of the engines. An engineer can randomly choose one of the three engines and demand it to run in either FULL or SLOW speed (both cases with a 50% probability). Each request has a duration of 150 time units. The first request occurs in a time instant uniformly chosen in the interval [50, 100]. The other requests start after the end of the previous one in a time instant uniformly chosen in the interval [2500, 3000].
<figure><img src="image_8.png" /><figcaption>Fig. 7. UPPAAL model of the centralized IDS (C-IDS).</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Fig. 8. UPPAAL model of the Supervisor.</figcaption></figure>

**Verification of Our Multi-engine System.** As we are interested in studying the impact of cyber-physical attacks on our multi-engine system, our verification aims at ensuring the correct behavior of the IDS in the absence of attacks. Moreover, we are interested in characterizing the physical runtime behavior of the system. This information will be used in Sect. 4 as a baseline to study the physical impact of three different attacks.

*Settings.* We conducted our impact evaluation using a notebook with the following set-up: (i) 2.8 GHz Intel i7 7700 HQ, with 16 GB memory, and Linux Ubuntu 20.04 LTS OS; (ii) UPPAAL SMC model-checker 64-bit, version 4.1.26-2. The statistical parameters of false negatives ($\alpha$) and probabilistic uncertainty ($\epsilon$) are both set to 0.01, leading to a 99% accuracy. Note that these parameters only affect the accuracy of the results and the consequent time required for the analyses. Considering a lower accuracy would result in faster analyses. For our analysis, we simulate runs of our system that are 10,000 time units long. As the system consists of periodic sub-components (the single engines), the length of the run has been chosen long enough to observe several cycles of the system.

*System Analysis.* To verify the proper functioning of the IDS employed in our multi-engine system in the absence of attacks, we use UPPAAL SMC and model
the system behavior of interest as probability estimation queries of formulas of the form $\Diamond_{\le t} e_{prop}$, where $t$ is a time bound (in our case 10,000) and $e_{prop}$ is a side-effect free expression over variables. In practice, given a formula $\Diamond_{\le t} e_{prop}$, UPPAAL SMC returns a probability interval $[p_1, p_2]$ in which the property $e_{prop}$ holds in at least one time instant in 0..t. In the following, as we work with a 99% accuracy, we write that a property *holds with high probability* when UPPAAL SMC says that the property holds with a probability in the interval [0.980005, 1]. Similarly, we write that a property *does not hold with high probability* when UPPAAL SMC says that the property holds with a probability laying in the interval [0, 0.0199955].

In normal conditions, the intrusion detection system should not trigger any warning or alarm, i.e., it should not generate false positives. We formalize these properties in terms of probability estimation queries as follows:

$$ \mathbf{P1}: \Diamond_{\le t} (warning == 1) $$

$$ \mathbf{P2}: \Diamond_{\le t} (alarm == 1) $$

Intuitively, **P1** and **P2** returns the probabilities that a warning or an alert is triggered within time *t*, respectively. The analysis shows that our multi-engine system does yield neither warnings nor alarms. In particular, we verified that neither **P1** nor **P2** hold, with high probability, on runs of at most 10000 time instants. The verification of each property required approximately 40 minutes.

To study the *physical impact* of cyber-physical attacks on our multi-engine system, we focus on two specific physical target for attackers: (i) the increased activity of the cooling system with the consequent increase in coolant consumption, and (ii) modifications of the average temperatures of the engines. To derive this information, we use UPPAAL's *value estimation* queries $E[t; N](max : total\_var)$ by introducing two auxiliary variables: $total\_cooling[i]$ and $total\_temp[i]$, for $i \in \{0, 1, 2\}$. The integer variable $total\_cooling[i]$ counts the time instants in a run in which the cooling system of the engine *i* is active, whereas the double variable $total\_temp[i]$ returns the summation of the temperatures reached by the engine *i* in all time instants of a run. We use these variables to compute the average cooling time and temperature for a run.

By running 2000 execution traces, each consisting of 10000 time instants, we obtain the following information: (1) each engine spends, on average, around 47% of its time in cooling down the temperature; (2) the temperature of the three engines is, on average, around 95.5 degrees. Formally, these results are obtained using the following value estimations in UPPAAL SMC:

$$ \mathbf{E1}: E[\le 10000; 2000](max : \sum_{i \in \{0,1,2\}} total\_cooling[i]/3) = 4700.9 \pm 1.37. $$

$$ \mathbf{E2}: E[\le 10000; 2000](max : total\_temp[i]/10000) = 95.4554 \pm 0.0028, \text{ for } i \in \{0, 1, 2\}. $$

Here, "max : expr" returns for all 2000 simulation runs, the maximum value reached by the expression *expr*. The verification of each value estimation requires around 4 hours.

It is worth noting that value estimations are not associated with an accuracy but only provide an average of the estimated values over the tested runs along
with a graphical representation of the distribution of the real values computed for each run. Thus, to assess the quality of the estimated value with respect to all runs, we leveraged this information to verify a lower and an upper bound of the estimated value (extracted from its distribution of **E1** and **E2**) with an accuracy of 99%. To this end, we define the following two properties:

**P3:** $\Diamond_{\le 10000} (time==10000 \text{ and } \exists i \in \{0, 1, 2\}. \text{not}(4500 \le \text{total\_cooling}[i] \le 4900))$

**P4:** $\Diamond_{\le 10000} (time==10000 \text{ and } \exists i \in \{0, 1, 2\}. \text{not}(95 \le \text{total\_temp}[i]/10000 \le 96))$

The simulation of the multi-engine system for 10,000 runs shows that both properties do not hold with a high priority. Accordingly: (1) in each run, each engine spends at least 45% and at most 49% of its time in cooling down the temperature; (2) the temperature of each engine lays, on average, between 95 and 96 degrees. The verification of each of the queries above requires around 40 minutes.

# 4 An SMC-Based Security Analysis

In this section, we use UPPAAL SMC to perform a security analysis of the system under investigation when exposed to three different cyber-physical attacks aiming to cause *equipment* and/or *production damage* (cf. the attack goals seen in the Introduction). In particular, we implement three coordinated attacks consisting of (three) distinct distributed attackers, injecting malicious code in each controller of our multi-engine system. The distributed attackers coordinate with each other via a *covert channel* without introducing extra, possibly suspicious, communications between engines' controllers. Notice that we focus on attacks that compromise the controllers only (the automaton _Ctrl_ in our implementation), that is, we assume that the other logical components of the systems (local and central IDSs and Supervisor) have been secured against malicious attacks, and their runtime behavior cannot be altered by the attacker. To this end, we modeled the three attacks by replacing the automaton _Ctrl_ of each engine with a compromised version resulting from the attacker's injection. All attacks go through four phases: *waiting*, *starting*, *active* and *ended*. We assume that the attack duration is established a priori by the attacker, and that the exact time when the attack begins depends on some specific request of system engineers to change the speed of one or more engines.

We verify the system under attack in runs of 10000 time units. The time instant when the attack is triggered by the request of a system engineer is stored in a variable *start* whose value is randomly chosen in the time interval [50, 100]. Given the periodicity of our system, we chose an attack window of 9000 time units, covering several cycles. This choice provides us the possibility to observe eventual anomalies after the attack. Note that these attack time parameters, such as beginning of the attack and its duration, do not influence the outcome of the specific attacks and, thus, they are the same for all three attacks. The verification of each probabilistic estimation required at most 40 minutes and the computation of each value estimation around 4 h.
<figure><img src="image_10.png" /><figcaption>Fig. 9. Simulation of the multi-engine system exposed to Attack 1.</figcaption></figure>

## Attack 1: Degrading System Performance

*Objective.* The goal of the attacker is to compromise the performance of the multi-engine system by forcing the three engines to run at SLOW speed whenever a system engineer asks for higher performance by demanding an engine to switch from HALF to FULL speed. Accordingly, it can be seen as an attack aiming at *production damage*.

*Description.* Initially, the compromised multi-engine system behaves normally (the three attackers are in the *waiting phase*) until the system engineer demands a specific engine to run at FULL speed via the Supervisor. Upon receiving such a request, the associated attacker steps in the *starting phase* and performs a flooding/integrity attack on the *cool* actuator to induce an overheating for a few time instants. Thus, an overheating warning is transmitted by the local IDS to the Supervisor which sends instructions to the compromised engine controller to run at SLOW speed. At the same time, the attacker maintains that speed for the whole attack window via a flooding/integrity attack on the *speed* actuator (*active phase*). Furthermore, the Supervisor sends a request for compensation (FULL request) to the adjacent engine controller. This triggers the corresponding attacker to force the engine at SLOW speed. Note that Supervisor's requests are used as *covert channel* to propagate the attack to the whole multi-engine system.

In Fig. 9, we reports the temperature behavior of the three engines under attack. For the sake of visualization, the figure plots runs of 800 time units where the attack lasts 500 time units; note that the reported behavior is similar to the one that can be observed in the simulations used for our analysis. We can observe that in the time interval [90, 110], the three engines experience an overheating due to the beginning of the attack. Then, during the attack window, as the engines run at the SLOW speed, their temperatures grow more slowly. At the same time, their cooling systems are more effective in dropping their temperatures.
<figure><img src="image_11.png" /><figcaption>Fig. 10. UPPAAL automaton _Ctrl_ compromised by Attack 1.</figcaption></figure>

Therefore, when under attack, the engines exhibit a different (actually wider) periodic behavior.

The compromised controller of each engine is modeled by the automaton of Fig. 10. This automaton extends the one in Fig. 6 (left-hand side) by adding a variable *attack* to denote the different phases of the attack. In the *waiting phase*, the compromised controller behaves as the one in Fig. 6 while waiting for a trigger coming from system engineers or the Supervisor (bottom-left of Fig. 10). In the *starting phase* (top-right of Fig. 10), the flooding on the actuator *cool* is modeled by manipulating the communication between the controller and the actuator (via channel *cool_offCtrl*[id]) until the temperature exceeds the threshold of 103 °C, which triggers the intervention of the Supervisor (bottom-right of Fig. 10). Then, in the *active phase* the engine is maintained at SLOW speed via a similar flooding on the actuator *speed* (this time via channel *speed_slowCtrl*[id]) for the duration of the attack (bottom-left of Fig. 10). Finally, at the end of the attack window (top-left of Fig. 10), the controller restores its genuine behavior.

*Security Analysis.* We assessed the impact of the attack on the multi-engine system. First, we verified if the attack is successful in forcing the three engines to run at SLOW speed during the attack window, up to a short transitory initial phase necessary to propagate the attack to the three engines. To this end, we defined the following property:

$$ \Diamond_{\le 10000} (start + 150 \le time \le start + 90000 \text{ and } \exists i \in \{0, 1, 2\}. speed[i] != SLOW) $$ Intuitively, this property checks whether any of the three engines does not run at SLOW speed during the attack window. Our analysis shows that the property does not hold with high probability; thus, we can conclude that the attack was successful with high probability. Note that the attack propagation time is derived from an empirical observation of the attacked system's simulation graph, where 150 time units is a (safe) upper bound of the real propagation time.
To verify the stealthiness of the attack, we verified if properties **P1** and **P2** (cf. Sect. 3) hold when the system is under attack. Our verification shows that the central IDS does not fire any alarm (i.e., **P2** does not hold with high probability). However, some warnings were triggered by the local IDS as we observe that **P1** holds with high probability. An in-depth investigation showed that the warnings only happen in the initial transitory phase when the attack propagates throughout the multi-engine system. Formally, we verified that:

- $\Diamond_{\le 10000} (start \le time < start + 150 \text{ and } warning == 1)$ holds with high probability.

- $\Diamond_{\le 10000} (time < start \text{ and } time \ge start + 150 \text{ and } warning == 1)$ does not hold with high probability.

We also verified properties **P3** and **P4** to study the attack's impact on system performance. We observed that the average cooling time decreases to 17.5% (compared to 47% in the regular situation) and that the average temperature decreases to 91 (compared to 95.5 in the regular situation), showing that this attack has a limited impact on system performance.

## Attack 2: Putting the Multi-engine System Under Stress

*Objective.* The attacker aims to stress the multi-engine system by forcing the three engines to run at FULL speed whenever a system engineer asks an engine to switch from HALF to SLOW speed. Thus, the main goal is *equipment damage* as engines under stress are prone to ruptures in the long run; the attack also achieves *production damage* because running all engines at FULL power results in extra coolant consumption.

*Description.* Initially, the compromised multi-engine system behaves normally (the three attackers are in the *waiting phase*) until the system engineer demands a specific engine to run at SLOW speed via the Supervisor. Upon receiving such a request, the associated attacker steps in the *starting phase* and performs a flooding/integrity attack on the *cool* actuator to induce an under-heating for a few time instants. This results in a warning of the local IDS that triggers the Supervisor to instruct the engine to run at FULL speed. At the same time, the attacker maintains that speed for the whole attack window via a flooding/integrity attack on the *speed* actuator (*active phase*). Furthermore, the Supervisor sends a request for compensation (request for SLOW speed) to the adjacent controller. This triggers the corresponding attacker to force the engine at FULL speed. Again, the Supervisor's requests are used as covert channel to propagate the attack.

Figure 11 reports the evolution of the temperature for the three engines. Similarly to the previous attack, we illustrate the system behavior for a run of 800 time units where the system engineering randomly chose the SLOW (triggering) request in the interval [50, 100]; the attack lasts 500 units of time. We can observe that in the time interval [70, 180], the three engines experience an under-heating
<figure><img src="image_12.png" /><figcaption>Fig. 11. Simulation of the multi-engine system exposed to Attack 2.</figcaption></figure>

due to the beginning of the attack. Then, during the attack window, as the engines run at the FULL speed; thus, their temperatures grow more quickly and decrease more slowly. Again, when under attack, the engines exhibit a different (actually shorter) periodic behavior.

*Security Analysis.* We assessed the impact of the attack on the multi-engine system. First, we verified if the attack is successful in forcing the three engines to run at FULL speed during the attack, up to a short transitory initial phase (150 time units) necessary to propagate the attack to three engines. To this end, we defined the following property:

$\Diamond_{\le 10000} (start + 150 \le time \le start + 90000 \text{ and } \exists i \in \{0, 1, 2\}. speed[i]! = \text{FULL})$ Intuitively, this property checks whether any of the three engines does not run at FULL speed during the attack window. Our analysis shows that this property does not hold with high probability; thus, we can conclude that the attack was successful: all engines run at FULL speed during the attack window.

To verify the level of stealthiness of the attack, we verified if properties **P1** and **P2** (cf. Sect. 3) hold when the system is under attack. Our verification shows that the *central IDS* does not fire any alarm (i.e., **P2** does not hold with high probability). However, **P1** holds with high probability, indicating that the *local IDS* triggers some warnings. Further investigation showed that the warnings only happen in the initial transitory phase when the attack propagates throughout the multi-engine system. This insight is obtained by verifying the following properties:

- $\Diamond_{\le 10000} (start \le time < start + 150 \text{ and } warning == 1)$ holds with high probability.

- $\Diamond_{\le 10000} (time < start \text{ and } time \ge start + 150 \text{ and } warning == 1)$ does not hold with high probability.
We also studied the attack's impact on system performance using properties **P3** and **P4**. We observed that, on average, each engine spends 72% of its time cooling down the temperature (compared to 47% in the regular situation). Formally:

$$E[<= 10000; 2000](max: \sum_{i \in \{i=0,1,2\}} total\_cooling[i]/3) = 7221.45 \pm 0.264.$$

From this estimation, we can derive quantitative information on the increase of coolant consumption due to the attack: every engine spends at least 71% and at most 73% of its time in cooling down the temperature. We obtained this by observing that the following property does not hold with high probability:

$$\Diamond_{\le 10000} (time == 10000 \text{ and } \exists i \in \{0, 1, 2\} . \text{not}(7100 \le total\_cooling[i] \le 7300))$$

A similar analysis for the temperature shows the average temperature at each engine increased to 97 degrees (compared to 95.5 degrees obtained in the regular situation).

## Attack 3: Pushing the Multi-engine System to the Temperature Threshold

*Objective.* The attacker aims to keep the temperature of the engines close to the threshold, 100 degrees, when a system engineer asks for slowing down an engine. This is achieved by tampering with the cooling systems of all engines. Thus, the main goal of the attack is *equipment damage* as the engines work for a long period at a temperature very close to the threshold, with obvious consequences on its physical components in the long run.

*Description.* The attack proceeds as in Attack 2. The only difference is in the *active phase*, where each attacker, injected in the controller, reduces the duration of the cooling activity by deactivating the cooling system as soon as the temperature reaches 100 degrees.

Figure 12 shows a simulation of the system under attack. As for the previous attacks, we show a run of 800 time units where the system engineering randomly chose the SLOW (triggering) request in the interval [50, 100] and the attack lasts 500 time units. We can observe that in the time interval [60, 140], the three engines experience an under-heating due to the beginning of the attack. Then, during the attack window, as the engines run at the HALF (normal) speed; However, when under attack, the three engines all work at a temperature very close to the threshold of 100 °C.

*Security Analysis.* We assessed the impact of the attack on the multi-engine system. To verify if the attack is successful, we computed the value estimation of the temperature of each engine for the system under attack. These value estimations show that the temperature of the three engines is, on average, 99.25 degrees. Formally,

$$E[<= 10000; 2000](max: total\_temp[i]/10000) = 99.23 \pm 0.0002.$$
<figure><img src="image_13.png" /><figcaption>Fig. 12. Simulation of the multi-engine system exposed to Attack 3.</figcaption></figure>

From this estimation, we can determine that the attack is successful in increasing the average temperature of all engines. In particular, we observed that the following property does not hold with high probability:

$$ \diamond_{\le 10000} (time == 10000 \text{ and } \exists i \in \{0, 1, 2\}. \text{not}(98.8 \le \text{total\_temp}[i]/10000 \le 99.8)). $$

Therefore, the temperature of each engine lays, on average, between 98.8 and 99.8 degrees (instead of 95 and 96 degrees as in normal situations).

To verify the level of stealthiness of the attack, we verified if properties **P1** and **P2** (cf. Sect. 3) hold when the system is under attack. Similarly to the previous attacks, our verification shows that the *central IDS* does not fire any alarm (i.e., **P2** does not hold with high probability), but *local IDS* triggers some warnings (i.e., **P1** holds with high probability). As in the previous cases, the warnings only happen in the initial transitory phase when the attack propagates throughout the multi-engine system, as demonstrated by the following properties:

- $\diamond_{\le 10000} (start \le time < start + 150 \text{ and warning} == 1)$ holds with high probability.

- $\diamond_{\le 10000} (time < start \text{ and } time \ge start + 150 \text{ and warning} == 1)$ does not hold with high probability.

In this attack, the consumption of coolant remains unaffected, with the engine spending 47% of its time in cooling down the temperature.

## 5 Conclusions, Related and Future Work

We have used UPPAAL SMC [9] to perform statistical model checking of a coordinated and refrigerated multi-engine system enriched with a distributed intrusion detection system. As discussed in Lanotte et al. [23], SMC allows to better scale on the dimension of the CPS under security analysis, when compared
to the classical model checking tools. In particular, in prior unpublished work we implemented the refrigerated engine system at the core of our coordinated multi-engine system, using different model-checking tools, such as PRISM [19], UPPAAL [2], Real-Time Maude [27], and prohver, i.e., the safety model checker within the MODEST TOOLSET [11]. All these model-checking tools, however, suffer from the classical state explosion problem, even for relatively small systems. SMC enables a considerable step forward in the size of the CPSs we can verify.

Following this research line, the goal of this work was to test UPPAAL SMC as a tool for achieving a security analysis of a non-trivial CPS under attack. We have evaluated the physical impact of three carefully chosen coordinated cyber-physical attacks aiming at achieving production damages and/or equipment damages. In particular, we verified two families of system invariants of the system under attack: one focused on the runtime evolution of the physical-component of the CPS, and a second one focused on the effectiveness of the IDS (logical component) in detecting the proposed attacks. Here, the physical impact was measured in terms of changes in the average engine temperatures and the coolant consumption of the entire system. Many other physical invariants of our multi-engine could be checked similarly (number of activations/deactivations of the cooling system, efficiency of the engines, number of switches of the speed of each engine, etc.). Thus, we believe that our methodology can be easily generalized to any CPS under attack.

Our analysis provided us with insights into the effectiveness of the proposed distributed IDS and the impact of the attacks on the physical behavior of the system. In particular, we observed that the studied attacks are *stealthy*, as the IDS yields only some warning and no alarms, and are effective in achieving their goals. By assessing the impact of attacks on the physical process, system engineers may better understand whether they have to develop more accurate metrics or focus on different invariants to enhance their IDSs in order to detect such attacks, possibly at an early stage.

The modeling language provided by UPPAAL SMC has demonstrated to be effective in specifying realistic cyber-physical systems in terms of parallel timed automata. Such automata scale well and allowed us to represent cyber-physical attacks by focusing on specific compromised components. The time required for the analyses, with a 99% accuracy, was very reasonable: at most 40 min for each probabilistic estimation and around 4 h for each value estimation. To the best of our knowledge, this work is the first that studies the viability of UPPAAL SMC to perform security analyses of non-trivial CPSs exposed to coordinated cyber-physical attacks.

*Related Work.* Pedroza et al. [28] proposed a UML-based environment to model critical embedded systems. The verification of safety properties relies on UPPAAL, whereas the verification of security properties (e.g., confidentiality and integrity) relies on ProVerif [5]. Wardell et al. [33] proposed an approach for identifying security vulnerabilities of industrial control systems by modeling malicious attacks as PROMELA models. Kumar et al. [18] introduced an attack-fault tree formalism to describe attack scenarios; they conduct formal analyses using
UPPAAL SMC to obtain quantitative estimations on the impact of both system failures and security threats. Cheh et al. [6] used UPPAAL SMC to perform statistical model checking on a railway system to assess the safety of the system under attack. Similar to our work, they tied safety analyses to security analyses and considered an attack that manipulates the communication messages exchanged between the signaling components of the railway system (this affects the speed of the trains and the routes they take). More precisely, their attack can remove, insert, modify, or delay those network packets, akin to a Dolev-Yao attacker. Huang et al. [15] analyzed the impact of attacks compromising the safety of automotive systems. In particular, they considered attacks affecting vehicle communication: forgery of fake data, replay of old data, and spoofing of vehicle IDs. Both safety and security properties are verified in UPPAAL SMC. Taormina et al. [29] modeled the interaction between the physical and cyber layer of water distribution systems in epanetCPA, an open-source MATLAB toolbox allowing users to design custom cyber-physical attacks and simulate the hydraulic response of water networks. epanetCPA features a wide range of cyber-physical attacks: physical attacks on sensors and actuators, deception attacks, DoS on communication channels, replay attacks, and alteration of PLC and SCADA control statements. Although this tool can deal with several cyber-physical attacks, its analysis is based on single simulations. Lanotte et al. [21] used the safety checker *prohver* within the MODEST TOOLSET for the security analysis of a simple engine system with one physical variable, one sensor, and one actuator. Munteanu et al. [26] tested the effectiveness of the statistical model checker *modes* of the same toolset when doing a security and safety analysis of a significantly larger CPS. Jahandideh et al. [17] propose the Hybrid Rebeca language (an extension of the actor-based language Rebeca) to support the modeling of cyber-physical systems. The SpaceEx framework is used for reachability analysis. In particular, the authors show that event-based asynchronous models in Hybrid Rebeca improve the analysis by reducing the number of real variables and increase modularity. More recently, Zarneshan et al. [34] use Timed Rebecca to validate the interactions among the timing properties of components in inter-operable medical systems. More recently, Bernardeschi et al. [4] have proposed a formal methodology to validate the design of drone co-operative systems based on co-simulation and formal verification. The methodology relies on the Proto-type Verification System, an interactive theorem prover based on a higher-order logic language, and the Functional Mock-up Interface.

*Future Work.* As future work, we aim to stress the scalability of our SMC analysis by increasing the number of engines involved in our multi-engine system. Moreover, we plan to replicate and test more complex coordinated cyber-physical attacks targeting CPS controllers [13,35]. We believe that our work poses the basis for the design and development of detection mechanisms that leverage an understanding of the impact of cyber-physical attacks. We plan to investigate how our methodology can be extended to assist system engineers in devising tailored impact metrics and in identifying system invariants to enhance IDSs to detect cyber-physical attacks, possibly at their early stage.
**Acknowledgments.** We thank the reviewers for their insightful feedback.

## References

1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183-235 (1994)

2. Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST 2006, pp. 125-126. IEEE Computer Society (2006)

3. Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200-236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

4. Bernardeschi, C., Domenici, A., Fagiolini, A., Palmieri, M.: Co-simulation and formal verification of co-operative drone control with logic-based specifications. Comput. J. 66(2), 295-317 (2023)

5. Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363-434 (2009)

6. Cheh, C., Fawaz, A., Noureddine, M.A., Chen, B., Temple, W.G., Sanders, W.H.: Determining tolerable attack surfaces that preserves safety of cyber-physical systems. In: PRDC, pp. 125-134. IEEE Computer Society (2018)

7. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)

8. Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1-12. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_1

9. David, A., Larsen, K.G., Legay, A., Mikuäionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397-415 (2015)

10. Gollmann, D., Gurikov, P., Isakov, A., Krotofil, M., Larsen, J., Winnicki, A.: Cyber-physical systems security: experimental analysis of a vinyl acetate monomer plant. In: ACM CCPS, pp. 1-12 (2015)

11. Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593-598. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_51

12. Hastings, W.K.: Monte carlo sampling methods using markov chains and their applications. Biometrika 57(1), 97-109 (1970)

13. He, H., Yan, J.: Cyber-physical attacks and defences in the smart grid: a survey. IET Cyber-Phys. Syst. Theor. Appl. 1(1), 13-27 (2016)

14. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What's decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94-124 (1998)

15. Huang, L., Kang, E.-Y.: Formal verification of safety & security related timing constraints for a cooperative automotive system. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 210-227. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_12

16. Huang, Y., Cárdenas, A.A., Amin, S., Lin, Z., Tsai, H., Sastry, S.: Understanding the physical and economic consequences of attacks on control systems. Int. J. Crit. Infrastructure Prot. 2(3), 73-83 (2009)

17. Jahandideh, I., Ghassemi, F., Sirjani, M.: An actor-based framework for asynchronous event-based cyber-physical systems. Softw. Syst. Model. 20(3), 641-665 (2021). https://doi.org/10.1007/s10270-021-00877-y
18. Kumar, R., Stoelinga, M.: Quantitative security and safety analysis with attack-fault trees. In: HASE, pp. 25–32. IEEE Computer Society (2017)

19. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

20. Lanotte, R., Merro, M., Mogavero, F.: On the decidability of linear bounded periodic cyber-physical systems. In: HSCC, pp. 87–98. ACM (2019)

21. Lanotte, R., Merro, M., Munteanu, A.: A modest security analysis of cyber-physical systems: a case study. In: Baier, C., Caires, L. (eds.) FORTE 2018. LNCS, vol. 10854, pp. 58–78. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92612-4_4

22. Lanotte, R., Merro, M., Munteanu, A., Tini, S.: Formal impact metrics for cyber-physical attacks. In: CSF, pp. 1–16. IEEE (2021)

23. Lanotte, R., Merro, M., Munteanu, A., Viganò, L.: A formal approach to physics-based attacks in cyber-physical systems. ACM Trans. Priv. Secur. 23(1), 3:1–3:41 (2020)

24. Lanotte, R., Merro, M., Tini, S.: Towards a formal notion of impact metric for cyber-physical attacks. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 296–315. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_17

25. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_11

26. Munteanu, A., Pasqua, M., Merro, M.: Impact analysis of cyber-physical attacks on a water tank system via statistical model checking. In: FormaliSE@ICSE 2020, pp. 34–43. ACM (2020)

27. Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time maude. Higher-Order Symbolic Comput. 20(1–2), 161–196 (2007)

28. Pedroza, G., Apvrille, L., Knorreck, D.: AVATAR: a SysML environment for the formal verification of safety and security properties. In: NOTERE, pp. 1–10. IEEE (2011)

29. Taormina, R., Galelli, S., Douglas, H., Tippenhauer, N., Salomons, E., Ostfeld, A.: A toolbox for assessing the impacts of cyber-physical attacks on water distribution systems. Environ. Model. Softw. 112, 46–51 (2019)

30. Umsonst, D., Sandberg, H., Cárdenas, A.A.: Security analysis of control system anomaly detectors. In: ACC, pp. 5500–5506. IEEE (2017)

31. Urbina, D.I., et al.: Limiting the impact of stealthy attacks on industrial control systems. In: ACM CCS, pp. 1092–1105. ACM (2016)

32. Urbina, D.I., et al.: Limiting the impact of stealthy attacks on industrial control systems. In: CCS, pp. 1092–1105. ACM (2016). https://doi.org/10.1145/2976749.2978388

33. Wardell, D.C., Mills, R.F., Peterson, G.L., Oxley, M.E.: A method for revealing and addressing security vulnerabilities in cyber-physical systems by modeling malicious agent interactions with formal verification. Procedia Com. Sc. 95, 24–31 (2016)

34. Zarneshan, M., Ghassemi, F., Khamespanah, E., Sirjani, M., Hatcliff, J.: Specification and verification of timing properties in interoperable medical systems. Log. Methods Comput. Sci. 18(2), 13:1–13:37 (2022)

35. Zhang, H., Liu, B., Wu, H.: Smart grid cyber-physical attack and defense: a review. IEEE Access 9, 29641–29659 (2021)