Showing 1–13 of 13 results for author: Merro, M

Measuring Robustness in Cyber-Physical Systems under Sensor Attacks

Authors: Jian Xiang, Ruggero Lanotte, Simone Tini, Stephen Chong, Massimo Merro

Abstract: This paper contributes a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions, quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is w… ▽ More This paper contributes a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions, quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is with respect to the specified postcondition, and (2) how strong the specified precondition is with respect to the weakest precondition of the system needed to ensure the specified postcondition holds. We introduce two notions, forward and backward robustness, to characterize the robustness of a system against sensor attacks as the loss of safety. To reason about robustness, we introduce two simulation distances, forward and backward simulation distances, which are defined based on the behavioral distances between the original system and the system with compromised sensors. Forward and backward distances, respectively, characterize upper bounds of the degree of forward and backward safety loss caused by the sensor attacks. We verify the two simulation distances by expressing them as modalities, i.e., formulas of differential dynamic logic, and develop an ad-hoc proof system to reason with such formulas. We showcase our formal notions and reasoning techniques on two non-trivial case studies: an autonomous vehicle that needs to avoid collision and a water tank system. △ Less

Submitted 9 March, 2024; originally announced March 2024.

Comments: Preprint submitted to Elsevier

Runtime Enforcement of Programmable Logic Controllers

Authors: Ruggero Lanotte, Massimo Merro, Andrei Munteanu

Abstract: With the advent of Industry 4.0, industrial facilities and critical infrastructures are transforming into an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, increasingly interconnected and therefore exposed to cyber-physical attacks, i.e., security breaches in cyberspace that may adversely affect the physical processes underlying industrial control… ▽ More With the advent of Industry 4.0, industrial facilities and critical infrastructures are transforming into an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, increasingly interconnected and therefore exposed to cyber-physical attacks, i.e., security breaches in cyberspace that may adversely affect the physical processes underlying industrial control systems. In this paper, we propose a formal approach based on runtime enforcement to ensure specification compliance in networks of controllers, possibly compromised by colluding malware that may tamper with actuator commands, sensor readings, and inter-controller communications. Our approach relies on an ad-hoc sub-class of Ligatti et al.'s edit automata to enforce controllers represented in Hennessy and Regan's Timed Process Language. We define a synthesis algorithm that, given an alphabet $P$ of observable actions and a timed correctness property $e$, returns a monitor that enforces the property $e$ during the execution of any (potentially corrupted) controller with alphabet $P$, and complying with the property $e$. Our monitors correct and suppress incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical requirements, such as transparency and soundness, the proposed enforcement enjoys deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers. Finally, we test the proposed enforcement mechanism on a non-trivial case study, taken from the context of industrial water treatment systems, in which the controllers are injected with different malware with different malicious goals. △ Less

Submitted 18 November, 2021; v1 submitted 22 May, 2021; originally announced May 2021.

A process calculus approach to correctness enforcement of PLCs (full version)

Authors: Ruggero Lanotte, Massimo Merro, Andrei Munteanu

Abstract: We define a simple process calculus, based on Hennessy and Regan's Timed Process Language, for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specifications compliance. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/d… ▽ More We define a simple process calculus, based on Hennessy and Regan's Timed Process Language, for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specifications compliance. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/drop actuator commands and inter-controller communications. Then, we strengthen the capabilities of our monitors by allowing the insertion of actions to mitigate malware activities. This gives us deadlock-freedom monitoring: malware may not drag monitored controllers into deadlock states. △ Less

Submitted 11 September, 2020; v1 submitted 18 July, 2020; originally announced July 2020.

Comments: 21-st Italian Conference on Theoretical Computer Science (ICTCS 2020). CEUR Workshop Proceedings

A Formal Approach to Physics-Based Attacks in Cyber-Physical Systems (Extended Version)

Authors: Ruggero Lanotte, Massimo Merro, Andrei Munteanu, Luca Viganò

Abstract: We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1)~We define a hybrid pro… ▽ More We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1)~We define a hybrid process calculus to model both CPSs and physics-based attacks. (2)~We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands in order to drive a CPS into an undesired state, and we provide the means to assess attack tolerance/vulnerability with respect to a given attack. (3)~We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. (4)~We illustrate our definitions and results by formalising a non-trivial running example in Uppaal SMC, the statistical extension of the Uppaal model checker; we use Uppaal SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts. △ Less

Submitted 22 May, 2021; v1 submitted 12 February, 2019; originally announced February 2019.

Comments: This document extends the paper "A Formal Approach to Physics-Based Attacks in Cyber-Physical Systems" that will appear in ACM Transactions on Privacy and Security by providing proofs that are worked out in full details. arXiv admin note: text overlap with arXiv:1611.01377

Journal ref: ACM Trans. Priv. Secur. 23(1): 3:1-3:41 (2020)

Towards a formal notion of impact metric for cyber-physical attacks (full version)

Authors: Ruggero Lanotte, Massimo Merro, Simone Tini

Abstract: 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 cor… ▽ More 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. △ Less

Submitted 27 June, 2018; originally announced June 2018.

Equational Reasonings in Wireless Network Gossip Protocols

Authors: Ruggero Lanotte, Massimo Merro, Simone Tini

Abstract: Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout large-scale networks. In this paper, we propose a compositional analysis technique to study formal probabilistic models of gossip protocols expressed in a simple probabilistic timed process calculus for wireless sensor networks. We equip the calculus with a simulation theory to compare pro… ▽ More Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout large-scale networks. In this paper, we propose a compositional analysis technique to study formal probabilistic models of gossip protocols expressed in a simple probabilistic timed process calculus for wireless sensor networks. We equip the calculus with a simulation theory to compare probabilistic protocols that have similar behaviour up to a certain tolerance. The theory is used to prove a number of algebraic laws which revealed to be very effective to estimate the performances of gossip networks, with and without communication collisions, and randomised gossip networks. Our simulation theory is an asymmetric variant of the weak bisimulation metric that maintains most of the properties of the original definition. However, our asymmetric version is particularly suitable to reason on protocols in which the systems under consideration are not approximately equivalent, as in the case of gossip protocols. △ Less

Submitted 27 September, 2018; v1 submitted 11 July, 2017; originally announced July 2017.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 3 (September 28, 2018) lmcs:3845

A Probabilistic Calculus of Cyber-Physical Systems

Authors: Ruggero Lanotte, Massimo Merro, Simone Tini

Abstract: We propose a hybrid probabilistic process calculus for modelling and reasoning on cyber-physical systems (CPSs). The dynamics of the calculus is expressed in terms of a probabilistic labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based probabilistic behavioural semantics which supports compositional reasonings. For a more careful comparison between CP… ▽ More We propose a hybrid probabilistic process calculus for modelling and reasoning on cyber-physical systems (CPSs). The dynamics of the calculus is expressed in terms of a probabilistic labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based probabilistic behavioural semantics which supports compositional reasonings. For a more careful comparison between CPSs, we provide two compositional probabilistic metrics to formalise the notion of behavioural distance between systems, also in the case of bounded computations. Finally, we provide a non-trivial case study, taken from an engineering application, and use it to illustrate our definitions and our compositional behavioural theory for CPSs. △ Less

Submitted 27 April, 2020; v1 submitted 7 July, 2017; originally announced July 2017.

Comments: arXiv admin note: text overlap with arXiv:1612.00484

A Calculus of Cyber-Physical Systems

Authors: Ruggero Lanotte, Massimo Merro

Abstract: We propose a hybrid process calculus for modelling and reasoning on cyber-physical systems (CPS{s}). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which support compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial cas… ▽ More We propose a hybrid process calculus for modelling and reasoning on cyber-physical systems (CPS{s}). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which support compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study. △ Less

Submitted 7 July, 2018; v1 submitted 1 December, 2016; originally announced December 2016.

Comments: 11th International Conference on Language and Automata Theory and Applications. arXiv admin note: text overlap with arXiv:1611.01377

A Formal Approach to Cyber-Physical Attacks

Authors: Ruggero Lanotte, Massimo Merro, Riccardo Muradore, Luca Viganò

Abstract: We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and cyber-physical attacks. We focus on %a formal treatment of both integrity and DoS attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are threefold: (1) we define a hybrid process calculus to model both CPSs and cyber-physical a… ▽ More We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and cyber-physical attacks. We focus on %a formal treatment of both integrity and DoS attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are threefold: (1) we define a hybrid process calculus to model both CPSs and cyber-physical attacks; (2) we define a threat model of cyber-physical attacks and provide the means to assess attack tolerance/vulnerability with respect to a given attack; (3) we formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. We illustrate definitions and results by means of a non-trivial engineering application. △ Less

Submitted 21 April, 2017; v1 submitted 4 November, 2016; originally announced November 2016.

A Semantic Theory of the Internet of Things

Authors: Valentina Castiglioni, Ruggero Lanotte, Massimo Merro

Abstract: We propose a process calculus for modelling systems in the Internet of Things paradigm. Our systems interact both with the physical environment, via sensors and actuators, and with smart devices, via short-range and Internet channels. The calculus is equipped with a standard notion of bisimilarity which is a fully abstract characterisation of a well-known contextual equivalence. We use our semanti… ▽ More We propose a process calculus for modelling systems in the Internet of Things paradigm. Our systems interact both with the physical environment, via sensors and actuators, and with smart devices, via short-range and Internet channels. The calculus is equipped with a standard notion of bisimilarity which is a fully abstract characterisation of a well-known contextual equivalence. We use our semantic proof-methods to prove run-time properties as well as system equalities of non-trivial IoT systems. △ Less

Submitted 23 February, 2016; v1 submitted 16 October, 2015; originally announced October 2015.

Comments: The contribution of Valentina Castiglioni is limited to an early writing of some of the proofs in the Appendix

Semantics for Locking Specifications

Authors: Michael Ernst, Damiano Macedonio, Massimo Merro, Fausto Spoto

Abstract: To prevent concurrency errors, programmers need to obey a locking discipline. Annotations that specify that discipline, such as Java's @GuardedBy, are already widely used. Unfortunately, their semantics is expressed informally and is consequently ambiguous. This article highlights such ambiguities and formalizes the semantics of @GuardedBy in two alternative ways, building on an operational semant… ▽ More To prevent concurrency errors, programmers need to obey a locking discipline. Annotations that specify that discipline, such as Java's @GuardedBy, are already widely used. Unfortunately, their semantics is expressed informally and is consequently ambiguous. This article highlights such ambiguities and formalizes the semantics of @GuardedBy in two alternative ways, building on an operational semantics for a small concurrent fragment of a Java-like language. It also identifies when such annotations are actual guarantees against data races. Our work aids in understanding the annotations and supports the development of sound formal tools that verify or infer such annotations. △ Less

Submitted 15 November, 2015; v1 submitted 21 January, 2015; originally announced January 2015.

Modelling MAC-Layer Communications in Wireless Systems

Authors: Andrea Cerone, Matthew Hennessy, Massimo Merro

Abstract: We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual equivalence to compare the external behaviour of such wireless networks. Further, we construct an extensional LTS (labelled transition system) which… ▽ More We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual equivalence to compare the external behaviour of such wireless networks. Further, we construct an extensional LTS (labelled transition system) which models the activities of stations that can be directly observed by the external environment. Standard bisimulations in this LTS provide a sound proof method for proving systems contextually equivalence. We illustrate the usefulness of the proof methodology by a series of examples. Finally we show that this proof method is also complete, for a large class of systems. △ Less

Submitted 30 March, 2015; v1 submitted 3 November, 2014; originally announced November 2014.

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 1 (March 31, 2015) lmcs:1138

A Semantic Analysis of Key Management Protocols for Wireless Sensor Networks

Authors: Francesco Ballardin, Damiano Macedonio, Massimo Merro, Mattia Tirapelle

Abstract: We propose a simple timed broadcasting process calculus for modelling wireless network protocols. The operational semantics of our calculus is given in terms of a labelled transition semantics which is used to derive a standard (weak) bi-simulation theory. Based on our simulation theory, we reformulate Gorrieri and Martinelli's timed Generalized Non-Deducibility on Compositions (tGNDC) scheme, a w… ▽ More We propose a simple timed broadcasting process calculus for modelling wireless network protocols. The operational semantics of our calculus is given in terms of a labelled transition semantics which is used to derive a standard (weak) bi-simulation theory. Based on our simulation theory, we reformulate Gorrieri and Martinelli's timed Generalized Non-Deducibility on Compositions (tGNDC) scheme, a well-known general framework for the definition of timed properties of security protocols. We use tGNDC to perform a semantic analysis of three well-known key management protocols for wireless sensor networks: μTESLA, LEAP+ and LiSP. As a main result, we provide a number of attacks to these protocols which, to our knowledge, have not yet appeared in the literature. △ Less

Submitted 23 September, 2011; originally announced September 2011.

Comments: 51 pages