Carla Piazza

Dalila Ressi, Alvise Spanò, Lorenzo Benetollo et al.

Smart contracts are central to a myriad of critical blockchain applications, from financial transactions to supply chain management. However, their adoption is hindered by security vulnerabilities that can result in significant financial losses. Most vulnerability detection tools and methods available nowadays leverage either static analysis methods or machine learning. Unfortunately, as valuable as they are, both approaches suffer from limitations that make them only partially effective. In this survey, we analyze the state of the art in machine-learning vulnerability detection for Ethereum smart contracts, by categorizing existing tools and methodologies, evaluating them, and highlighting their limitations. Our critical assessment unveils issues such as restricted vulnerability coverage and dataset construction flaws, providing us with new metrics to overcome the difficulties that restrain a sound comparison of existing solutions. Driven by our findings, we discuss best practices to enhance the accuracy, scope, and efficiency of vulnerability detection in smart contracts. Our guidelines address the known flaws while at the same time opening new avenues for research and development. By shedding light on current challenges and offering novel directions for improvement, we contribute to the advancement of secure smart contract development and blockchain technology as a whole.

Dalila Ressi, Riccardo Romanello, Sabina Rossi et al.

The increasing size of recently proposed Neural Networks makes it hard to implement them on embedded devices, where memory, battery and computational power are a non-trivial bottleneck. For this reason during the last years network compression literature has been thriving and a large number of solutions has been been published to reduce both the number of operations and the parameters involved with the models. Unfortunately, most of these reducing techniques are actually heuristic methods and usually require at least one re-training step to recover the accuracy. The need of procedures for model reduction is well-known also in the fields of Verification and Performances Evaluation, where large efforts have been devoted to the definition of quotients that preserve the observable underlying behaviour. In this paper we try to bridge the gap between the most popular and very effective network reduction strategies and formal notions, such as lumpability, introduced for verification and evaluation of Markov Chains. Elaborating on lumpability we propose a pruning approach that reduces the number of neurons in a network without using any data or fine-tuning, while completely preserving the exact behaviour. Relaxing the constraints on the exact definition of the quotienting method we can give a formal explanation of some of the most common reduction techniques.

Jane Hillston, Carla Piazza, Sabina Rossi

In this paper we present an information flow security property for stochastic, cooperating, processes expressed as terms of the Performance Evaluation Process Algebra (PEPA). We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: the first involves a single bisimulation-like equivalence check, while the second is formulated in terms of unwinding conditions. The observation equivalence at the base of our definition relies on the notion of lumpability and ensures that, for a secure process P, the steady state probability of observing the system being in a specific state P' is independent from its possible high level interactions.