{'fraction_non_alphanumeric': 0.05607727394687416, 'fraction_numerical': 0.009275940051362643, 'mean_word_length': 3.787064220183486, 'pattern_counts': {'":': 0, '<': 14, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 47, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards a formal notion of impact metric for cyber-physical attacks (full version)

Industrial facilities and critical infrastructures are transforming into"smart"environments that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components integrated in cyber-physical systems which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of the systems. We provide a formal compositional metric to estimate the impact of cyber-physical attacks targeting sensor devices of IoT systems formalised in a simple extension of Hennessy and Regan's Timed Process Language. Our impact metric relies on a discrete-time generalisation of Desharnais et al.'s weak bisimulation metric for concurrent systems. We show the adequacy of our definition on two different attacks on a simple surveillance system.


Introduction
The Internet of Things (IoT) is heavily affecting our daily lives in many domains, ranging from tiny wearable devices to large industrial systems with thousands of heterogeneous cyber and physical components that interact with each other.
Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow the latter to affect the computations of the former and vice versa. Historically, CPSs relied on proprietary technologies and were implemented as stand-alone networks in physically protected locations. However, the growing connectivity and integration of these systems has triggered a dramatic increase in the number of cyber-physical attacks [26], i.e., security breaches in cyberspace that adversely affect the physical processes, e.g., manipulating sensor readings and, in general, influencing physical processes to bring the system into a state desired by the attacker.
Cyber-physical attacks are complex and challenging as they usually cross the boundary between cyberspace and the physical world, possibly more than once [14]. Some notorious examples are: (i) the Stuxnet worm, which reprogrammed PLCs of nuclear centrifuges in Iran [9], (ii) the attack on a sewage treatment facility in Queensland, Australia, which manipulated the SCADA system to release raw sewage into local rivers [34], or the (iii) the recent BlackEnergy cyber-attack on the Ukrainian power grid, again compromising the SCADA system [18].
The points in common of these systems is that they are all safety critical and failures may cause catastrophic consequences. Thus, the concern for consequences at the physical level puts CPS security apart from standard IT security.
Timing is particularly relevant in CPS security because the physical state of a system changes continuously over time and, as the system evolves in time, some states might be more vulnerable to attacks than others [20]. For example, an attack launched when the target state variable reaches a local maximum (or minimum) may have a great impact on the whole system behaviour [21]. Also the duration of the attack is an important parameter to be taken into consideration in order to achieve a successful attack. For example, it may take minutes for a chemical reactor to rupture [37], hours to heat a tank of water or burn out a motor, and days to destroy centrifuges [9].
Actually, the estimation of the impact of cyber-physical attacks on the target system is crucial when protecting CPSs [13]. For instance, in industrial CPSs, before taking any countermeasure against an attack, engineers first try to estimate the impact of the attack on the system functioning (e.g., performance and security) and weight it against the cost of stopping the plant. If this cost is higher than the damage caused by the attack (as is sometimes the case), then engineers might actually decide to let the system continue its activities even under attack. Thus, once an attack is detected, impact metrics are necessary to quantify the perturbation introduced in the physical behaviour of the system under attack.
The goal of this paper is to lay theoretical foundations to provide formal instruments to precisely define the notion of impact of cyber-physical attack targeting physical devices, such as sensor devices of IoT systems. For that we rely on a timed generalisation of bisimulation metrics [8,7,39] to compare the behaviour of two systems up to a given tolerance, for time-bounded executions.
Weak bisimulation metric [8] allows us to compare two systems M and N , writing M ≃ p N , if the weak bisimilarity holds with a distance or tolerance p ∈ [0, 1], i.e., if M and N exhibit a different behaviour with probability p, and the same behaviour with probability 1 − p. A useful generalisation is the n-bisimulation metric [38] that takes into account bounded computations. Intuitively, the distance p is ensured only for the first n computational steps, for some n ∈ N. However, in timed systems it is desirable to focus on the passage of time rather than the number of computational steps. This would allow us to deal with situations where it is not necessary (or it simply does not make sense) to compare two systems "ad infinitum" but only for a limited amount of time.
Contribution. In this paper, we first introduce a general notion of timed bisimulation metric for concurrent probabilistic systems equipped with a discrete no-In order to make security assessments of our IoT systems, we adapt a wellknow approach called Generalized Non Deducibility on Composition (GNDC) [10] to compare the behaviour of an IoT system M with the behaviour of the same system under attack, written M A, for some arbitrary cyber-physical attack A. This comparison makes use of our timed bisimulation metric to evaluate not only the tolerance and the vulnerability of a system M with respect to a certain attack A, but also the impact of a successful attack in terms of the deviation introduced in the behaviour of the target system. In particular, we say that a system M tolerates an attack A if M A ≈ ∞ 0 M , i.e., the presence of A does not affect the behaviour of M ; whereas M is said to be vulnerable to A in the time interval m..n with impact p if m..n is the smallest interval such that M A ≈ m−1 0 M and M A ≈ k p M , for any k ≥ n, i.e., if the perturbation introduced by the attack A becomes observable in the m-th time slot and yields the maximum impact p in the n-th time slot. In the concluding discussion we will show that the temporal vulnerability window m..n provides several informations about the corresponding attack, such as stealthiness capability, duration of the physical effects of the attack, and consequent room for possible run-time countermeasures.
As a case study, we use our timed bisimulation metric to measure the impact of two different attacks injecting false positives and false negative, respectively, into a simple surveillance system expressed in our process calculus.
Outline. Section 2 formalises our timed bisimulation metrics in a general setting. Section 3 provides a simple calculus of IoT systems. Section 4 defines cyberphysical attacks together with the notions of tolerance and vulnerability w.r.t. an attack. In Section 5 we use our metrics to evaluate the impact of two attacks on a simple surveillance system. Section 6 draws conclusions and discusses related and future work. In this extended abstract proofs are omitted, full details of the proofs can be found in the Appendix.
In this section, we introduce timed bisimulation metrics as a general instrument to derive a notion of timed and approximate weak bisimulation between probabilistic systems equipped with a discrete notion of time. In Section 2.1, we recall the semantic model of nondeterministic probabilistic labelled transition systems; in Section 2.2, we present our metric semantics.

Nondeterministic Probabilistic Labelled Transition Systems
Nondeterministic probabilistic labelled transition systems (pLTS) [33] combine classic LTSs [19] and discrete-time Markov chains [15,35] to model, at the same time, reactive behaviour, nondeterminism and probability. We first provide the mathematical machinery required to define a pLTS.
The state space in a pLTS is given by a set T , whose elements are called processes, or terms. We use t, t ′ , .. to range over T . A (discrete) probability subdistribution over T is a mapping ∆ : T → [0, 1], with t∈T ∆(t) ∈ (0, 1]. We denote t∈T ∆(t) by | ∆ |, and we say that ∆ is a probability distribution if |∆|= 1. The support of ∆ is given by ⌈∆⌉ = {t ∈ T : ∆(t) > 0}. The set of all sub-distributions (resp. distributions) over T with finite support will be denoted with D sub (T ) (resp. D(T )). We use ∆, Θ, Φ to range over D sub (T ) and D(T ).
In Definition 1, we assume the presence of a special deadlocked term Dead ∈ T . Furthermore, we assume that the set of actions A contains at least two actions: τ and tick. The former to model internal computations that cannot be externally observed, while the latter denotes the passage of one time unit in a setting with a discrete notion of time [16]. In particular, tick is the only timed action in A.
We write t the set of the derivatives (i.e. distributions) reachable from term t through action α. We say that a pLTS is image-finite [17] if der (t, α) is finite for all t ∈ T and α ∈ A. In this paper, we will always work with image-finite pLTSs.
Weak transitions. As we are interested in developing a weak bisimulation metric, we need a definition of weak transition which abstracts away from τ -actions. In a probabilistic setting, the definition of weak transition is somewhat complicated by the fact that (strong) transitions take terms to distributions; consequently if we are to use weak transitions then we need to generalise transitions, so that they take (sub-)distributions to (sub-)distributions.
To this end, we need some extra notation on distributions. For a term t ∈ T , the point (Dirac) distribution at t, denoted t, is defined by t(t) = 1 and t(t ′ ) = 0 for all t ′ = t. Then, the convex combination i∈I p i · ∆ i of a family {∆ i } i∈I of (sub-)distributions, with I a finite set of indexes, p i ∈ (0, 1] and i∈I p i ≤ 1, is the (sub-)distribution defined by ( i∈I p i · ∆ i )(t) def = i∈I p i · ∆ i (t) for all t ∈ T . We write i∈I p i · ∆ i as p 1 · ∆ 1 + . . . + p n · ∆ n when I = {1, . . . , n}.

Timed Weak Bisimulation with Tolerance
In this section, we define a family of relations ≈ k p over T , with p ∈ [0, 1] and k ∈ N + ∪ {∞}, where, intuitively, t ≈ k p t ′ means that t and t ′ can weakly bisimulate each other with a tolerance p accumulated in k timed steps. This is done by introducing a family of pseudometrics m k : T × T → [0, 1] and defining t ≈ k p t ′ iff m k (t, t ′ ) = p. The pseudometrics m k will have the following properties for any t, t ′ ∈ T : (i) m k1 (t, t ′ ) ≤ m k2 (t, t ′ ) whenever k 1 < k 2 (tolerance monotonicity); (ii) m ∞ (t, t ′ ) = p iff p is the distance between t and t ′ as given by the weak bisimilarity metric in [8] in an untimed setting; (iii) m ∞ (t, t ′ ) = 0 iff t and t ′ are related by the standard weak probabilistic bisimilarity [30].
Let us recall the standard definition of pseudometric.
In order to define the family of functions m k , we define an auxiliary family of functions m k,h : T × T → [0, 1], with k, h ∈ N, quantifying the tolerance of the weak bisimulation after a sequence of computation steps such that: (i) the sequence contains exactly k tick-actions, (ii) the sequence terminates with a tick-action, (iii) any term performs exactly h untimed actions before the first tick-action, (iv) between any i-th and (i+1)-th tick-action, with 1 ≤ i < k, there are an arbitrary number of untimed actions.
The definition of m k,h relies on a timed and quantitative version of the classic bisimulation game: The tolerance between t and t ′ as given by m k,h (t, t ′ ) can be below a threshold ǫ ∈ [0, 1] only if each transition t α − → ∆ is mimicked by a weak transition t ′α = ⇒ Θ such that the bisimulation tolerance between ∆ and Θ is, in turn, below ǫ. This requires to lift pseudometrics over T to pseudometrics over (sub-)distributions in D sub (T ). To this end, we adopt the notions of matching [43] (also called coupling) and Kantorovich lifting [5].
Definition 3 (Matching). A matching for a pair of distributions (∆, Θ) ∈ D(T ) × D(T ) is a distribution ω in the state product space D(T × T ) such that: , for all t ∈ T , and -t∈T ω(t, t ′ ) = Θ(t ′ ), for all t ′ ∈ T . We write Ω(∆, Θ) to denote the set of all matchings for (∆, Θ).
A matching for (∆, Θ) may be understood as a transportation schedule for the shipment of probability mass from ∆ to Θ [43].
Note that since we are considering only distributions with finite support, the minimum over the set of matchings Ω(∆, Θ) used in Definition 4 is well defined.
Pseudometrics m k,h are inductively defined on k and h by means of suitable functionals over the complete lattice Notice that in this lattice, for each set D ⊆ [0, 1] T ×T , the supremum and infimum are defined as sup(D)(t, t ′ ) = sup d∈D d(t, t ′ ) and inf(D)(t, t ′ ) = inf d∈D d(t, t ′ ), for all t, t ′ ∈ T . The infimum of the lattice is the constant function zero, denoted by 0, and the supremum is the constant function one, denoted by 1.
Notice that all max in Definition 5 are well defined since the pLTS is imagefinite. Notice also that any strong transitions from t to a distribution ∆ is mimicked by a weak transition from t ′ , which, in general, takes to a sub-distribution Θ. Thus, process t ′ may not simulate t with probability 1− |Θ|.
Definition 6 (Timed weak bisimilarity metrics). The family of the timed weak bisimilarity metrics m k : (T × T ) → [0, 1] is defined for all k ∈ N by Note that any m k,h is obtained from m k−1 by one application of the functional B tick , in order to take into account the distance between terms introduced by the k-th tick-action, and h applications of the functional B, in order to lift such a distance to terms that take h untimed actions to be able to perform a tick-action. By taking sup h∈N m k,h we consider an arbitrary number of untimed steps.
The pseudometric property of m k is necessary to conclude that the tolerance between terms as given by m k is a reasonable notion of behavioural distance. Theorem 1. For any k ≥ 1, m k is a 1-bounded pseudometric.
Finally, everything is in place to define our timed weak bisimilarity ≈ k p with tolerance p ∈ [0, 1] accumulated after k time units, for k ∈ N ∪ {∞}.
Definition 7 (Timed weak bisimilarity with tolerance). Let t, t ′ ∈ T , k ∈ N and p ∈ [0, 1]. We say that t and t ′ are weakly bisimilar with a tolerance p, which accumulates in k timed actions, written t ≈ k p t ′ , if and only if m k (t, t ′ ) = p. Then, we write t ≈ ∞ p t ′ if and only if m ∞ (t, t ′ ) = p. Since the Kantorovich lifting K is monotone [29], it follows that both functionals B and B tick are monotone. This implies that, for any k ≥ 1, (m k,h ) h≥0 is a non-decreasing chain and, analogously, also (m k ) k≥0 is a non-decreasing chain, thus giving the following expected result saying that the distance between terms grows when we consider a higher number of tick computation steps.
Proposition 1 (Tolerance monotonicity). For all terms t, t ′ ∈ T and k 1 , k 2 ∈ N + with k 1 < k 2 , t ≈ k1 p1 t ′ and t ≈ k2 p2 t ′ entail p 1 ≤ p 2 . We conclude this section by comparing our behavioural distance with the behavioural relations known in the literature.
We recall that in [8] a family of relations ≃ p for untimed process calculi are defined such that t ≃ p t ′ if and only if t and t ′ weakly bisimulate each other with tolerance p. Of course, one can apply these relations also to timed process calculi, the effect being that timed actions are treated in exactly the same manner as untimed actions. The following result compares the behavioural metrics proposed in the present paper with those of [8], and with the classical notions of probabilistic weak bisimilarity [30] denoted ≈. Proposition 2. Let t, t ′ ∈ T and p ∈ [0, 1]. Then,

A Simple Probabilistic Timed Calculus for IoT Systems
In this section, we propose a simple extension of Hennessy and Regan's timed process algebra TPL [16] to express IoT systems and cyber-physical attacks. The goal is to show that timed weak bisimilarity with tolerance is a suitable notion to estimate the impact of cyber-physical attacks on IoT systems. Let us start with some preliminary notations.

Notation 1
We use x, x k for state variables, c, c k , for communication channels, z , z k for communication variables, s, s k for sensors devices, while o ranges over both channels and sensors. Values, ranged over by v, v ′ , belong to a finite set of admissible values V. We use u, u k for both values and communication variables. Given a generic set of names N , we write V N to denote the set of functions N → V assigning a value to each name in N . For m ∈ N and n ∈ N ∪ {∞}, we write m..n to denote an integer interval. As we will adopt a discrete notion of time, we will use integer intervals to denote time intervals.
State variables are associated to physical properties like temperature, pressure, etc. Sensor names are metavariables for sensor devices, such as thermometers and barometers. Please, notice that in cyber-physical systems, state variables cannot be directly accessed but they can only be tested via one or more sensors.
Definition 8 (IoT system). Let X be a set of state variables and S be a set of sensors. Let range : X → 2 V be a total function returning the range of admissible values for any state variable x ∈ X . An IoT system consists of two components: a physical environment ξ = ξ x , ξ m where: • ξ x ∈ V X is the physical state of the system that associates a value to each state variable in X , such that ξ x (x) ∈ range(x) for any x ∈ X , • ξ m : V X → S → D(V) is the measurement map that given a physical state returns a function that associates to any sensor in S a discrete probability distribution over the set of possible sensed values; -a logical (or cyber) component P that interacts with the sensors defined in ξ, and can communicate, via channels, with other cyber components.
We write ξ ⋊ ⋉ P to denote the resulting IoT system, and use M and N to range over IoT systems.
Let us now formalise the cyber component of an IoT system. Basically, we adapt Hennessy and Regan's timed process algebra TPL [16].
Definition 9 (Logics). Logical components of IoT systems are defined by the following grammar: The process tick.P sleeps for one time unit and then continues as P . We write P Q to denote the parallel composition of concurrent processes P and Q. The process ⌊pfx .P ⌋Q denotes prefixing with timeout. We recall that o ranges over both channel and sensor names. Thus, for instance, ⌊c!v.P ⌋Q sends the value v on channel c and, after that, it continues as P ; otherwise, if no communication partner is available within one time unit, it evolves into Q. The process ⌊c?(z).P ⌋Q is the obvious counterpart for channel reception. On the other hand, the process ⌊s?(z).P ⌋Q reads the sensor s, according to the measurement map of the systems, and, after that, it continues as P . The process ⌊s!v.P ⌋Q writes to the sensor s and, after that, it continues as P ; here, we wish to point out that this a malicious activity, as controllers may only access sensors for reading sensed data. Thus, the construct ⌊s!v.P ⌋Q serves to implement an integrity attack that attempts at synchronising with the controller of sensor s to provide a fake value v. In the following, we say that a process is honest if it never writes on sensors. The definition of honesty naturally lifts to IoT systems. In processes of the form tick.Q and ⌊pfx .P ⌋Q, the occurrence of Q is said to be time-guarded.
Recursive processes H ũ are defined via equations H(z 1 , . . . , z k ) = P , where (i) the tuple z 1 , . . . , z k contains all the variables that appear free in P , and (ii) P contains only time-guarded occurrences of the process identifiers, such as H itself (to avoid zeno behaviours). The two remaining constructs are standard; they model conditionals and channel restriction, respectively. Finally, we define how to compose IoT systems. For simplicity, we compose two systems only if they have the same physical environment.
Definition 10 (System composition). Let M 1 = ξ ⋊ ⋉ P 1 and M 2 = ξ ⋊ ⋉ P 2 be two IoT systems, and Q be a process whose sensors are defined in the physical environment ξ. We write: ; -M 1 \c as an abbreviation for ξ ⋊ ⋉ (P 1 \c).
We conclude this section with the following abbreviations that will be used in the rest of the paper. Notation 2 We write P \{c 1 , c 2 , . . . , c n }, or P \c, to mean P \c 1 \c 2 · · · \c n . For simplicity, we sometimes abbreviate both H(i) and H i with H i . We write pfx .P as an abbreviation for the process defined via the equation H = ⌊pfx .P ⌋H , where the process name H does not occur in P . We write tick k .P as a shorthand for tick.tick. . . . tick.P , where the prefix tick appears k ≥ 0 consecutive times. We write Dead to denote a deadlocked IoT system that cannot perform any action.

Probabilistic labelled transition semantics
As said before, sensors serve to observe the evolution of the physical state of an IoT system. However, sensors are usually affected by an error/noise that we represent in our measurement maps by means of discrete probability distributions. For this reason, we equip our calculus with a probabilistic labelled transition system. In the following, the symbol ǫ ranges over distributions on physical environments, whereas π ranges over distributions on (logical) processes. Thus, ǫ ⋊ ⋉ π The symbol γ ranges over distributions on IoT systems. In Table 1, we give a standard labelled transition system for logical components (timed processes), whereas in Table 2 we rely on the LTS of Table 1 to define a simple pLTS for IoT systems by lifting transition rules from processes to systems.
In Table 1, the meta-variable λ ranges over labels in the set {τ, tick, o!v, o?(z)}. Rule (Sync) serve to model synchronisation and value passing, on some name (for channel or sensor) o: if o is a channel then we have standard point-to-point communication, whereas if o is a sensor then this rule models an integrity attack on sensor s, as the controller is provided with a fake value v. The remaining rules are standard. The symmetric counterparts of rules (Sync) and (Par) are omitted.
According to Table 2, IoT systems may fire four possible actions ranged over by α. These actions represent: internal activities (τ ), the passage of time (tick), channel transmission (c!v) and channel reception (c?v).
Rules (Snd) and (Rcv) model transmission and reception on a channel c with an external system, respectively. Rule (SensRead) models the reading of the value detected at a sensor s according to the current physical environment ξ = ξ x , ξ m . In particular, this rule says that if a process P in a system ξ ⋊ ⋉ P reads a sensor s defined in ξ then it will get a value that may vary according to the probability distribution resulting by providing the state function ξ x and the sensor s to the measurement map ξ m .
Rule (Tau) lifts internal actions from processes to systems. This includes communications on channels and malicious accesses to sensors' controllers. Ac- Table 2. Probabilistic LTS for a IoT system ξ ⋊ ⋉ P with ξ = ξx, ξm cording to Definition 10, rule (Tau) models also channel communication between two parallel IoT systems sharing the same physical environment. A second lifting occurs in rule (Time) for timed actions tick. Here, ξ ′ denotes an admissible physical environment for the next time slot, nondeterministically chosen from the finite set next( ξ x , ξ m ). This set is defined as for any x ∈ X }. 3 As a consequence, the rules in Table 2 define an image-finite pLTS.
For simplicity, we abstract from the physical process behind our IoT systems.

Cyber-physical attacks on sensor devices
In this section, we consider attacks tampering with sensors by eavesdropping and possibly modifying the sensor measurements provided to the corresponding controllers. These attacks may affect both the integrity and the availability of the system under attack. We do not represent (well-known) attacks on communication channels as our focus is on attacks to physical devices and the consequent impact on the physical state. However, our technique can be easily generalised to deal with attacks on channels as well.
Definition 11 (Cyber-physical attack). A (pure) cyber-physical attack A is a process derivable from the grammar of Definition 9 such that: -A writes on at least one sensor; -A never uses communication channels.
In order to make security assessments on our IoT systems, we adapt a wellknown approach called Generalized Non Deducibility on Composition (GNDC) [10]. Intuitively, an attack A affects an honest IoT system M if the execution of the composed system M A differs from that of the original system M in an observable manner. Basically, a cyber-physical attack can influence the system under attack in at least two different ways: -The system M A might have non-genuine execution traces containing observables that cannot be reproduced by M ; here the attack affects the integrity of the system behaviour (integrity attack ).
-The system M might have execution traces containing observables that cannot be reproduced by the system under attack M A (because they are prevented by the attack); this is an attack against the availability of the system (DoS attack ). Now, everything is in place to provide a formal definition of system tolerance and system vulnerability with respect to a given attack. Intuitively, a system M tolerates an attack A if the presence of the attack does not affect the behaviour of M ; on the other hand M is vulnerable to A in a certain time interval if the attack has an impact on the behaviour of M in that time interval.
Definition 12 (Attack tolerance). Let M be a honest IoT system. We say that M tolerates an attack Definition 13 (Attack vulnerability and impact). Let M be a honest IoT system. We say that M is vulnerable to an attack A in the time interval m..n with impact p ∈ [0, 1], for m ∈ N + and n ∈ N + ∪{∞}, if m..n is the smallest time interval such that: Basically, the definition above says that if a system is vulnerable to an attack in the time interval m..n then the perturbation introduced by the attack starts in the m-th time slot and reaches the maximum impact in the n-th time slot.
The following result says that both notions of tolerance and vulnerability are suitable for compositional reasonings. More precisely, we prove that they are both preserved by parallel composition and channel restriction. Actually, channel restriction may obviously make a system less vulnerable by hiding channels.
Theorem 2 (Compositionality). Let M 1 = ξ ⋊ ⋉ P 1 and M 2 = ξ ⋊ ⋉ P 2 be two honest IoT systems with the same physical environment ξ, A an arbitrary attack, andc a set of channels.
Note that if an attack A is tolerated by a system M and can interact with a honest process P then the compound system M P may be vulnerable to A. However, if A does not write on the sensors of P then it is tolerated by M P as well. The bound p ′ ≤ (p 1 + p 2 − p 1 p 2 ) can be explained as follows.
The likelihood that the attack does not impact on Thus, the likelihood that the attack impacts neither on M 1 nor on M 2 is at least (1 − p 1 )(1 − p 2 ). Summarising, the likelihood that the attack impacts on at least one of the two systems M 1 and M 2 is at most An easy corollary of Theorem 2 allows us to lift the notions of tolerance and vulnerability from a honest system M to the compound systems M P , for a honest process P . Corollary 1. Let M be a honest system, A an attack,c a set of channels, and P a honest process that reads sensors defined in M but not those written by A.
-If M tolerates A then (M P )\c tolerates A.
-If M is vulnerable to A in the interval m..n with impact p, then (M P )\c is vulnerable to A in a time interval m ′ ..n ′ ⊆ m..n, with an impact p ′ ≤ p.

Attacking a smart surveillance system: A case study
Consider an alarmed ambient consisting of three rooms, r i for i ∈ {1, 2, 3}, each of which equipped with a sensor s i to detect unauthorised accesses. The alarm goes off if at least one of the three sensors detects an intrusion. The logics of the system can be easily specified in our language as follows: Intuitively, the process Sys is composed by three controllers, Ctrl i , one for each sensor s i , and a manager Mng that interacts with the controllers via private channels c i . The process Mng fires an alarm if at least one of the controllers signals an intrusion. As usual in this kind of surveillance systems, the alarm will keep going off for k instants of time after the last detected intrusion.
As regards the physical environment, the physical state ξ x : {r 1 , r 2 , r 3 } → {presence, absence} is set to ξ x (r i ) = absence, for any i ∈ {1, 2, 3}. Furthermore, let p + i and p − i be the probabilities of having false positives (erroneously detected intrusion) and false negatives (erroneously missed intrusion) at sensor s i 5 , respectively, for i ∈ {1, 2, 3}, the measurement function ξ m is defined as follows: Thus, the whole IoT system has the form ξ ⋊ ⋉ Sys, with ξ = ξ x , ξ m . We start our analysis studying the impact of a simple cyber-physical attack that provides fake false positives to the controller of one of the sensors s i . This attack affects the integrity of the system behaviour as the system under attack will fire alarms without any physical intrusion.
Example 1 (Introducing false positives). In this example, we provide an attack that tries to increase the number of false positives detected by the controller of some sensor s i during a specific time interval m..n, with m, n ∈ N, n ≥ m > 0. Intuitively, the attack waits for m − 1 time slots, then, during the time interval m..n, it provides the controller of sensor s i with a fake intrusion signal. Formally, In the following proposition, we use our metric to measure the perturbation introduced by the attack to the controller of a sensor s i by varying the time of observation of the system under attack.
, for j > n or j = ∞. By an application of Definition 13 we can measure the impact of the attack A fp to the (sub)systems ξ ⋊ ⋉ Ctrl i . Corollary 2. The IoT systems ξ ⋊ ⋉ Ctrl i are vulnerable to the attack A fp i, m, n in the time interval m..n with impact 1 − (p + i ) n−m+1 . Note that the vulnerability window m..n coincides with the activity period of the attack A fp . This means that the system under attack recovers its normal behaviour immediately after the termination of the attack. However, in general, an attack may impact the behaviour of the target system long after its termination.
Note also that the attack A fp i, m, n has an impact not only on the controller Ctrl i but also on the whole system ξ ⋊ ⋉ Sys. This because the process Mng will surely fire the alarm as it will receive at least one intrusion detection from Ctrl i . However, by an application of Corollary 1 we can prove that the impact on the whole system will not get amplified.
Proposition 4 (Impact of the attack A fp ). The system ξ ⋊ ⋉ Sys is vulnerable to the attack A fp i, m, n in a time interval m ′ ..n ′ ⊆ m..n with impact p ′ ≤ 1 − (p + i ) n−m+1 . Now, the reader may wonder what happens if we consider a complementary attack that provides fake false negatives to the controller of one of the sensors s i . In this case, the attack affects the availability of the system behaviour as the system will no fire the alarm in the presence of a real intrusion. This because a real intrusion will be somehow "hidden" by the attack.
Example 2 (Introducing false negatives). The goal of the following attack is to increase the number of false negatives during the time interval m..n, with n ≥ m > 0. Formally, the attack is defined as follows: In the following proposition, we use our metric to measure the deviation introduced by the attack A fn to the controller of a sensor s i . With no surprise we get a result that is the symmetric version of Proposition 3.
Proposition 5. Let ξ be an arbitrary physical state for the system M i = ξ ⋊ ⋉ Ctrl i , for i ∈ {1, 2, 3}. Then, Again, by an application of Definition 13 we can measure the impact of the attack A fn to the (sub)systems ξ ⋊ ⋉ Ctrl i . Corollary 3. The IoT systems ξ ⋊ ⋉ Ctrl i are vulnerable to the attack A fn i, m, n in the time interval m..n with impact 1 − (p − i ) n−m+1 . As our timed metric is compositional, by an application of Corollary 1 we can estimate the impact of the attack A fn to the whole system ξ ⋊ ⋉ Sys.
Proposition 6 (Impact of the attack A fn ). The system ξ ⋊ ⋉ Sys is vulnerable to the attack A fn i, m, n in a time interval

Conclusions, related and future work
We have proposed a timed generalisation of the n-bisimulation metric [38], called timed bisimulation metric, obtained by defining two functionals over the complete lattice of the functions assigning a distance in [0, 1] to each pair of systems: the former deals with the distance accumulated when executing untimed steps, the latter with the distance introduced by timed actions. We have used our timed bisimulation metrics to provide a formal and compositional notion of impact metric for cyber-physical attacks on IoT systems specified in a simple timed process calculus. In particular, we have focussed on cyber-physical attacks targeting sensor devices (attack on sensors are by far the most studied cyber-physical attacks [44]). We have used our timed weak bisimulation with tolerance to formalise the notions of attack tolerance and attack vulnerability with a given impact p. In particular, a system M is said to be vulnerable to an attack A in the time interval m..n with impact p if the perturbation introduced by A becomes observable in the m-th time slot and yields the maximum impact p in the n-th time slot. Here, we wish to stress that the vulnerability window m..n is quite informative. In practise, this interval says when an attack will produce observable effects on the system under attack. Thus, if n is finite we have an attack with temporary effects, otherwise we have an attack with permanent effects. Furthermore, if the attack is quick enough, and terminates well before the time instant m, then we have a stealthy attack that affects the system late enough to allow attack camouflages [14]. On the other hand, if at time m the attack is far from termination, then the IoT system under attack has good chances of undertaking countermeasures to stop the attack.
As a case study, we have estimated the impact of two cyber-physical attacks on sensors that introduce false positives and false negatives, respectively, into a simple surveillance system, affecting the integrity and the availability of the IoT system. Although our attacks are quite simple, the specification language and the corresponding metric semantics presented in the paper allow us to deal with smarter attacks, such as periodic attacks with constant or variable period of attack. Moreover, we can easily extend our threat model to recover (well-known) attacks on communication channels.

Related work.
We are aware of a number of works using formal methods for CPS security, although they apply methods, and most of the time have goals, that are quite different from ours.
Burmester et al. [3] employed hybrid timed automata to give a threat model based on the traditional Byzantine fault model for crypto-security. However, as remarked in [36], cyber-physical attacks and faults have inherently distinct characteristics. In fact, unlike faults, cyber-physical attacks may be performed over a significant number of attack points and in a coordinated way.
In [40], Vigo presented an attack scenario that addresses some of the peculiarities of a cyber-physical adversary, and discussed how this scenario relates to other attack models popular in the security protocol literature. Then, in [41,42] Vigo et al. proposed an untimed calculus of broadcasting processes equipped with notions of failed and unwanted communication. They focus on DoS attacks without taking into consideration timing aspects or attack impact.
Bodei et al. [1,2] proposed an untimed process calculus, IoT-LySa, supporting a control flow analysis that safely approximates the abstract behaviour of IoT systems. Essentially, they track how data spread from sensors to the logics of the network, and how physical data are manipulated.
Rocchetto and Tippenhaur [32] introduced a taxonomy of the diverse attacker models proposed for CPS security and outline requirements for generalised attacker models; in [31], they then proposed an extended Dolev-Yao attacker model suitable for CPSs. In their approach, physical layer interactions are modelled as abstract interactions between logical components to support reasoning on the physical-layer security of CPSs. This is done by introducing additional orthogonal channels. Time is not represented.
Nigam et al. [28] worked around the notion of Timed Dolev-Yao Intruder Models for Cyber-Physical Security Protocols by bounding the number of intruders required for the automated verification of such protocols. Following a tradition in security protocol analysis, they provide an answer to the question: How many intruders are enough for verification and where should they be placed? Their notion of time is somehow different from ours, as they focus on the time a message needs to travel from an agent to another. The paper does not mention physical devices, such as sensors and/or actuators.
Finally, Lanotte et al. [23] defined a hybrid process calculus to model both CPSs and cyber-physical attacks; they defined a threat model for cyber-physical attacks to physical devices and provided a proof methods to assess attack tolerance/vulnerability with respect to a timed trace semantics (no tolerance allowed).
Future work. Recent works [22,11,24,25,12] have shown that bisimulation metrics are suitable for compositional reasoning, as the distance between two complex systems can be often derived in terms of the distance between their components. In this respect, Theorem 2 and Corollary 1 allows us compositional reasonings when computing the impact of attacks on a target system, in terms of the impact on its sub-systems. We believe that this result can be generalised to estimate the impact of parallel attacks of the form A = A 1 . . . A k in terms of the impacts of each malicious module A i .
As future work, we also intend to adopt our impact metric in more involved languages for cyber-physical systems and attacks, such as the language developed in [23], with an explicit representation of physical processes via differential equations or their discrete counterpart, difference equations.

A Proofs
To prove Theorem 1 we need some preliminary results. The first of these results is Proposition 7 below, which states that the pseudometric property is preserved by function K, namely K(d) is a pseudometric over D(T ) whenever d is a pseudometric over T . Lemma 1 supports Proposition 7.
⊓ ⊔ Now we prove that for all k ≥ 1, the function m k is a fixed point of B.
for all t, t ′ ∈ T , is a complete lattice. Indeed, for each set D ⊆ [0, 1] T ×T , the supremum and infimum are defined as The infimum of the lattice is clearly B tick (m k−1 ). Being B monotone, by the Knaster-Tarski theorem B has a least fixed point. Since our pLTS is image-finite, and all transitions lead to distributions with finite support, with arguments analogous to those used in [38] it is possible to prove that B is continuous and its closure ordinal is ω, thus implying that its least fixed point is the supremum of the Kleene ascending chain B tick (m k−1 ) ⊑ B(B tick (m k−1 )) ⊑ B 2 (B tick (m k−1 )) ⊑ . . . = m k,0 ⊑ m k,1 ⊑ m k,2 ⊑ . . ., and, by definition, the supremum of this chain is m k . Now we exploit Lemma 2 to prove that for arbitrary processes t, t ′ ∈ T , process t ′ is able to simulate transitions of the form tα = ⇒ ∆, besides those of the form t α − → ∆, when α = tick. Lemma 3. Given two arbitrary terms t, t ′ ∈ T , whenever tα = ⇒ ∆ for α = tick, we have: We reason by induction on the length n of tα = ⇒ ∆.
The length of derivation tβ 1 = = ⇒ ∆ ′ is n − 1. Therefore, by the inductive hypothesis we have Notice that m k (t, t ′ ) < 1 and Equation 1 ensure that the set {Θ ′ | t ′β 1 = = ⇒ Θ ′ } is not be empty. Moreover, being β 1 = τ , we have that |∆ ′ |= 1 and, for each transition t ′β 1 = = ⇒ Θ ′ , also |Θ ′ |= 1. Therefore, the inductive hypothesis Equation 1 instantiates to inf The sub-distribution ∆ ′ is of the form ∆ ′ = i∈I p i · t i for suitable processes t ′ i and, by definition of transition relationβ 2 − − →, the transition ∆ ′β 2 − − → ∆ is derived from a β 2 -transition by some of the processes t i , namely I is partitioned into sets Let us fix an arbitrary transition t ′β 1 = = ⇒ Θ ′ (remember we argued above that it is not possible that there are none). The sub-distribution Θ ′ is of the form Θ ′ = j∈J q j · t ′ j , for suitable processes t ′ j . Then, J can be partitioned into sets J 1 ∪ J 2 such that for all j ∈ J 1 we have t ′ jβ 2 = = ⇒ Θ j for suitable distributions Θ j and for each j ∈ J 2 we have t ′ Since we had t ′β 1 = = ⇒ Θ ′ , we can conclude t ′α = ⇒ Θ. Notice that we are sure that there exist some some Θ ′ with t ′β 1 = = ⇒ Θ ′ for which J 1 = ∅.
Indeed, if for all Θ ′ with t ′β 1 = = ⇒ Θ ′ we had J 1 = ∅, this would cause tα = ⇒ , giving B(m k )(t, t ′ ) = 1 and contradicting B(m k )(t, t ′ ) = m k (t, t ′ ) < 1. We remark that in all cases where J 1 = ∅, the weak transition t ′α = ⇒ Θ is obtained by firstly choosing one of the available weak transitions labelledβ 1 from t ′ , namely t ′β 1 = = ⇒ Θ ′ , and, then, by choosing one of the available weak transitions labelled For the transition t ′β 1 = = ⇒ Θ ′ fixed above, let ω be one of the optimal matchings realising K(m k )(∆ ′ , Θ ′ ). We can rewrite the distributions ∆ ′ and Θ ′ as ∆ ′ = i∈I,j∈J ω(t i , t ′ j ) · t i and Θ ′ = i∈I,j∈J ω(t i , t ′ j ) · t ′ j . For all i ∈ I 1 and j ∈ J, define ∆ i,j = ∆ i . We can rewrite ∆ as ∆ = i∈I1,j∈J ω(t i , t ′ j )·∆ i,j . Analogously, for each j ∈ J 1 and i ∈ I we note that the transition q j t ′ Then we note that for all i ∈ I 1 and j ∈ J 1 , all transition t ′ Indeed, by definition of B, whenever t i and Equation 3 follows.
Consider any j ∈ J 1 and i ∈ I 1 . By Equation 3 and B(m k )(t i , t ′ j ) = m k (t i , t ′ j ), we infer that if if m k (t i , t ′ j ) < 1, then the set of the weak transitions labelled β 2 from t ′ j cannot be empty. For any transition t ′ iβ 2 = = ⇒ Θ i,j , let ω i,j be one of the optimal matchings realising K(m k )(∆ i,j , Θ i,j + (1− |Θ i,j |)Dead). Define ω ′ : T × T → [0, 1] as the function such that for arbitrary processes u, v ∈ T we have: To infer the proof obligation it is now enough to show that: To show property 1 we prove that the left marginal of ω ′ is ∆ + (1− |∆|)Dead. The proof that the right marginal is Θ + (1− |Θ|)Dead is analogous. For any process u = Dead we have with the third equality from the fact that ω i,j is a matching in Ω(∆ i,j , Θ i,j ), the fourth equality by J = J 1 ∪ J 2 and the fifth equality by j∈J ω(t i , t ′ j ) = p i and ∆ i,j = ∆ i . Consider now Dead. We have where the third equality by the fact that ω i,j is a matching in Ω(∆ i,j , Θ i,j ) and the fact that Θ i,j is a distribution, the fourth equality by J = J 1 ∪ J 2 , the fifth equality by j∈J ω(t i , t ′ j ) = p i and ∆ i,j = ∆ i and the last equality follows from i∈I1,j∈J ω(s i , t j ) = i∈I1 p i =|∆|. Summarising, for all processes u ∈ T we have proved that v∈T ω ′ (u, v) = (∆ + (1− |∆|)Dead)(u), thus confirming that the left marginal of ω ′ is ∆ + (1− | ∆|)Dead.
To prove (2), by looking at the definition of ω ′ given above we get that is the summation of the following values: Dead). By moving the first summand of the second, third and fourth items to the first item, we rewrite this summation as the summation of the following values: Dead). Since the function ω i,j was defined as one of the optimal matchings realising K(m k )(∆ i,j , Θ i,j + (1− | Θ i,j |)Dead), the first item can be rewritten as The second item is clearly less or equal than i∈I1,j∈J2 ω(t i , t ′ j ). The third item is clearly less or equal than i∈I2,j∈J1 ω(t i , t ′ j ). Finally, the last item is 0 since m k (Dead, Dead) = 0. Namely, the infimum for all t ′ ) is bounded by the summation of the following three values: Then, since K(m k )(∆ ′ , Θ ′ ) is the summation of the following values: we infer that the right hand side of Equation which, together with Equation 2 gives Equation 5, which concludes the proof.

⊓ ⊔
We are now ready to prove Theorem 1.
Proof (of Theorem 1). We have to prove that m k satisfies the three properties in Definition 2. Properties m k (t, t) = 0 and m k (t, t ′ ) = m k (t ′ , t) for all t, t ′ ∈ T are immediate. The interesting case is the triangular property m k (t, t ′ ) ≤ m k (t, t ′′ ) + m k (t ′′ , t ′ ) for all t, t ′ , t ′′ ∈ T . To this purpose, let us define the function m : We will prove that m = m k . By the definition of m, this gives m k (t, t ′ ) ≤ m k (t, t ′′ ) + m k (t ′′ , t ′ ) for all t ′′ ∈ T , thus confirming that also the triangular property holds for m k .
In order to prove m = m k , we observe first that relation m ⊑ m k follows immediately by the definition of m. It remains to prove m k ⊑ m. To this purpose we prove that: (i) m k is the least prefixed point of the functional B on the complete lattice ({d : T × T → [0, 1] : B tick (m k−1 ) ⊑ d}, ⊑), and (ii) m is a prefixed point of the same functional on the same lattice.
Let us start with property (i) By Lemma 2, m k is the least fixed point of the functional B, which is monotone and continuous in the lattice. This coincides with the least prefixed point.
Let us consider now (ii). We have to prove B(m) ⊑ m, namely, whenever m(t, t ′ ) < 1, then, for all α = tick we have To prove Equation 8 we distinguish two cases, namely m(t, t ′ ) = m k (t, t ′ ) and ). Since m(t, t ′ ) < 1, there exist terms t ′′ ∈ T with m k (t, t ′′ ) + m k (t ′′ , t ′ ) < 1, thus implying both m k (t, t ′′ ) < 1 and m k (t ′′ , t ′ ) < 1. By Lemma 3, from m k (t, t ′′ ) < 1 and t By the definition of m and Lemma 1 we have and, by definition of infimum, which gives Equation 8 and concludes the proof.
Proof (of Proposition 2). We prove the first item, then the second item follows by the first and the result t ≃ 0 t ′ iff t ≈ t ′ given in [8]. First we recall that t ≃ p t ′ iff m(t, t ′ ) = p, where m is the least fixed point (and also least prefixed point) in the lattice Proof (of Theorem 2). We prove the second item. The proof of the third item is analogous, then the first item is a consequence of the others. To prove the thesis we can prove that for all k ∈ IN we have Since ξ ⋊ ⋉ P 1 P 2 A can mimic all the behaviours by ξ ⋊ ⋉ P 1 P 2 , the distance m k (ξ ⋊ ⋉ P 1 P 2 A, ξ ⋊ ⋉ P 1 P 2 ) is given by the behaviours by ξ ⋊ ⋉ P 1 P 2 A that are not mimicked by ξ ⋊ ⋉ P 1 P 2 . Then, since ξ ⋊ ⋉ P 1 A P 2 A can mimic all the behaviours by ξ ⋊ ⋉ P 1 P 2 A, we have that thus implying that to have the proof obligation we can prove the stronger property More in general, we prove for arbitrary Q 1 and Q 2 , written also To this purpose, first we need to introduce the notion of congruence closure for m k as the quantitative analogue of the well-known concept of congruence closure of a process equivalence. We define the metric congruence closure of m k for operator w.r.t. the bound provided in Equation 9 as a function m assigning to each pair of systems a distance in [0, 1] given by We note that m satisfies by construction m( N 2 )). We note also that m satisfies by construction m ⊑ m k . It remains to show that m k ⊑ m, thus giving m k = m, and Equation 9 holds. Since m k is the least prefixed point of B over the lattice ({d : T × T → [0, 1] | B tick (m k−1 ) ⊑ d}, ⊑) to show m k ⊑ m it is enough to prove that m is a prefixed point of the same functional on the same lattice.
To prove that B(m) ⊑ m we need to show that m satisfies the transfer condition of the bisimulation metrics, namely for all systems M, M with m(M, M ′ ) < 1 and α = tick. This can be proved by applying the same arguments used to prove Proposition 3.2 in [11].
⊓ ⊔ Proof of Proposition 3 First we observe that in the evolution of both systems ξ ⋊ ⋉ Ctrl i and ξ ⋊ ⋉ Ctrl i A fp i, m, n it never happens that there are more than two instantaneous actions in between any two tick actions. This implies that for all j ∈ IN, system M reachable from ξ ⋊ ⋉ Ctrl i and system N reachable from ξ ⋊ ⋉ Ctrl i A fp i, m, n , we have m j (M, N ) = sup h∈IN m j,h (M, N ) = m j,2 (M, N ). Then, the proof follows from the following 7 properties, by observing that first item of the thesis follows from the property expressed by item 1 below and the second and third items of the thesis follow from the property expressed by item 7 below, when, respectively, j 1 = j − m + 1 and j 2 = m − 1.
For any j ∈ IN, it holds that: The seven properties above can be proved for all m j and m j,l by well founded induction over the relation ≺ defined as follows: Obviously, ≺ is irreflexive and there does not exist any infinite descending chain (the base case is m 0 ). The base case j = 0 is immediate since m 0 is the constant zero function 0 and 1 − (p + i ) 0 = 0. We consider the inductive step.
1. The thesis can be easily proved since Q can perform only tick actions and, intuitively, it does not affect the behaviour of P .
Similarly, for l = 0 and j > 1, whenever ξ ⋊ ⋉ P tick −−− → i∈I ξ i ⋊ ⋉ P i , then ξ ⋊ ⋉ P Q tick −−− → i∈I ξ i ⋊ ⋉ P i Q ′ with Q ′ = tick j ′ −1 .B i, n − m + 1 . Hence the thesis holds since, by induction on case item 1, for any h, it holds that m j−1,h (ξ i ⋊ ⋉ P i , ξ i ⋊ ⋉ P Q ′ ) = 0 thus implying that m j−1 (ξ i ⋊ ⋉ P i , ξ i ⋊ ⋉ P Q ′ ) = sup h∈IN ∞ m j−1,h (ξ i ⋊ ⋉ P i , ξ i ⋊ ⋉ P Q ′ ) = 0. are such that ξ ′ x (r i ) = absence. Indeed the attacker could force N to perform c i !on with probability equal to 1. If ξ ′ (r i ) = absence, then M will perform c i !on with probability p + i . Hence M does not simulate N with a probability 1 − p + i . Otherwise, if ξ ′ (r i ) = presence, then M will perform c i !on with probability 1 − p − i . Hence M does not simulate N with a probability p − i . Since 0 ≤ p + i , p − i < 1 2 , then 1 − p + i > p − i . The system N = ξ ⋊ ⋉ P Q minimises min 3. Define M = ξ ⋊ ⋉ P and N = ξ ⋊ ⋉ P Q.
Analogously to item 2, to prove B(m j,0 )(M, N ) = 1 − (p + i ) j−1 it is sufficient to prove the following two facts: max Since m j = m j,2 , analogously to item 2, to prove B(m j,1 )(M, N ) = 1−(p + i ) j it is sufficient to prove the following two facts: max M τ − →∆ min N τ = ⇒Θ K(m j,1 )(∆, Θ + (1− |Θ|)Dead) ≤ 1 − (p + i ) j max N τ − →Θ min M τ = ⇒∆ K(m j,1 )(∆ + (1− |∆|)Dead, Θ) = 1 − (p + i ) j . The interesting case is the second. Indeed, N is always able to simulate M by considering the case in which the controller reads the right value of the sensor and does not take the value provided by the attacker. The system N = ξ ⋊ ⋉ P Q can perform two transitions depending on the fact that the controller reads or not the fake value provided by the attacker. But, obviously, the system N = ξ ⋊ ⋉ P Q maximises which completes the proof. 5. The proof is similar to the proof of item 2. Indeed this case can be proved by induction on case item 4 if j = j 1 and j 2 = 1, and, on case item 7 if j 2 > 1. 6. The proof is similar to the proof of item 3. Indeed this case can be proved by induction on case item 5. 7. The proof is similar to the proof of item 4. Indeed this case can be proved by induction on case item 6. ⊓ ⊔ Proof of Proposition 5 The proof is similar to that of Proposition 3 by considering p − i instead of p + i , and, C . . . instead of B . . . . ⊓ ⊔