Massimo Merro

I&C Journal 2021 Journal Article

A probabilistic calculus of cyber-physical systems

• Ruggero Lanotte
• Massimo Merro
• Simone Tini

Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow physical processes to affect computations and vice versa. Although CPSs can be found in several real-world domains, their verification often relies on simulation test systems rather than formal methodologies. We propose a hybrid probabilistic process calculus for modelling and reasoning on 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.

TCS Journal 2021 Journal Article

A process calculus approach to detection and mitigation of PLC malware

• Ruggero Lanotte
• Massimo Merro
• Andrei Munteanu

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 specification compliance at runtime. 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. Our enforcing monitors represent a formal mechanism for prompt detection of malicious activities within PLCs. Finally, we illustrate our results by implementing in Simulink a non-trivial Water Transmission Network (WTN) system, and testing the effectiveness of our monitors in detecting and mitigating three different attacks targeting the PLCs of our WTN.

FormaliSE Conference 2020 Conference Paper

Impact Analysis of Cyber-Physical Attacks on a Water Tank System via Statistical Model Checking

• Andrei Munteanu
• Michele Pasqua
• Massimo Merro

Cyber-Physical Systems (CPSs) are integrations of distributed computing systems with physical processes that monitor and control entities in a physical environment. Although the range of their applications include several critical domains, the current trend is to verify CPSs with simulation-test systems rather than formal methodologies. In this paper, we test the effectiveness of statistical model checking, within the MODEST TOOLSET, when analyzing the security of a non-trivial quadruple-tank water system equipped with an ad-hoc intrusion detection system (IDS) capable of mitigating attacks. Our goal is to evaluate the impact of three carefully chosen cyber-physical attacks, i. e. , attacks targeting sensors and/or actuators of the system with potential consequences on the safety of the inner physical process. Our security analysis estimates both the physical impact of the attacks and the performance of the proposed IDS. CCS CONCEPTS•Computer systems organization $\rightarrow$ Sensors and actuators; •Software and its engineering $\rightarrow$ Model checking.

I&C Journal 2018 Journal Article

A semantic theory of the Internet of Things

• Ruggero Lanotte
• Massimo Merro

We propose a process calculus for modelling and reasoning on 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 labelled bisimilarity which is proved to be a coinductive characterisation of a well-known contextual equivalence. We use our semantic proof-methods to prove run-time properties of a non-trivial case study as well as system equalities.

MFCS Conference 2017 Conference Paper

Compositional Weak Metrics for Group Key Update

• Ruggero Lanotte
• Massimo Merro
• Simone Tini

We investigate the compositionality of both weak bisimilarity metric and weak similarity quasi- metric semantics with respect to a variety of standard operators, in the context of probabilistic process algebra. We show how compositionality with respect to nondeterministic and probabilistic choice requires to resort to rooted semantics. As a main application, we demonstrate how our results can be successfully used to conduct compositional reasonings to estimate the performances of group key update protocols in a multicast setting.

TCS Journal 2011 Journal Article

A timed calculus for wireless systems

• Massimo Merro
• Francesco Ballardin
• Eleonora Sibilio

We propose a timed broadcasting process calculus for wireless systems where time-consuming communications are exposed to collisions. The operational semantics of our calculus is given in terms of a labelled transition system. The calculus enjoys a number of desirable time properties such as (i) time determinism: the passage of time is deterministic; (ii) patience: devices will wait indefinitely until they can communicate; (iii) maximal progress: data transmissions cannot be delayed, they must occur as soon as a possibility for communication arises. We use our calculus to model and study MAC-layer protocols with a special emphasis on collisions and security. The main behavioural equality of our calculus is a timed variant of barbed congruence, a standard branching-time and contextually-defined program equivalence. As an efficient proof method for timed barbed congruence we define a labelled bisimilarity. We then apply our bisimulation proof-technique to prove a number of algebraic laws.

I&C Journal 2009 Journal Article

An Observational Theory for Mobile Ad Hoc Networks (full version)

• Massimo Merro

We propose a process calculus to study the behavioural theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of (weak) simulation and bisimulation for ad hoc networks. The labelled bisimilarity completely characterises reduction barbed congruence, a standard branching-time and contextually-defined program equivalence. We then use our (bi)simulation proof method to formally prove a number of non-trivial properties of ad hoc networks.

I&C Journal 2005 Journal Article

Communication and mobility control in boxed ambients

• Michele Bugliesi
• Silvia Crafa
• Massimo Merro
• Vladimiro Sassone

Boxed Ambients (BA) replace Mobile Ambients’ open capability with communication primitives acting across ambient boundaries. The expressiveness of the new communication model is achieved at the price of communication interferences whose resolution requires synchronisation of activities at multiple, distributed locations. We study a variant of BA aimed at controlling communication as well as mobility interferences. Our calculus modifies the communication mechanism of BA, and introduces a new form of co-capability, inspired from Safe Ambients (SA) (with passwords), that registers incoming agents with the receiver ambient while at the same time performing access control. We prove that the new calculus has a rich semantics theory, including a sound and complete coinductive characterisation, and an expressive, yet simple type system. Through a set of examples, and an encoding, we characterise its expressiveness with respect to both BA and SA.

TCS Journal 2004 Journal Article

Towards a behavioural theory of access and mobility control in distributed systems

• Matthew Hennessy
• Massimo Merro
• Julian Rathke

We define a typed bisimulation equivalence for the language DPI, a distributed version of the π-calculus in which processes may migrate between dynamically created locations. It takes into account resource access policies, which can be implemented in DPI using a novel form of dynamic capability types. The equivalence, based on typed actions between configurations, is justified by showing that it is fully abstract with respect to a natural distributed version of a contextual equivalence. In the second part of the paper we study the effect of controlling the migration of processes. This affects the ability to perform observations at specific locations, as the observer may be denied access. We show how the typed actions can be modified to take this into account, and generalise the full-abstraction result to this more delicate scenario.

I&C Journal 2002 Journal Article

Aliasing Models for Mobile Objects

• Uwe Nestmann
• Hans Hüttel
• Josva Kleist
• Massimo Merro

In Obliq, a lexically scoped, distributed, object-oriented programming language, object migration was suggested as the creation of a copy of the state of an object at the target site, followed by turning the object itself into an alias, also called surrogate, for the remote copy. We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a typed distribution-free subset of Obliq, and provide four different configuration-style semantics, which only differ in the respective aliasing model. We show that two of the semantics, one of which matches Obliq's implementation, render migration unsafe, while our new proposal allows for safe migration at least for a large class of program contexts. In addition, we propose a type system that allows a programmer to statically guarantee that programs belong to that class. Our work suggests a straightforward repair of Obliq's aliasing model.

I&C Journal 2002 Journal Article

Mobile Objects as Mobile Processes

• Massimo Merro
• Josva Kleist
• Uwe Nestmann

Obliq is a lexically scoped, distributed, object-based programming language. In Obliq, the migration of an object is proposed as creating a clone of the object at the target site, whereafter the original object is turned into an alias for the clone. Obliq has only an informal semantics, so there is no proof that this style of migration is safe, i. e. , transparent to object clients. In previous work, we introduced Ø, an abstraction of Obliq, where, by lexical scoping, sites have been abstracted away. We used Ø in order to exhibit how the semantics behind Obliq's implementation renders migration unsafe. We also suggested a modified semantics that we conjectured instead to be safe. In this paper, we rewrite our modified semantics of Ø in terms of the π-calculus, and we use it to formally prove the correctness of object surrogation, the abstraction of object migration in Ø.

I&C Journal 2002 Journal Article

Mobile Objects as Mobile Processes

• Massimo Merro
• Josva Kleist
• Uwe Nestmann