publications

Attribute-based memory Updates (Image 1in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed reactive systems, such as autonomic and smart IoT device ensembles. In this model, an event (e.g., an input from a sensor, or a device state update) can trigger an ECA rule, whose execution can cause the state update of (possibly) many remote devices at once; the latter are selected “on the fly” by means of predicates over their state, without the need of a central coordinating entity. However, the combination of different Image 1systems may yield unexpected interactions, e.g., when a new device is added to an existing secure system, potentially hindering the security of the whole ensemble of devices. This can be critical in the IoT, where smart devices are more and more pervasive in our daily life. In this paper, we consider the problem of ensuring security and safety requirements for Image 1systems (and, in turn, for IoT devices). The first are a form of noninterference, as they correspond to avoid forbidden information flows (e.g., information flows violating confidentiality); while the second are a form of non-interaction, as they correspond to avoid unintended executions (e.g., leading to erroneous/unsafe states). In order to formally model these requirements, we introduce suitable behavioral equivalences for Image 1. These equivalences are generalizations of hiding bisimilarity, i.e., a kind of weak bisimilarity where we can compare systems up to actions at different levels of security. Leveraging these behavioral equivalences, we propose (syntactic) sufficient conditions guaranteeing the requirements and, then, effective algorithms for statically verifying such conditions.

Adhesive categories, and variants such as 𝓜,𝓝-adhesive ones, marked a watershed moment for the algebraic approaches to the rewriting of graph-like structures, since they provide an abstract framework where many general results (on e.g. parallelism) could be recast and uniformly proved. However, often checking that a model satisfies the adhesivity properties is far from immediate. In this paper we present a new criterion giving a sufficient condition for 𝓜,𝓝-adhesivity, a generalisation of the original notion of adhesivity. To show the effectiveness of this criterion, we apply it to several existing categories of graph-like structures, including hypergraphs, various kinds of hierarchical graphs (a formalism that is notoriously difficult to fit in the mould of algebraic approaches to rewriting), and combinations of them.

MTProto 2.0 is the suite of security protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using ProVerif, a state-of-the-art symbolic security protocol verifier based on the Dolev-Yao model. We provide the first formal symbolic model of MTProto 2.0; in this model, we provide fully automated proofs of the soundness of authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy. At the same time, we discover that the rekeying protocol is vulnerable to an unknown key-share (UKS) attack. To achieve these results, we proceed in an incremental way: each protocol is examined in isolation, relying only on the guarantees provided by the previous ones and the robustness of the basic cryptographic primitives. The importance of this research is threefold. First, it proves the formal correctness of MTProto 2.0 with respect to most relevant security properties. Secondly, we isolate the aspects of cryptographic primitives that escape the symbolic model and thus require further investigation in the computational model. Finally, our modelisation can serve as a reference for the implementation and analysis of clients and servers.

In recent years, event-driven programming languages, in particular those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing ubiquitous and pervasive systems. These implementations are mostly centralized, where a single server (often in the cloud) collects and processes all the inputs from the environment. In fact, placing the computation on the nodes interacting with the environment requires suitable abstractions for effective communication and coordination of (possibly large) ensembles of these distributed components — abstractions that current ECA languages are still missing. To this end, in this paper we present AbU, a calculus for modeling and reasoning about ECA-based systems with attribute-based communication. The latter is an interaction model recently introduced for the coordination of (possibly large) families of nodes: communication is similar to broadcast but the actual receivers are selected on the spot, by means of predicates over nodes properties. Thus, the programmer can specify interactions between nodes in a declarative way, abstracting from details such as nodes identity, number, or even their existence, without the need for a central server: the computation is moved on the “edge”, thus improving reliability, scalability, privacy and security. After having defined syntax and formal semantics of AbU, we showcase its expressiveness by providing some example applications and the encoding of AbC, the archetypal calculus with attribute-based communication. Then, we focus on two key properties of reactive systems: stabilization (i.e., termination of internal steps) and confluence. For both these properties we provide formal semantic definition, sufficient syntactic conditions on AbU systems, and algorithms to statically check such conditions. Hence, AbU is both a basis for the formal analysis of event-driven architectures with attributed-based interaction, and a reference model for a full-fledged language for IoT and edge computing.

Abstract Recently, unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions) have been proposed with the aim of providing general results and tools. This paper provides two contributions in this respect. First, we present a general {GSOS} specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the {ULTraS} model, an extension of the usual {LTSs} where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function {GSOS} (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and {GSOS} formats (e.g. GSOS, Weighted GSOS, Segala-GSOS). The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.

Abstract In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endofunctors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule format, called MGSOS, representing abstract {GSOS} over Meas, and yielding fully abstract universal semantics, for which behavioral equivalence is a congruence. An {MGSOS} specification defines how semantics of processes are composed by means of measure terms, which are expressions specifically designed for describing finite measures. The syntax of these measure terms, and their interpretation as measures, are part of the {MGSOS} specification. We give two example applications, with a simple and neat {MGSOS} specification: a “quantitative CCS”, and a calculus of processes living in the plane R 2 whose communication rate depends on their distance. The approach we follow in these cases can be readily adapted to deal with other quantitative aspects.

We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on special order enriched categories, i.e. categories whose hom-sets are endowed with suitable complete orders. Using this structure we provide an abstract notion of saturation, which allows us to define various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences; on the other, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc.