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.
Exploiting maximum likelihood to improve network traffic deanonymization performances
Gian Luca Foresti, Axel De Nardin, Alessio Fiorin, Marino Miculan, and Claudio Piciarelli
Pairing an Autoencoder and a SF-SOINN for Implementing an Intrusion Detection System
Gabriele Voltan, Gian Luca Foresti, and Marino Miculan
In Proceedings of the Thematic Workshops co-located with the 3rd CINI National Lab AIIS Conference on Artificial Intelligence (Ital IA 2023), Pisa, Italy, May 29-30, 2023 2023
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.
Automated Verification of Telegram’s MTProto 2.0 in the Symbolic Model
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.
Composable partial multiparty session types for open systems
Claude Stolze, Marino Miculan, and Pietro Di Gianantonio
Attribute-based memory updates (AbU in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed systems, particularly suited for the IoT. It can be seen as a memory-based counterpart of attribute-based communication, keeping the simplicity of ECA rules.
Closure Hyperdoctrines
Davide Castelnovo, and Marino Miculan
In CALCO 2021 Conference Proceedings 2021
A time-series classification approach to shallow web traffic de-anonymization
Axel De Nardin, Marino Miculan, Claudio Piciarelli, and Gian Luca Foresti
In Proceedings of the Fifth Italian Conference on Cyber Security, ITASEC 2021 2021
We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern matching (RLPM) and graph simulation (GS). Being a unification of all these notions, LGS allows us to express directly also problems which are “mixed” instances of previous ones, and hence which would not fit easily in any of them. After the definition and some examples, we show that the problem of finding loose graph simulations is NP-complete, we provide formal translation of SGI, RLPM, and GS into LGSs, and we give the representation of a problem which extends both SGI and RLPM. Finally, we identify a subclass of the LGS problem that is polynomial.
First and Second International Workshops on Meta Models for Process Languages (MeMo), Selected Papers
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.
Open Transactions on Shared Memory
Marino Miculan, Marco Peressotti, and Andrea Toneguzzo
In Coordination Models and Languages - 17th IFIP WG 6.1 International Conference, COORDINATION 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings 2015
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.
Behavioural equivalences for coalgebras with unobservable moves
Tomasz Brengos, Marino Miculan, and Marco Peressotti
Journal of Logical and Algebraic Methods in Programming 2015
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.
PreProceedings of the 2nd International Workshop on Meta Models for Process Languages (MeMo 2015)
GSOS for non-deterministic processes with quantitative aspects
Marino Miculan, and Marco Peressotti
In Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014. 2014