Abdelaziz Khaled
email: abdelaziz.khaled@evina.fr

Samir Ouchani
email: souchani@cesi.fr

Zahir Tari
email: zahir.tari@rmit.edu.au

Khalil Drira
email: khalil@laas.fr

Evina

Assessing the Severity of Smart Attacks in Industrial Cyber Physical Systems

Keywords: CPS, Smart Attacks, Cyber-Security, Formal methods, Artificial intelligence, Knowledge, Probabilistic Verification, Countermeasures, Reinforcement Learning, Multi-criteria Selection

Industrial cyber-physical systems (ICPS) are heterogeneous inter-operating parts that can be physical, technical, networking, and even social like agent operators. Incrementally, they perform a central role in critical and industrial infrastructures, governmental, and personal daily life. Especially with the Industry 4.0 revolution, they became more dependent on the connectivity by supporting novel communication and distance control functionalities, which expand their attack surfaces that result in a high risk for cyber-attacks. Furthermore, regarding physical and social constraints, they may push up new classes of security breaches that might result n serious economic damages. Thus, designing a secure ICPS is a complex task since this needs to guarantee security and harmonize the functionalities between the various parts that interact with different technologies. This paper highlights the significance of cyber-security infrastructure and shows how to evaluate, prevent, and mitigate ICPS-based cyber-attacks. We carried out this objective by establishing an adequate semantics for ICPS's entities and their composition, which includes social actors that act differently than mobile robots and automated processes. This paper also provides the feasible attacks generated by a reinforcement learning mechanism based on multiple criteria that selects both appropriate actions for each ICPS component and the possible countermeasures for mitigation. To efficiently analyze ICPS's security, we proposed a model checking based framework that relies on a set of predefined attacks from where the security requirements are used to assess how well the model is secure. Finally, to show the effectiveness of the proposed solution, we model, analyze, and evaluate the ICPS security on two real use cases.

Introduction

With the immense connectivity and full automation provided by Industry 4.0, we witness an exponential expansion in the development and deployment of Cyber-Physical Systems (CPS) [3] in various critical domains. From the existing variety of CPS, we focus mainly on Industrial Cyber-Physical Systems (ICPS) that are an integration of computation, networking, industrial and physical processes, and social actors as agents. Nowadays, ICPS are playing progressively an important role in more critical infrastructure, governmental, and everyday life system (e.g. water distribution system, health-care systems, electrical power grids, oil and natural gas distribution, household appliances, transportation systems, etc.) [START_REF] Gaddadevara | Cyber-Physical Systems: A Computational Perspective[END_REF]3]. Theoretically, they are expected to be immune against all cyber-attacks and to be free of vulnerabilities, which is practically difficult in daily real-life systems.

To build a more efficient, stable and robust ICPS, many features like computation, communication, and control are integrated while security is not appropriately tackled [START_REF] Sabaliauskaite | Aligning cyber-physical system safety and security[END_REF]4]; especially one of the fundamental issues is the heterogeneity between ICPS entities while they have a variation of components with different aspects connected in many ways. For example, hardware components can be sensors, embedded systems, and actuators. Further, they might cover also different chain tools of software for monitoring and control. Or either physical components like motors, tracks, tanks, etc. By relying on attack surface that is defined as a subset of resources that an attacker can exploit [START_REF] Ouchani | Generating attacks in sysml activity diagrams by detecting attack surfaces[END_REF], each component and its integration might increase the attack surface of an ICPS; and consequently contributing to the success of such an attack. Understanding the current ICPS security trends, including vulnerabilities and weaknesses, attacks and mitigation mechanisms could provide a deeper understanding of the existing security disposition and challenges of ICPSs. ICPSs are generally distributed across a wide range of distant geographic areas, they therefore collect a huge amount of non-formatted messages and data for analysis and decision making. Based on the collected information, the decisions rely generally on sophisticated machine learning (ML) techniques, which are known to consume more (execution) time and memory. Accordingly, breaches in the information collection step could harm a wide-scale data of distinct sensitivity level, and these can occur during the different stages of the system's operations (e.g. data collection and extraction, transmission and processing, storage).

Unfortunately, most of the existing ICPS design methodologies do not consider data protection, especially the complexity of ICPSs and the heterogeneity of its components complicate security hardening and privacy protection [START_REF] Sabaliauskaite | Aligning cyber-physical system safety and security[END_REF]4]. In particular, with the complexity of ICPS design, threats and vulnerabilities become more difficult to detect/assess/etc as the ICPS environment is highly dynamic and new security threats may stem easily. Additionally, it is also hard to check, identify, and trace attacks, which may originate from one or more sources. One should be able to point out ICPS's loopholes that make them vulnerable to different attacks and therefor devise appropriate methods to defend against them. Further, we believe that the evaluation of ICPS's security throughout their life cycle is a necessary step to guarantee their security when deployed.

This work describes the SSA-ICPS framework 1 which can be used to assess the severity of attacks in industrial cyber physical systems (ICPS) by covering the following three parts: (1) modeling, (2) analysis, and (3) mitigation. First, the modeling part implements a flexible and extensible library of a predefined templates of the ICPS architectures and components, as well as a variety of the used communication protocols. In addition, it models smart attacks retailed to each ICPS's component. These attacks are powerful and smart as they rely on reinforcement learning that maximizes the reward (with an optimal policy search) as well as selects appropriate actions given a set of criteria. Further, SSA-ICPS models ICPS's behaviour where a developer selects a proper ICPS architecture and later refines its components behaviour following a well-guided predefined syntax. The library covers a set of predefined security requirements, which are needed to be satisfied on ICPS as well as a set of countermeasures, to recover or reinforce the system when needed. The analysis part forms initially a malicious environment by instantiating then composing the potential attacks within the modeled ICPS. Then, it instantiates the security properties needed to be satisfied on the composed environment (ICPS/attacks). To overcome the analysis complexity, SSA-ICPS relies on the probabilistic model checking PRISM that helps to rapidly find the possible attack scenarios as well as to measure the severity of the succeeded ones. Finally, the mitigation procedure reinforces the ICPS model using a recommendation process that selects the appropriate countermeasures configuration to be deployed for the identified/detected attacks.

The main contributions of this paper can be summarised as follows.

• ICPS architecture that defines the main components of ICPS by covering: the social aspect of actors, hardware (sensors, etc), software (applications, web services, etc), and physical components (infrastructures, motors, etc). Also, the architecture defines the way of how each component communicates, interacts, and is composed with others.

• ICPS semantics that models the architecture in a process algebra formalism by capturing the underlying of ICPS components, their behaviours, as well as their composition operators.

• The ICPS requirements that express in Probabilistic Computation Tree Logic (PCTL) formula the set of functional and security properties needed to check and reinforce ICPS.

• A security analysis technique based on probabilistic verification that transforms the ICPS model into the PRISM input language.

• A library of attacks related to the different aspects of components carried by the ICPS architecture. Each attack maximizes its rewards by using reinforcement learning and selects appropriate actions through the use of a multi selection criteria algorithm.

• A library of countermeasures that match the different attack scenarios.

• A mitigation mechanism that recovers and reinforces the modeled ICPS from attacks.

The next section surveys existing solutions, and Section 3 provides details of the proposed security assessment framework. Section 4 discusses the experimental results, and finally we conclude this paper in Section 5.

Related work

This section reviews and discusses approaches that deal with modeling, functional analysis, and security specification techniques, as well as the communication protocols for ICPS.

Cheh et al. [6] analyzed the safety of railway systems corresponding to different classes of venomous actors based on to their abilities defined in the system access control. Initially, they constructed a hybrid automata that models a railway system, where each attack capability is defined as a pattern that represents its effects when appended to a component in the system. This combination describes the system behaviour and the possible actions of an attacker that might be executed. Then, they used a statistical model checking to assess the safety of the system for various input configurations of railways. Chen et al. [7] studied the detectability of data deception in CPS by assuming that an attack detector has access to a linear function of the initial system state and it cannot be changed by an attacker. In this context, the attack has the power to be undetectable by any dynamic attack detector under any specific constraints. The attacks are characterized to be maintained arbitrarily for long periods without being detected. Initially, they defined the zero state by inducing only the attacks that remain dynamically undetectable regardless the available information to the attack detector at the initial state. Cheh et al. [6] and Chen et al. [7] consider attacks that are initiated when the system starts the execution without showing the impact of each attack action on the behaviour of the system functionality. Further, they do not consider how to overcome them.

Bakirtzis et al. [5] proposed to evaluate the security level of CPS at each step of their life cycle development with the focus on deploying and operating safety-critical applications. To allow the analysis of vulnerabilities before deployment, they defined a taxonomy of attributes, which is a generalized schema that can capture mainly the characteristics of a safety-critical application. Then, they proposed to cover the maximum space of attack vectors associated with the model. Thus, the possible attack vectors are matched in order to mitigate them at the design level using SysML. Linzini et al. [START_REF] Lenzini | Security analysis of sociotechnical physical systems[END_REF] proposed a framework to check and evaluate attacks in socio-technical systems. The model supports probability and cost, where the intruder model can challenge honest agents. For analysis, they express the security properties using PCTL and PRISM to validate the correctness of the properties on the model. Ouchani et Linzini [START_REF] Ouchani | Generating attacks in sysml activity diagrams by detecting attack surfaces[END_REF] formalized socio-technical physical systems as SysML activity diagrams and provided a library of attacks taken from standard catalogs of social engineering and technical attacks (CAPEC). Then, each diagram is analyzed separately by computing the probability of the weakest points that might host attacks. Bakirtzis et al. [5], Linzini et al. [START_REF] Lenzini | Security analysis of sociotechnical physical systems[END_REF], and Ouchani et Linzini [START_REF] Ouchani | Generating attacks in sysml activity diagrams by detecting attack surfaces[END_REF] rely on a taxonomy of attacks without showing how to instantiate an attack pattern for a specific use case. In addition, they focus more on matching the countermeasures within attacks instead of measuring the severity of attacks then select the appropriate countermeasure.

Mitchell and Chen [START_REF] Mitchell | Modeling and analysis of attacks and counter defense mechanisms for cyber physical systems[END_REF] used stochastic Petri nets to develop an analytical model that can capture the interactions between the adversary and the defense models of CPS by focusing on three failures: attrition, perversion, and exfiltration. Agrawal et al. [2] try to design more secure CPS by relying on two categories of attacks. The attacks from outside were considered as a threat model, which might not be able to connect to an insider threat with the physical access to a CPS. At the same time, they included an attack detection mechanism for an insider attack with a physical access to a CPS. Thus, the dynamics of the system are exploited to detect adversaries based on the laws of Physics. Rocchetto et al. [START_REF] Rocchetto | Cpdy: Extending the dolev-yao attacker with physical-layer interactions[END_REF] proposed to extend Dolev-Yao's attacker model in order to analyze the security of CPS. A set of rules are used to define potential actions of attackers with respect to messages exchanged between parties during a protocol execution. Also, it allowed additional orthogonal interaction channels between parties. Physical properties such as locations and distances were included in the rule set. The previous approaches focus more on attacks related to physical properties instead of looking how to exploit technical vulnerabilities to command the physical processes remotely.

Rocchetto et al. [START_REF] Rocchetto | On attacker models and profiles for cyber-physical systems[END_REF] proposed a class of attacks that can retrieve, update, actuate, and command physical processes. The physical layer is designed to include attack vectors and their associated mitigation mechanisms that cover the attackers' capabilities by relying on a taxonomy that classifies and compares attacker actions. Finally, they select a set of attacker profiles that they consider them more powerful. Puys et al. [START_REF] Puys | Generation of applicative attacks scenarios against industrial systems[END_REF] assessed the security of industrial systems by considering attackers that have already shown their ability to abuse some security breaches to earn access into the industrial systems. To find such attacks, they took into account different parameters especially the behaviour of the process, the safety properties to be ensured, and the possible positions and abilities of attackers. Both contributions try to find potential attacks from a predefined classes without a mitigation process. Further, they do not estimate the sevirity of each attack.

Xiaoxue et al. [START_REF] Liu | Modeling cyber-physical attacks based on probabilistic colored petri nets and mixed-strategy game theory[END_REF] described the existing threats that are dependent to the security and safety of CPS that are modeled by using a hierarchical method of division and integration. They proposed a quantitative analysis and modeling approach to express threat propagation using a probabilistic colored Petri net model that includes basic models, rules, logical operators and transitions as a menace breeding between nodes. The weights of the connections in the attack model are computed using a mixed-strategy attack-defense game approach by solving the Nash equilibrium. Adepu and Mathur [1] designed attacker models dedicated to CPS by generating a parameterized attack models in order to capture both physical and cyber attack abilities. For each class of attacks, they look for the common possible parameters between cyber and physical attributes. Ouchani [START_REF] Ouchani | Ensuring the Functional Correctness of IoT through Formal Modeling and Verification[END_REF] proposed to analyze the functional correctness of IoT in a mixed environment. A formal model is proposed to cover various aspects such objects and services. For the analysis part, the approach relied on the PRISM probabilistic model checking by transforming an IoT model into PRISM source code, and expressing the functional properties in PCTL. The model covered the main components of IoT systems, however the framework suffers from the model checking inherited limitations and the security properties are not specified. Those contributions presented a formal modeling for CPS without showing how it has been developed. Further, the developed attacks are generic without relying on the provided models.

With respect to the reviewed approaches, the present work try to capture the underlying semantics of ICPS, and develop an automatic way to generate the behaviour of a concrete model. Further, it develops an extensible library that can be updated for attacks and countermeasures. Furthermore, it relies on PRISM model checker to assess the security of ICPS.

The security assessment framework

The SSA-ICPS framework depicted in Figure 1 assesses the severity degree of attacks in industrial cyber physical systems (ICPS) by covering the modeling, the security analysis, attacks, and mitigation of ICPS. For the modeling part, SSA-ICPS develops a predefined library of flexible and extensible templates for the ICPS architectures, components, and communication protocols. Further, it models different smart attacks related to every ICPS component. To precisely describe an ICPS's behaviour, a user has only to rely on the library to design a complete ICPS as well as to specify the behaviour of each component following a well-guided predefined syntax. Additionally, it covers the set of security requirements needed to be satisfied as well as a set of countermeasures to recover and reinforce the system under development. The analysis module instantiates first the possible attacks specific to the modeled ICPS so to compose them together to form a malicious environment. Also, it instantiates the security properties to check if they are valid or not within this composition. To overcome the analysis complexity, SSA-ICPS has an acceleration procedure that makes the checking process much easier and helps to rapidly find all possible attack scenarios as well as to measure the severity of each succeeded one. Finally, to reinforce the ICPS model, the recommendation process produces the possible optimal countermeasures configuration for the attacks.

System's model

This section describes the formal model that takes into consideration the ICPS architecture previously discussed (see Figure 1) as a composition of interconnected nodes: physical objects (devices and controllers, e.g. sensors and buildings), mobiles applications, cloud and computing online services, and social agents (people).

Node

This is the main entity describing an ICPS, and it is defined as tuple ⟨id, attr, Actuator, Σ, Beh⟩, where:

• id is a fixed set of insignia id ϵ , • • • , id i , • • • ∈ id identifying nodes where id ϵ is the empty node.

• attr : id → 2 T evaluates the attributes of a node, such that T = {p, c, m, d, r} where p, c, m, d, and r stand respectively for physical, container, movable, destroyable, and reproducible.

• Actuator : id → loc × 2 id × id × B is a function that evaluates the tuple ⟨loc, cont, key, locked⟩ specifying the status of a node id i by returning respectively its: location, contained objects, key, and if it is locked or not.

• Σ is a finite set of atomic actions that a given node can execute, where:

Σ ={Start, Terminate, Send(id i , id j ), Receive(id i , id j ), Update(id i , id j ), Lock(id i , id j ), Unlock(id i , id j ),
Move(l, l ′ ) : id i , id j ∈ id and l, l ′ ∈ loc}.

Start and Terminate starts and terminates the process of a node, Send(id i , id j ) and Receive(id i , id j ) sends and receives id i to/from id j , Update(id i , id j ) updates id i by id j , Lock(id i , id j ) and Unlock(id i , id j ) lock and unlock id i with id j , respectively.

• Beh : id → L returns the expression written in the language L that describes the behaviour of a node. The syntax of L is given by:

BStart |Terminate | α • B | α • B + g α • B | α • B + p α • B | α • B + α • B | α • B| α α • B | α • B||α • B
, where α ∈ Σ and " • " composes sequentially the actions, and + g is a guarded choice decision, + p is a probabilistic decision, + is a non deterministic choice, | α is a synchronization on the action α, and || is the interleaving operation.

Node's behaviour

To characterize the behaviour of a node, say n, we first define its state and how this can change as a labeled state transition system ⟨S, s 0 , -→⟩ where S is all possible states of n, s 0 ∈ S is its initial state, and -→⊆ (S × L × µ × S) is the closure transition relation between states labeled by l ∈ L and executed with a probability p ∈ µ (µ is a probabilistic distribution). A transition → defines the changes of a node n and represented by a set of operational semantics rules. For example, the SRT rule describes the initial execution of a node n.

B n = Start.B ′ n SRT ⟨id n , -, ⟨-, -⟩, -⟩ startn ----→ ⟨id n , B ′ n , ⟨-, -⟩, -⟩ The rule UP updates sending a value [[m]] of the variable x by a value [[m ′ ]] in a node n. B n = Update(x, [[x ′ ]]).B ′ n ∧ x ∈ cont(n) UP ⟨id n , -, < -, {x, [[x]]} >, -⟩ upx --→ ⟨id n , B ′ n , < -, {x, [[x ′ ]]} >, -⟩
The rule SYN describes a node n sending a value [[m]] of a variable x to another node n ′ carried by the variable y.

B n = Send(n ′ , x).B ′ n ∧ x ∈ cont(n) ∧ [[x]] = m ̸ = ϵ o B n = Receive(n, y).B ′ n ′ SYN ⟨⟨id n , -, < -, {x, [[x]]} >, -⟩, ⟨id n ′ , -, < -, {y, -} >, -⟩⟩ sndrcvx -----→ ⟨⟨id n , B ′ n , < -, {x, [[x]]} >, -⟩, ⟨id n ′ , B ′ n ′ , < -, {y, [[x]]} >, -⟩⟩
The set of all operational semantics rules are given in Appendix 6.1.

ICPS Architecture

The ICPS architecture is the main structure carrying a ICPS system. In harmony, it regroups all nodes together. It is modeled by a directed graph where the vertices are the set of nodes and edges are their interaction. Formally, the ICPS architecture is a tuple ⟨V, E, π, CM ⟩, where:

• V = N is a finite set of nodes: n 0 , • • • . • E ⊆ N × N is a finite set of links between nodes, such that for every e ∈ E
there is a pair of channels e ij = ⟨n i , n j ⟩ and e ji = ⟨n j , n i ⟩.

• π : E -→ P rot returns the communication protocol for an edge in E.

• CM : N ∪ E -→ C returns the proper countermeasure to a node or an edge.

The communication protocol synchronizes and organizes the communication and the interactions between nodes. However, we have also defined many communication protocols depends on the nature of each node. Formally, prot ∈ P rot is the tuple ⟨P rot o,s , P rot s,s , P rot o,o , P rot h,o ⟩ where P rot o,s ensures the communication between objects and services, P rot s,s between services, P rot o,o between objects, P rot h,o between social actors and abjects.

For P rot s,s , we would take the example of Modbus protocol described with a set of action and events Σ ′ , where we have:

Σ ′ = {start L (m), send L (a 1 , a 2 , m 1 ), recieve L (a 2 , a 1 , m 2 )}.
The action start L (m) is the initialisation of the protocol, send L (a 1 , a 2 , m 1 ) denotes sending the message m 1 from agent a 1 to a 2 , recieve L (a 2 , a 1 , m 2 ) means receiving m 2 by a 2 from a 1 . The label L gives the order of events. Further, we consider the execution of the behaviour as a session, and formally it is defined as a tuple s = ⟨id, σ, φ, ε⟩, where id is the identifier of the session, σ are the initiator and the responder, φ are the values of the variables, ε is a set of events.

Let prot ∈ P rot be the specification of a protocol and A is the set of active sessions. The basic operational semantics rule of P rot are given in Table 1. The Start rule states that a new session can only be created if its identifier has not been used yet. The send rule shows that if the session executes the send event then the message will be added to the buffer B s and executes the next event ε. The receive rule expresses that there is a session where the next event is receive and B r contains a message. The latter will be removed from the buffer B r to proceed the execution of the next event ε.

s = (id, σ, φ, ε) ∈ P rot id / ∈ A ⟨B s , B r , A⟩ start( s ) ----→ ⟨B s , B r , A ∪ {s}⟩ start e = send L (a 1 , a 2 , m 1 ) (id, σ, φ, [e].ε) ∈ A ⟨B s , B r , A⟩ send(s) ---→ ⟨B s \{m}, B r {m}, A⟩ send e = recieve L (a 2 , a 1 , m 2 ) (id, σ, φ, [e].ε) ∈ A m ∈ B r ⟨B s , B r , A⟩ recieve(s) -----→ ⟨B s \{m}, B r {m}, A⟩
recieve Table 1: A session operational semantics rules.

We defined the operational semantics rules using a labelled transition system ⟨S, S 0 , -→ ⟩, where S is the set of all states in the system, S 0 is the initial state and -→⊆ (S × L × S) is the transition relation between states labeled by L, where L ∈ labels(Σ ′ ) and labels is a function that returns a label for each action of Σ ′ .

Figure 2 depicts the architecture of an ICPS using ICPS-graph, where C is a multi-protocol client, S 1 and S 2 are Modbus and OPC-UA servers, P is a pro-grammable logic controller (PLC), Se is a sensor, V is a valve, and M is a motor. All nodes are connected through digital (e.g. Modbus, OPC-UA) and analogic channels.

Countermeasures

To harden a system against various attacks, we use a suitable security measure. A countermeasure could take different forms, such as recommendations about how to modify the architecture of the system, how to assure the security of the system or a software, and/or how to add or modify physical measures (e.g. door digital code, firewall, etc.). Formally a countermeasure c ∈ C is a tuple ⟨id, N, Σ cm , Beh cm ⟩, where:

• id is a finite set of tags id 1 , • • • , id i , • • • , id n identifying a software or physical measures.

• N is a finite set of nodes.

• Σ cm is a set of actions can be executed by a countermeasure cm, where:

Σ cm ={Start, Terminate, Filters(net i , net j ), Scan(n i ), Crypt(n i , n j ), Decrypt(n i , n j ), Auth(n i ), CheckPers(e i ), Lock(n i , d j ), Unlock(n i , d j ) : net i , net j ∈ N et, n i , n j ∈ N ode, e i ∈ E and k j ∈ Key}
Start and Terminate starts and terminates the process of a countermeasure, Filters(net i , net j ) filters and controls incoming and outgoing network traffic between net i and net j based on predefined security rules, Scan(n i ) scans the node n i (e.g. computer) from malwares, Crypt(n i , n j ) encrypts the communication between the nodes n i and n j , Decrypt(n i , n j ) decrypts the communication between nodes n i and n j , Auth(n i ) uses an authentication method (e.g. password) for the node n i , CheckPers(a i ) exams the personalty of an employee e i , Lock(n i , k j ) and Unlock(n i , k j ) locks and unlocks n i with n j , respectively.

• Beh cm : CM -→ L cm returns the behaviour of a countermeasure. The syntax of L cm is given by:

BStart • B |Terminate | α • B | α • B + g α • B
, where α is an action and " • " composes sequentially the actions, and + g is a guarded choice decision.

Attacker model

Based on the literature, Dolev-Yao attacker model [START_REF] Dolev | On the security of public key protocols[END_REF] is the most powerful one that can access and manipulate arbitrarily all the network traffic. This attacker model is usually employed for the identification attacks (e.g, Web Application). It can intercept messages and analyze them if he possesses the corresponding keys for decryption. Also, it can generate messages from his knowledge, and send them as any honest or impersonate agent. However, this attacker model suffers from the state explosion and affects only the network layer as a main-in-the-middle. Our proposed attacker model is an improved version using the reinforcement learning and the multi-criteria analysis, where the attacker can perform all type of attacks (i.e. network, physical, software, and social engineering). In addition, we avoid the state explosion problem by relying on the reinforcement learning based on the multi-criteria analysis that makes the decision more deterministic and smart.

Hence, we describes the potential attacks proper to ICPS components and their interactions. As shown in Figure 3, the ICPS attacker model has two components: 1) Data contains knowledge, personality and skills, and 2) the Analyzer that is an inference based engine generating attacks according to data, the received inputs, and its skills and inference levels. The attacker model could be one from the internal employer who works inside or outside (e.g. disgruntled employees or a social engineering victims), a malicious software, or any node with powerful capabilities and techniques.

The ICPS attacker depicted in Figure 3 takes as input the channel Chan, the physical access P hy, and the human interaction Hum. Chan means that the attacker intercepts the message between the ICPS components. P hy means that the attacker has physical access (e.g. open a door). Hum means that the attacker interacts or communicates with an employ from inside.

Data

The data ω of the attacker is a tuple ⟨K, P, S⟩, where K represents its knowledge, P is the personality of the attacker, and S is the set of skills. Formally, the knowledge of the attacker (K) is a tuple, K = ⟨M, Sec, Alg⟩. Consequently, the knowledge in data can change according to the type or the level of attackers.

Personality

To fulfill the personality requirements, we rely on the well know theory from psychology called the big five personality traits, and also known as the five-factor model (FFM). Each factor represents a type of personality (Openness to experience, Conscientiousness, Extra-version, Agreeableness, Neuroticism) and the highest factor from the five above is the personality of the person. In our work, we are interested in the last factor Neuroticism, because the people who have a high level in this factor have emotions like: anger, anxiety, depression, and vulnerability. Formally, the personalty is a vector Per, where each element is an emotion e in the state i.

Per = e 1 e 2 . . .

e n where ∀i ∈ [1, n], e i = 1 positive 0 absence -1 negative

Goal

An attack is a set of actions or small attacks where each action has a goal, and formally a goal G is a set G = {g 1 , g 2 , . . . , g n }. An attacker must achieve all goals where g i is an expression specifying a state of nodes.

Analyzer

Since a given attack A is a set of actions, the choice of this set depends on the set of the selected criteria. We use Markov Decision Process (MDP) and a multi-criteria analysis to model the decision of the attacker as well as the reinforcement learning to select the optimal sequence of actions to maximize the attacker assets. Algorithm 1 describes how the attacker could choose an action based on its goal while minimizing the cost.

Algorithm 1 Generation attack actions.

U (s) = R(s) + λ max a∈A(s) s ′ ∈S P(s ′ , s, a) × U (s ′ ); //Measure
the cost of a state s. Algorithm 1 takes as input a Markov Decision Process model M mdp to produce the set of actions π. M mdp is a tuple M mdp = (S, A, s 0 , R, P, γ), where:

• S is a set of finite states s 2 , s 2 , etc.

• A is a set of finite actions a 1 , a 2 , etc.

• s 0 is the initial state.

• R(s) is a reward function that returns the utility for each state s.

• P(s, a, s ′ ) the probability of being in the state s ′ after executing the action a from state s.

• γ is a discount factor 0 < γ < 1.

To achieve a state s i in the model representing a sub-goal g i , the attacker should execute an action a i according to a sequence of decisions based on data. R(s) is calculated with respect to the Weight Sum Method as follows

R(s) = m j=1 w j c ij , i = 1, 2, ..., n
whre c is a set of criterion to select an action and w denotes the relative weight of importance of c. The probability of a transition P(s, a, s ′ ) depends on the value of R(s ′ ) and the sum of all the R(s ′ ) for the successors of the state s. P(s, a, s

′ ) = R(s ′ ) ∀s ′ ∈succ(s) R(s ′ )
The selection of a transition depends of the utility of each state and the accumulated reward. In our case, the attacker will choose the actions to earn more rewards.

ICPS Engine

The ICPS engine contains two main parts. The first part is the analyzer that measures the severity of attacks and their scenarios. Further, it reports bugs and existing vulnerabilities. The second part relies on the security report to recommend the optimal countermeasures. It also provides hints the best practices for the developed ICPS system.

ICPS Analyzer

For the analysis, we rely on the probabilistic symbolic model checker PRISM that verifies probabilistic specifications over probabilistic models. A specification can be expressed either in the probabilistic computation tree logic (PCTL) and a model can be described using PRISM language.

A model can be a discrete-time Markov chains, continuous-time Markov chains, and Markov decision processes (MDPs). Alternatively, a model can be a probabilistic timed automata. PRISM also supports probabilistic automata. PRISM verification is efficient, since it stores models as binary decision diagrams and multi-terminal BDDs. To overcome the state explosion problem, PRISM has built-in symmetry reduction and implements some iterative numerical analysis like Jacobi and Gauss-Siedel.

In general, a given PRISM program is a composition of a set of modules. A module is evaluated over a fixed number of local variables, of type Boolean or integer. Whereas the state of a given module is formulated as the evaluation of its local variables, the global state of a PRISM program is the evaluation of all variables, local and global, for all modules. Further, the composition and the communication between PRISM modules adopt the operators developed by the CSP process algebra.

Basically a PRISM module defines the kernel behaviour of a PRISM program. At this end, the behaviour of a module is a collection of commands that can be probabilistic or Dirac. Textually, a probabilistic command is expressed by [α] g → p 1 : u 1 +...+p m : u m , such as p i are probabilities (p i ∈]0, 1[ and m i=0 p i = 1), α is a label expressing the name of the action α, g is the guard represented as a propositional logic formula over all variables, local and global, and u i describes the update (new value) for an ensemble of variables. A given update expressed by

(v ′ j = val j )& • • • &(v ′ k = val k ),
assigns only values val i to local variables v i . So, for a given action α, if the guard g is valid, then the update u i is enabled with a probability p i . In general, the guard is an expression consisting of the evaluation of all variables that are connected explicitly with the propositional logic operators. The Dirac case where p = 1 is a special case command expressed simply by: [a] g → u.

Syntactically, a module named M is delimited by two keywords: the module head "module M ", and the module termination "endmodule". Further, we can model costs with a reward module R delimited by keywords "rewards R" and "endrewards". A reward module is composed from a state reward or a transition reward. A state reward associates a cost (reward) of value r to any state satisfying g and it is expressed by g : r. A transition reward is specified by [a] g : r to express that the transitions labeled a, from states satisfying g, are acquiring the reward of value r.

Finally for the analysis, a PRISM program P proper will be generated to the provided ICPS formalism. For that, we introduced the function T P that assigns for each ICPS node behaviour its proper PRISM code fragment that is bounded by 'module node name' and 'endmodule' and the semantic rules of each action is expressed by a PRISM command.

For the semantic rule of any entity, its premises represent the guard of the entity PRISM command, whereas the update describes the consequence of the rule. For example, o o2 is an atomic proposition showing the the object o possess o 2 , l a and l o present the locations, and p o3 precises the physicality attribute of o 3 . The variables and propositions are evaluated first to describe the initial state of nodes by relying on the tuple obtained by the Actuator proper to each entity. T P implements this transformation for each entity depends its category, and here we consider the transformation of rules already presented in Section 3.1.

T P (α) =                                            [Syn o2 ]o o2 ∧ o 1o 3 ∧ ¬p o2 ∧ ¬p o3 → (o ′ 2 = o 2 ); [Syn o2 ]o o2 ∧ o 1o 3 ∧ ¬p o2 ∧ ¬p o3 → (o ′ 3 = o 2 ); iff:Send(o 1 , o 2 ) ∈ Σ o1 o , Receive(o 3 , o 2 ) ∈ Σ o2 o . [T ak o1 ]l a = l o ∧ o o2 ∧ ¬lock o ∧ p o2 → (a ′ o2 = ⊤); [T ak o1 ]l a = l o ∧ o o2 ∧ ¬lock o ∧ p o2 → (o ′ o2 = ⊥); iff:Receive(o, o 2 ) ∈ Σ a . [loc o1 ]o o1 ∧ o o2 ∧ ¬k o1 ∧ p o1 = p o2 → (k ′ o1 = ⊤); [loc o1 ]o o1 ∧ o o2 ∧ ¬k o1 ∧ p o1 = p o2 → (o ′ o1 = ⊤); iff:Lock(o 1 , o 2 ) ∈ Σ o o .
More details about the function T P are provided in Appendix 6.2.

Security requirements

To specify ICPS security requirements and policies we use PCTL syntax presented as follows

ϕ ::= ⊤ | ap | ϕ ∧ ϕ | ¬ϕ | P ▷◁ p [ψ] | R[ψ] ψ ::= Xϕ | ϕU ≤ k ϕ | ϕUϕ
where the term "⊤" means true, "ap" is an atomic proposition, k ∈ N , p ∈ [0, 1], and ▷◁∈ {<, ≤, >, ≥}. The operator "∧" represents the conjunction and "¬" is the negation operator, P is the probabilistic operator, and R is the reward operator. Also, "X", "U ≤ k ", and "U" are the next, the bounded until, and the until temporal logic operators, respectively.

ICPS Recommendation

To provide a secure and valid system model, we designed a recommendation strategy to reinforce the model's system. It is based on the defense-attack tree by extending Markov Decision Attack Trees with counter-measures. Each path of the attack tree is labelled with a countermeasure. Formally a recommendation, say r, is the tuple ⟨M, C , Φ⟩, where:

• M is the attack tree instantiated from the MDP.

• C is a finite set of countermeasures c 1 , • • • , c i , • • • c n
• Φ : P -→ C returns for a path p i a countermeasure c i . P is the set of paths and sub-path proper to M.

Figure 4 depicts an Markov Decision Attack

Tree extended by countermeasures. The red node is the goal of the attack, blue nodes are the sub-goals or steps of an attack whereas the green nodes are the countermeasures for each path of an attack. R is the reward to achieve the state of a node. (P), (1 -P), (1) are the probabilities to execute an action.

Goal R 1 R 2 Countermeasures Action2 (P = 1) A ct io n 1 (P ) R 3 R 5 R 6 Countermeasures Action7 (1) A ct io n 4 (P ) R 4 R 7 Countermeasures Action6 (1)
A ct io n5 (1 -P )

A ct io n3 (1 -P )

Experimental results

This section describes the implementation of our approach and its validation on two real use cases. The experiments were carried out on a PC with Intel Core i5-7200U @ 2.50GHz processor and a RAM of 8.00 GB.

Tool Architecture

Figure 5 depicts the overall architecture of the proposed framework. It implements four packages: (i) the user interface to interact within the kernel of the tool, (ii) the model builder to create and composite the system model and the attacker, (iii) the verification engine to check and reinforce the system in case of successful attacks, and (v) the library that contains templates, attackers, and countermeasures.

User interface

The graphical interface allows a user to interact with our tool through four services.

Template service is connected with the library and it is used to create the system model by relying on specific templates like nodes and protocols. Syntax Checker checks the syntax of our language which is used to define the model service. The language is defined in Section 3.1 and we will see how to model a system with it in our case studies.

Simulation shows the execution of the system and Report presents information about the generated PRISM model, the attacks scenarios, attacks impacts, and countermeasures.

Model builder

The main objective of this component is to build the system model in interaction with the attacker. We build the model system from templates and nodes behaviours after that we compose the model system with the attacker through synchronization channels.

Engine

It is the main part in our tool, it contains two components, Model checker to verify the security requirements and to generate the attacks scenarios and Recommendation service to reinforce the system model by proposing a list of suitable countermeasures.

Library

It contains the templates of nodes, protocols, countermeasures and attack models.

Case study 1: Utah water-supply

The proposed framework is validated on Utah water-supply2 system (see Figure 6), which is designed by Logan to enable building an interconnection between Trenton and Amalga systems to guarantee water supply during emergency situations. This system connects numerous sensors to monitor the pressure from water sources to tanks and from tanks to both towns by measuring tank level, chlorine water level, flood conditions and chlorine gas leaks at the building hosting the system. Also, the system controls a set of pumps and valves.

Figure 6: Water-Supply system.

We parameterized the system with a set of variables of type Boolean and integer to define the status of the monitoring and control dashboard. The set of Boolean variables that controls the pumps and valves is V p = {P ump, V alve 1 , V alve 2 , SysRun}, where SysRun is used to initiate the system, P ump and V alve 1 defined to fill the tank, and V alve 2 introduced to distribute the water from the tank to the agglomeration. To better monitor the status of sensors, V d is used to define each flag and data that evaluate a sensor's measure, where: V d = {T ankLevel, F lood, ChlLeaks, ChlInwater, P res}. T ankLevel returns the level of the tank, F lood evaluates if there is any flooding in the building, ChlLeaks to check if there is chlorine gas leaks at the building, ChlInwater measures the level of the chlorine in the water, and P re returns the measured pressure of the water. Further in an emergency situation, the worker can manually start or stop the pump.

The formal model

In the water-supply system presented in Figure 6, two servers s 1 and s 2 are accessible through the client c (a unique client deploying multi-protocols). o s1 p is the object of the vector V p controlled by the OPC-UA server s 1 . The o s2 d is the object of the vector V d controlled by the Modbus server s 2 . The servers s 1 and s 2 control the objects o s1 p and o s2 d through the PLC p. Herein, we describe briefly the behaviours of the client C, the servers s 1 , s 2 , and one physical node (e.g. valve).

The ICPS Model -The behaviour of the client c.

Beh(c) = Start.(Receive s,s ([[o d ]], s 2 ).Update s,s (o p , [[o ′ p ]]).Send s,s (s 1 , o ′ p ) +Receive s,s ([[o d ]], s 2 ).Update s,s (o d , [[o ′ d ]])+Send s,s (s 1 , o p )).Terminate.
-The behaviours of the servers.

Beh(s) = Start.(Receive s,s ([[o]], c).Send o,s (o, s) + Receive o,s ([[o]], o).Send s,s (c, [[o]])).Terminate.
-The behaviour of the valve.

Beh(v) = Start.(Receive o,o ([[o]], p).Unlock o (v, port) + Receive o,s ([[o]], p).Lock o (v, port)).Terminate.

The technical attacker

We consider here an attacker that gains the access to the network with the ability to interact with an employee who has access to the room of control. Herein, we describe briefly the different parts and the ability of this attack.

Knowledge The attacker knowledge consists of the information about the architecture of the network without having any private keys or any physical access. Also he has the algorithm to encrypt, decrypt, and hash messages.

Personality We do not define the personality of the attacker because we will not cover the security analysis related to the social aspect within this attack. We will consider it in the next attack's case.

Skills

In this case study we have defined only the communication attacks as a skills for the attacker. So, according to his knowledge he can intercept, replay and create messages, encrypt and decrypt if he has a private key. Table 2 specifies the attacker skills. We have used SPi-calculus to formalise the skills of the attacker . (v i) allows to add, save, update or get data from his knowledge.

Table 2: Specification of the attacker's skills A = (v i)(canal(x).!(i⟨x⟩.0 + i(m).0 + i(pk).0 + i(sk).0

+ i(m 1 ).i(m 2 ). ī(⟨m 1 , m 2 ⟩).0 + case x of ⟨m 1 , m 2 ⟩ in i⟨m 1 ⟩.0 + case x of ⟨m 1 , m 2 ⟩ in i⟨m 2 ⟩.0 + i(⟨m 1 , m 2 ⟩).i(m 3 ). ī(⟨m 3 , m 2 ⟩).0 + i(⟨m 1 , m 2 ⟩).i(m 3 ). ī(⟨m 1 , m 3 ⟩).0 + case x of {[m]} sk in i⟨m⟩.0). (canal⟨m⟩.0 + canal⟨[{H(m)}] sk ⟩.0))
Goal The goal of the attacker is to dysfunction the system by not filling the tank.

Analysis The attacker objective is described as a Markov decision tree and to calculate the reward for each state we use a weight sum method. Table 3 describes the selected criterion. D is the expected probability to not detect the attack step, 1 means no risk to detect whereas 0 means there is a big risk to detect the attack. F means the feasibility of the attack, 1 means that the attack is feasible and 0 not. S represents if the attacker has the skills to realize this attack step or no, 1 means true and 0 false. The Socio-technical attacker

Here we consider the attacker as an employee who works in this water-supply. For his knowledge and skills, he has the information about all the system and the access control of SCADA client. Further for his personality, he has a high factor of Neuroticism which means that he is vulnerable and he could be exploited by social engineering technique.

Security requirements

For this case study, we exhibit the following properties:

• The attacker cannot stop the system. • The attacker cannot open the valve and the tank is full.

Φ 3 : P max =?[F (V alv1 = 1 & T ank = 2)]

Results

The results, obtained from the verification of the code in Appendix 6.3, are summarized in Table 4 where the symbol ✓ means an attack has been found and the symbol ✗ means that the property is safe. Further, we show the verification of each property with respect to the category of the attack. For the technical attack, the obtained MDP model has 215380 states (1 initial), 1169586 transitions with 997282 choices. Whereas the obtained MDP model for the socio-technical attack has 99220 states (1 initial), 514008 transitions with 434632 choices. In theory, the technical attacker cannot violate the property Φ 1 because the OPC-UA server controls the SysRun variable. Thus, the only way to break the property Φ 1 is to manipulate the social attacker, which obviously is not possible as the technical attacker does not have social engineering skills. As well the social attacker does not violate any property because we supposed that he could violate the properties only if he was manipulated by social engineering skills. The result of attacks proper to Φ2 in Figure 7 shows the convergence of the probability evaluation from 0 to 0.15 after two steps, then it increases up to the maximum value of 0.25 after 10 steps. This result shows that the risk is low when the system is turned on. Compared to the property Φ1, the probability of attacks for Φ2 increases linearly to achieve a maximum of 0.225.

Figure 8 depicts the sequence diagram of the attacker violating Φ3. The Modbus server sends a message to inform a client that the tank is full, and therefore the valve needs to be closed. However, the attacker intercepts the message and modify it in order to leave the valve open while the tank is full. This experiment shows that, even if the non-secure protocols control only the nodes that are not more sensitive than the other nodes, this can create vulnerabilities and destabilize the system. Countermeasures As shown in Figure 9, the origin of the security breach was originally related to the specifications/implementation of Modbus protocol. Unfortunately, this cannot be changed to OPC-UA protocol as the most deployed equipment (sensors or other) requires the use of Modbus. Consequently, as output, the recommendation system suggests the use of Modbus protocol under the VPN to guarantee better security of the running system.

Case study 2: Maroochy Shire Sewage Spill

Maroochy Shire is located about 100 kilometers north of the Queensland State Capital of Brisbane. It has 880 kilometers of gravity sewers treating an average of 35 million liters/day. The Maroochy Water Services Sewerage SCADA system consists of 142 Sewage Pumping Stations, and each pumping station had a computerized system capable of receiving commands from a central control center (master station) and transmitting signals back to the center. The communication between pumping stations and the control center was through a private two-way radio system. Figure 10 shows the system architecture and the connection between its components. The control of the pumping stations can be through the main SCADA station or through one of the pumping stations access points.

The formal model

In the Maroochy Water Services presented in Figure 10, p i is a pump, s i j a sensor that measures the status of the pump p i , r k a remote terminal unit (RTU), m a master station, a an access point, and h an agent who uses the access points with a laptop to manage the system. We used Beh(m) to describe the behaviour of the master station m where it can receive or send a command from/to RTU r i . Beh(r i ) represents the behaviour of the RTU r i where it can communicate with the master station m, another RTU r j , a pump p j , an access point a j or a sensor s j . Beh(p i ) is the behaviour of the pump, it could receive a command o rj from an RTU to change its state to start or stop running. Beh(s i ) represents the behaviour of the sensor to receive the status of the pump and send it to the RTU. Beh(h i ) is the behaviour of an agent using the access point to receive and send commands.

-The behaviour of the master station m.

Beh(m) = Start.(Receive([[o ri ]], r i ).Update(o im , [[o ri ]])+Send(r i , [[o im ]]) + Send(r j , [[o jm ]])).Terminate -The behaviours of the RTU r i . Beh(r i ) = Start.(Receive([[o mi ]], m)+Receive([[o rj ]], r j )+Receive([[o aj ]], a j ) + Receive([[o pj ]], p j ).Update(o i , [[o i ]]).Send(m, [[o ri ]]) + Send(r j , [[o rj ]]) + Send(p k , [[o ri ]])).Terminate.
-

The insider technical attacker

In this scenario, we model the attacker who hacked the system in the real world.

Knowledge The real attacker was an old employee with a strong knowledge about the system functionalities and the used communication protocols.

Personality The attacker has a high factor of Neuroticism.

Skills The attacker has already installed the software in his laptop as well as he has the knowledge to connect to the system, to change the state of all the pumps, and either to enable/disable alarms. Table 5 specifies the insider attacker skills.

Table 5: Specification of the insider technical attacker.

A = (v i)(canal(x).!(i⟨x⟩.0 + i(m).0 + i(m 1 ).i(m 2 ). ī(⟨m 1 , m 2 ⟩).0 + case x of ⟨m 1 , m 2 ⟩ in i⟨m 1 ⟩.0 + case x of ⟨m 1 , m 2 ⟩ in i⟨m 2 ⟩.0 + i(⟨m 1 , m 2 ⟩).i(m 3 ). ī(⟨m 3 , m 2 ⟩).0 + i(⟨m 1 , m 2 ⟩).i(m 3 ). ī(⟨m 1 , m 3 ⟩).0). (canal⟨m⟩.0)
Goal. The main objective of the attacker is to take the control over the station pumping.

Analyzer. Table 6 describes the expected probability to not detect the attack step D, the feasibility of the attack F, and the skills S. The external technical attacker #1

This attacker has less knowledge and skills than the insider attacker.

Knowledge This attacker has a knowledge about the fourth pumping station as well as the radio communications.

Personality In this scenario of attack, we exclude the importance of the attacker personality.

Skills This attacker knows how to find the radio frequency and how to receive and send data over the found channel. He can do only DoS attack to saturate the channel. Table 7 specifies the skills of the external technical attacker #1.

Table 7: Specification of the external technical attacker #1.

A = (v i)((canal(x).i⟨x⟩.0 ) + ( i(m). !(canal⟨m⟩.0)))

Analyzer. Table 8 describes the selected criterion D, F, and S previously defined. The external technical attacker #2

We model this attacker with another kind of knowledge and skills than the first one.

Knowledge We consider that this attacker has no knowledge about the pumping stations.

Personality We exclude in this scenario the personality description and impact on the attack goal.

Skills As described in Table 9, the attacker has good skills on malware development, reverse engineering, network analysis and social engineering.

Table 9: Specification of the external technical attacker #2.

A = (v i)((canal chan (x) + canal hum (x)).!(i⟨x⟩.0 + i(m).0

+ i(m 1 ).i(m 2 ). ī(⟨m 1 , m 2 ⟩).0 + case x of ⟨m 1 , m 2 ⟩ in i⟨m 1 ⟩.0 + case x of ⟨m 1 , m 2 ⟩ in i⟨m 2 ⟩.0 + i(⟨m 1 , m 2 ⟩).i(m 3 ). ī(⟨m 3 , m 2 ⟩).0 + i(⟨m 1 , m 2 ⟩).i(m 3 ). ī(⟨m 1 , m 3 ⟩).0). ((canal chan ⟨m⟩ + canal hum ⟨m⟩).0))
Analyzer. Compared to the previous cases, we consider F as a probabilistic value (Table 10) since the feasibility of a social engineering attack does not depend only on the skills of the attacker but also on the reactions of victims. The feasibility for the social engineering attack is a variable x since he does not know the personalities of the employees. In this case, we consider two scenarios depending the values of x that can be either 0 (scenario 1) or 0.5 (scenario 2). Also, we consider that we have five employees and one of them has a high factor of Neuroticism which means he is vulnerable and he could be exploited by social engineering techniques. Each one of the employee has the information about all the system and the access control of SCADA client. Also they have a laptop and the software to access to the SCADA system through the access points.

Security requirements

For this case study, we have the following properties:

• Pump 4 was running when it should not.

Results

Table 12 and Table 13 show the verification results of the three properties for the described attacks, respectively. Table 11 refers to the size of the constructed MDP proper to each attack in terms of states, transitions, and choices. From the obtained results, we found that the insider attacker and the social-Technical attacker violate all the properties since both of them have all the knowledge, skills and the software to control the system. Further, the external technical attacker #1 could not violate the third property because he has only DoS attack as skills. Thus, he could not disturb the other pump stations. Furthermore, the external technical attacker #2 could not violate all the properties because he do not have the skills and the knowledge about the system to violate the properties but he succeeded when mastering social-technical attack techniques. Figure 11 shows the success of the insider attacker and the external-technical attacker #1 for Φ 1 . The probability evaluation of the insider attack converges to 0.138 Figure 13 depicts the sequence diagram of violating Φ3 by the external technical attacker #2 (scenario #2). The attack start by sending emails (social engineering attack) to all agents. This phishing email contains a link to download a fake update of the system control software. When the agent click on the link, a malware will be download instead of the trusted software update. Then, the malware starts recording everything (packets, keyboard inputs, etc) and send it back to the attacker. After analyzing the received data, he patches the malware to update the commands. After that, the malware intercepts the command, modifies and sends it to the RTU. Consequently, the pump will be stopped.

Countermeasures Figure 14 shows the countermeasures generated for the violation of Φ2 by the insider attacker (the bottom path), the external attacker #1 (the middle path), and the external attacker in scenario #2 (the upper path). Each path is an attempt from all possible flows of each attack. The origin of the security breaches were initially related to two points: 1) the insider attacker has too much power, and 2) the use of the radio communication. The generated countermeasure rely on a defense-in-depth strategy. First, it proposes the use of access control to alleviate an attack. In addition, it suggests an identification and authentication mechanism to harden the access control and issuing radio commands. Further, it prefers the use of the system monitoring to ensure the real time trustworthy and functionality of the system. Also, it recommends a system and information integrity to avoid sending false commands and controlling pumps. Furthermore, it proposes to periodically perform personality tests to assess the employee behaviours and plan training to overcome social engineering attacks.

Stop pump

R1 R2 R3

• Access Control.

• Identification and Authentication.

• System monitoring. flooding the target record a signal ra di o fr eq ue nc y sc an ne r

R1 R2

• System and Information Integrity.

• System monitoring. Disable alarm connect

R1

R2 R3 R4

• Access Control.

• Identification and Authentication.

• System monitoring.

• System and Information Integrity.

Conclusion

This paper sets the fundamentals needed for a fully automatic framework to correctly model and analyze safely security in ICPS. We provided details of the formalism needed for a complete ICPS architecture that captures the main structures and possible behaviour of ICPS entities by covering the physical and information infrastructures, services, assets, social actors, and also their activities and interactions. Further, the formalism included the intruder with different powers regarding the aspect of each ICPS entity. The execution of an action has a cost and guided by probabilities under contextual conditions. At this end, the reinforcement learning aims to help an attack to select an optimal sequence of actions in terms of reducing the cost and maximizing the reward. The proposed formalism has also a rich and flexible semantics, which is used to capture the ICPS functional and security requirements expressing the possibility, the likelihood, and the cost of actions. This is designed to be easy for other extensions/refinements and to automatically carry the functional correctness and security analysis. This is done using the proposed algorithm that transforms an ICPS model into the input language of PRISM so to be checked against the requirements expressed in PCTL within the presence of attacks. Finally, the effectiveness of the framework is validated on two case studies that shows the impact of attacks and how they are mitigated.

The proposed work sets the stage for further improvements. First, we intend to refine the contextual conditions of the proposed formalism, generate automatically the security requirements needed for verification, and provide a countermeasure mechanism that automatically reinforces the ICPS security. Also from a theoretical point of view, we needed to automate the presented proofs for each developed step in a proof assistant (e.g. Coq). Further, we need to accelerate the analysis procedure by introducing the parallelism for probabilistic verification. Furthermore, we intend to implement the proposed framework as a full standing tool and later validate it on different case studies.

Appendices

Operational semantics

For anode n, rules LCK, UCK, and MOV describe respectively locking, unlocking, and moving a node. TRT is to terminate the process. module C l i e n t s c l i e n t : [ 0 . . 7 ] i n i t 0 ;

[ S r e q ] ( s c l i e n t = 0 ) -> ( s c l i e n t ' = 1 ) ; [ Rreq ] ( s c l i e n t = 1 ) -> ( s c l i e n t ' = 2 ; [SOPCUA] ( s c l i e n t = 2 ) -> ( s c l i e n t ' = 3 ) ; [ROPCUA] ( s c l i e n t = 3 ) -> ( s c l i e n t ' = 4 ) ; [ ] ( s c l i e n t = 4 ) -> ( s c l i e n t ' = 5 ) ; s A t t a c k e r =2 : 0 . 5 ; s A t t a c k e r =9 : 0 . 8 7 5 ; s A t t a c k e r =7 : 0 . 5 ; s A t t a c k e r =14 : 0 . 8 7 5 ; s A t t a c k e r =12 : 0 . 5 ; s A t t a c k e r =16 : 0 . 7 5 ; s A t t a c k e r =18 : 0 .

Figure 1 :

 1 Figure 1: SSA-ICPS framework.

Figure 2 :

 2 Figure 2: ICPS Graph.

Figure 3 :

 3 Figure 3: ICPS attacker model.

  |U (s) -U (s ′ )|; 10: end for 11: end while 12: π(s) = arg max a s ′ ∈S P (s ′ , s, a) × U (s ′ ); //Select the path maximizing the reward.

Figure 4 :

 4 Figure 4: Markov Decision Attack-Defense Tree.

Figure 5 :

 5 Figure 5: ICPS Tool Architecture.

Φ 1 :

 1 P max =?[F (SysRun = 0 & Attack = 1)] • The attacker cannot stop the pump. Φ 2 : P max =?[F (P ump = 0 & T ank = 1)]

Figure 7 :Figure 8 :

 78 Figure 7: Attack success for Φ 1 (left) and Φ 2 (right).

M

  od ify (1 -P ) in te rc ep t m sg (1 -P )

Figure 9 :

 9 Figure 9: Markov Decision Attack-Defense Tree proper to Φ3.

Figure 10 :

 10 Figure 10: The Maroochy Water Services Sewerage System.

Φ 1 :

 1 P max =?[F (P ump 4 = 1 & Sensor 4 = 0)] • Pump 4 was not running when it should not. Φ 2 : P max =?[F (P ump 4 = 0 & Sensor 4 = 1)] • Could the attacker stop another pump rather than pump 4. Φ 3 : P max =?[F (P ump i̸ =4 = 0 & Sensor i̸ =4 = 1)]

Figure 11 :

 11 Figure 11: The success of insider Attacker (left) and the External-technical Attacker #1 for Φ 1 (right).

Figure 12 :Figure 13 :

 1213 Figure 12: The success of the social technical attacker for Φ 2 (left) and Φ 3 (right). Attacker Agent Malware RTU Pump send email

•Figure 14 :

 14 Figure 14: Markov Decision Attack-Defense Tree for Φ2.

  B n = lock(o 1 , o 2 ).B ′ n ∧ ¬locked(o 1 ) ∧ o 1 , o 2 ∈ cont(n) ∧ p ∈ attr(o 1 ) ∩ attr(o 2 ) LCK ⟨id n , -, < -, {o 1 , ¬locked(o 1 )} >, -⟩ lock(o1,o2) -------→ ⟨id n , B ′ n , < -, {o 1 , locked(o 1 )} >, -⟩ B n = lock(o 1 , o 2 ).B ′ n ∧ locked(o 1 ) ∧ o 1 , o 2 ∈ cont(n) ∧ p ∈ attr(o 1 ) ∩ attr(o 2 ) UCK ⟨id n , -, < -, {o 1 , locked(o 1 )} >, -⟩ lock(o1,o2) -------→ ⟨id n , B ′ n , < -, {o 1 , ¬locked(o 1 )} >, -⟩ B n = Move(l, l ′ ).B ′ n ∧ loc(n) = l ∧ locked(lock(l)) MOV ⟨id n , -, < loc(n) = l, -, -, -⟩ upx --→ ⟨id n , B ′ n , < loc(n) = l ′ , -, -, -⟩6.3 The Generated PRISM ModelFor the security and performance assessment of the water-supply, the tool generates the PRISM code presented in Listing 6.3 that is proper to the model under test. It shows the code fragments of client, modbus, opcua, and attacker. / / Water -s u p p l y s y s t e m / / C l i e n t : M u l t i p r o t o c o l s / / S e r v e r s ; Modbus , OPC-UA / / PLC / / P h y s i c a l n o d e s mdp / / Network v a r i a b l e s g l o b a l A c t i o n : [ 0 . . 1 0 ] i n i t 0 ; g l o b a l F u n c t i o n : [ 0 . . 1 ] i n i t 0 ; g l o b a l V a l u e : [ 0 . . 2 ] i n i t 0 ;

  l i e n t = 5 ) -> ( s c l i e n t ' = 6 ) & ( A c t i o n ' = 4 ) & ( F u n c t i o n ' = 0 ) ; [ ] ( s c l i e n t = 5 ) -> ( s c l i e n t ' = 6 ) & ( A c t i o n ' = 5 ) & ( F u n c t i o n ' = 0 ) ; [ SModbus ] ( s c l i e n t = 6 ) -> ( s c l i e n t ' = 7 ) ; [ RModbus ] ( s c l i e n t = 7 ) -> ( s c l i e n t ' = 5 c u a : [ 0 . . 3 ] i n i t 0 ; [SOPCUA] ( s o p c u a = 0 ) -> ( s o p c u a ' = 1 ) ; [ RPLC ] ( s o p c u a = 1 ) -> ( s o p c u a ' = 2 ) ; [ SPLC ] ( s o p c u a = 2 ) -> ( s o p c u a ' = 3 ) ; [ROPCUA] ( s o p c u a = 3 ) -> ( s o p c u a ' = 0 ) ; endmodule r e w a r d s s A t t a c k e r =1 : 1 ; s A t t a c k e r =4 : 0 . 8 7 5 ;

  2 5 ; s A t t a c k e r = 5 : 0 ; e n d r e w a r d s module A t t a c k e r s A t t a c k e r : [ 0 . . 1 0 ] i n i t 0 ; A t t a c k : [ 0 . . 1 ] i n i t 0 ; / / I n t e r c e p t [ r e c i e v e _ m o d b u s ] s A t t a c k e r =0 -> ( s A t t a c k e r ' = 5 ) ; [ s e n d _ o p c ] s A t t a c k e r =0 -> ( s A t t a c k e r ' = 5 ) ; [ ] s A t t a c k e r =5 -> 0 . 0 9 7 : ( s A t t a c k e r ' = 1 ) + 0 . 1 7 0 : ( s A t t a c k e r ' = 3 ) + 0 . 0 9 7 : ( s A t t a c k e r ' = 6 ) + 0 . 1 7 0 : ( s A t t a c k e r ' = 8 ) + 0 . 0 9 7 : ( s A t t a c k e r ' = 1 1 ) + 0 . 1 7 0 : ( s A t t a c k e r ' = 1 3 ) + 0 . 1 5 1 : ( s A t t a c k e r ' = 1 5 ) + 0 . 0 4 8 : ( s A t t a c k e r ' = 1 7 ) ; / / Modify Modbus m e s s a g e [ ] s A t t a c k e r =3 -> ( s A t t a c k e r ' = 4 ) & ( A c t i o n ' = 6 ) & ( F u n c t i o n ' = 0 ) & ( Value ' = 0 ) & ( A t t a c k ' = 1 ) ; [ ] s A t t a c k e r =3 -> ( s A t t a c k e r ' = 4 ) & ( A c t i o n ' = 6 ) & ( F u n c t i o n ' = 0 ) & ( Value ' = 1 ) & ( A t t a c k ' = 1 ) ; [ ] s A t t a c k e r =3 -> ( s A t t a c k e r ' = 4 ) & ( A c t i o n ' = 6 ) & ( F u n c t i o n ' = 1 ) & ( Value ' = 0 ) & ( A t t a c k ' = 1 ) ; [ ] s A t t a c k e r =3 -> ( s A t t a c k e r ' = 4 ) & ( A c t i o n ' = 6 ) & ( F u n c t i o n ' = 1 ) & ( Value ' = 1 ) & ( A t t a c k ' = 1 ) ; [ ] s A t t a c k e r =4 -> ( s A t t a c k e r ' = 1 0 ) ; [ r e c i e v e _ m o d b u s _ 1 ] s A t t a c k e r =10 -> ( s A t t a c k e r ' = 0 ) ; endmodule

Table 3 :

 3 Weight sum method settings for the attacker.

	Action/criterion	D	F	S
		0.25 0.25 0.5
	Intercept	1	1	1
	Create msg (Modbus)	0.5	1	1
	Create msg (OPC-UA)	0	0	0
	Modify msg (Modbus)	0.5	1	1
	Modify msg (OPC-UA)	0	0	0
	Replay msg (Modbus)	0.5	1	1
	Replay msg (OPC-UA)	0	0	0
	Block msg	0	1	1
	Social engineering	1	0	0

Table 4 :

 4 The verification results.

	Action/	Technical Verification Social-Technical Verification
	Criterion Attacker Time (secs)	Attacker	Time (secs)
	Φ 1	✗	0.365	✗	0.115
	Φ 2	✓	0.226	✗	0.088
	Φ 3	✓	0.377	✗	0.092

  The behaviour of the pump p i .Beh(p i ) = Start.(Receive([[o rj ]], r j ).(Unlock(p i , o pi )+Lock(p i , o pi ))).Terminate.-The behaviour of the sensor S i .Beh(s i ) = Start.Receive([[s pj ]], p j ).Update(s i , [[s pj ]]).Send(r i , [[s pi ]]).Terminate.-The behaviour of the agent h i .Beh(h i ) = Start.(Receive([[o aj ]], a j ).Update(o i , [[o aj ]]).(Send(a j ′ , [[o i ]] + Receive([[o aj ]], a j )).Terminate.

Table 6 :

 6 Weight sum method settings for the insider technical attacker.

	Action/criterion D F S
		0	1 1
	Create msg	0	1 1
	Replay msg	0	1 1
	DoS attack	0.5 1 0

Table 8 :

 8 Weight sum method settings for the external technical attacker #1.

	Action/criterion D F S
		0.5 1 1
	Read msg	1	1 1
	DoS attack	0.5 1 1

Table 10 :

 10 Weight sum method settings for the external technical attacker #2.

	Action/criterion	D	F	S
		1 0.5 1
	Modify Msg	1	1	1
	Social engineering attack 1	x	1

Table 11 :

 11 The model complexity in the presence of the different attackers.

	Action/	Insider	External-Technical	External-Technical	External-Technical
	Criterion Attacker	Attacker #1	Attacker #2 (scenario #1) Attacker #2 (scenario #2)
	States	29520	45980	59040	117260
	Transitions 259200	440924	518400	1029600
	Choices	141120	220220	282240	560560

Table 12 :

 12 The verification results in the presence of the insider and the external technical #1 attackers.

	Action/	Insider	Verification External-Technical Verification
	Criterion Attacker Time (secs)	Attacker #1	Time (secs)
	Φ 1	✓	0.109	✓	0.393
	Φ 2	✓	0.221	✓	0.491
	Φ 3	✓	0.301	✗	0.537

Table 13 :

 13 The verification results in the presence of the external technical attacker #2.

	Action/	External Technical	Verification	External Technical	Verification
	Criterion Attacker #2 (scenario #1) Time (secs) Attacker #2 (scenario #2) Time (secs)
	Φ 1	✗	0.222	✓	0.051
	Φ 2	✗	0.297	✓	0.077
	Φ 3	✗	0.311	✓	0.092
	and to 0.327 for the external-technical attacker #1. Further, Figure 12 the suc-
	cess of the social technical attacker for Φ 2 with a maximum probability value of 0.362
	and 0.404 for Φ 3 (right).

SSA stands for "Severity of Smart Attacks in Industrial Cyber Physical Systems."

https://s.campbellsci.com/documents/us/case-studies/64utah-SCADA.pdf

For the composition operators, we define the following semantic rules where P1 and P2 represent the parallel composition rules, COM is the communication one, N1 and N2 are the non-deterministic rules. Further, G1 and G2 represent the guarded choice derivation rules. Finally PB1 and PB2 are the derivation rules for the probabilistic choices. To simplify the derivation rules, we consider n 1 and n 2 two different nodes.

6.2 Transformation Function

[


Axel Hutt
email: axel.hutt@inria.fr

André Grüning

Alex Hansen

Thomas Hartung

Raina Robeva

Editorial: Machine Learning in Natural Complex Systems

Keywords: model improvement, learning rules, deep learning, data assimilation, big data

Editorial on the Research Topic

Machine Learning in Natural Complex Systems

For many decades, scientists strive to develop intelligent machines to reproduce or improve human intelligent actions. Machine Learning (ML), a research branch of artificial intelligence, aims to learn and simulate specific intelligent human actions and has been applied to a large variety of artificial and natural systems. At first glance, it is tempting to automize solving complex problems by machines. Specifically, in ML this is done by learning features of a data training data set, i.e., learning hidden relations in the data. Since the learned patterns and the subsequent prediction is based on the training set, the success of ML heavily depends on the training data. This renders the application of ML to natural systems rather challenging, since natural systems' dynamics are complex, and the training data set has to reflect the diverse dynamics. Typically, this renders the data set huge in size and thus such methods apply well to so-called Big Data. Examples for applications are visual pattern recognition, language processing and signal processing. Moreover, ML techniques compete with model approaches, which have built-in relations between system elements and which do not depend on specific training sets. In certain research fields, such as meteorology, system models and corresponding techniques are already so powerful that a benefit of ML is still unclear. However, recent techniques combine ML and models to achieve the best insight into the dynamics of systems. The present Research Topic collects work from a large variety of research fields on natural complex systems and provides a good up-to-date overview of the field of ML.

An important percentage of ML applications focuses on classification of datasets. In medical science, a combination of different data types has proven to improve patient classification and prediction. In Zhu et al., the authors have shown that a deep learning classification of both patient and radiograph variables allow to predict osteonecrosis and thus may prevent its aggravation at an early stage. Similarly, Xue et al. shows that the combination of diverse patient variables, such as level of cholesterol and patient age, permits to predict pulmonary complications after gastrointestinal surgery by ML techniques. The latter studies demonstrate that ML techniques permit predictions in patients with a very high success rate. In line with this approach, Liu G. Although classification tasks play an important role in current ML research, existing ML techniques may also serve as tools to achieve a different research goal. For instance, Wang et al. shows how ML techniques may assist to learn time-dependent neural activity in order to understand better the relation of neural activity to behavior. ML may also help to understand complex systems on the basis of incomplete observations. Herzog et al. demonstrate how to complete sparsely sampled mechanical cardiac dynamics to predict electric heart activity by employing a dynamical model. The combination of ML techniques and mathematical models, as in this latter work, is especially powerful and promises to boost theoretical models of complex systems. This is shown nicely as well in Kigure, where the author demonstrates a numerical speed-up in a computational fluid dynamics model by employing ML.

In recent years, experimental observation techniques have been improved and are providing more and more data with increased temporal and spatial resolution. This progress demands advanced analysis techniques. For instance, today it is possible to observe neural activity in brain tissue by electrode grids with a high spatial resolution. Since the corresponding observed time series are correlated by virtue of the increased resolution, Geddes et al. propose a new data analysis technique for multivariate signals to extract novel underlying dynamic features. However, an improved temporal resolution of observations also requests improved analysis techniques that take into account multiple time scales. To this end, Manneschi et al. propose an extended reservoir computing technique to better learn computationally observed time series. Moreover, new observational data may also exhibit sparse dynamics that represents an important challenge to existing ML techniques. Nascimento et al. investigates how various sparse dynamics models can be combined with a graphical approach on the basis of EEG data to retrieve valuable insights into the brain's network connectivity. These latter data evolve on a certain grid in space and/or time and may be used to identify hidden patterns of functional and effective connectivity of brain networks. However, this is more difficult in other data, such as the temporally-changing positions of single objects in an environment. The authors Fromreide and Hansen address such data and present a method to predict the motion of moving ships. They demonstrate how to introduce movement patterns dependent on the land/sea environment.

In data analysis, a first step identifies data properties which are then examined in subsequent steps. In order to extract knowledge from a dataset and learn more about the system under study, it may be beneficial to look for structural patterns in the data. For instance, certain symmetries in datasets may immediately indicate pieces of redundant information and permit a simplifying dimensionality reduction. Capobianco addresses this issue and argues that data symmetries may enhance ML performance. Moreover, it may be promising to define novel similarity measures in life science data which are adapted to the respective data type (e.g., genetic sequences, chromosome data or chemical structure formulas). In Münch et al., the authors present strategies and concepts how to employ data-driven similarity measures in ML.

In conclusion, the Research Topic Machine Learning in Natural Complex Systems showcases the powerful impact of ML on the study of complex systems and the enormous potential this approach holds for gaining further knowledge about the complexities of their dynamics. We trust that the readers will enjoy these articles as much as we did and hope that the collection will help generate further discussion and inspire further discoveries.

  et al. reviews ML techniques for epilepsy detection in electroencephalographic signals (EEG). Such latter techniques involve the additional complexity of a temporal sequence in the data compared to the temporally static data in the studies mentioned earlier. The authors of Liu J. et al. also consider EEG signals and demonstrate how to classify emotions by ML techniques. A different application is considered in Peng et al. considering observed time series in a meteorological model. Here, the authors successfully find relationships between the climate variables using ML on the basis of precipitation observations.

Frontiers in Applied Mathematics and Statistics | www.frontiersin.org

March 2022 | Volume 8 | Article 869999

AUTHOR CONTRIBUTIONS

All authors listed have made a substantial, direct, and intellectual contribution to the work and approved it for publication.

Conflict of Interest:

The authors declare that the research was conducted in the absence of any commercial or financial relationships that could be construed as a potential conflict of interest.

Publisher's Note: All claims expressed in this article are solely those of the authors and do not necessarily represent those of their affiliated organizations, or those of the publisher, the editors and the reviewers. Any product that may be evaluated in this article, or claim that may be made by its manufacturer, is not guaranteed or endorsed by the publisher.