Letterio Galletta

Luca Pennella, Pietro Saggese, Fabio Pinelli et al.

Decentralized Finance (DeFi) applications introduce novel financial instruments replicating and extending traditional ones through blockchain-based smart contracts. Among these applications, DeFi derivatives protocols enable the creation and trading of decentralized derivative instruments whose value depends on underlying cryptoassets, indices, or other reference variables. Despite their growing significance, however, they remain relatively understudied compared to other DeFi protocols, such as lending protocols and decentralized exchanges. This paper systematically analyzes DeFi derivatives protocols, categorized into perpetuals, options, and synthetics, with the aim of comparing their instrument structures, protocol mechanisms, operational dynamics, and economic agents. We provide a formal characterization of the main classes of decentralized derivative instruments and develop a protocol-agnostic framework that connects instrument-level specifications, market-state variables, and protocol-level mechanisms. We complement the analytical framework with numerical simulations that evaluate how derivative positions evolve under varying economic conditions, including changes in underlying asset prices, volatility, protocol-specific fees, and leverage. Overall, this study provides a structured analytical framework for understanding and comparing the design and functioning of decentralized finance derivatives protocols.

Lorenzo Ceragioli, Pierpaolo Degano, Letterio Galletta et al.

In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange environments as a formal setting where agents specify and obey exchange policies, which are declarative statements about what resources they offer and what they require in return. Furthermore, we introduce a decidable extension of the computational fragment of linear logic as a fundamental tool for representing exchange environments and studying their dynamics in terms of provability.

Letterio Galletta, Fabio Pinelli

Blockchain technology has been successfully exploited for deploying new economic applications. However, it has started arousing the interest of malicious actors who deliver scams to deceive honest users and to gain economic advantages. Ponzi schemes are one of the most common scams. Here, we present a classifier for detecting smart Ponzi contracts on Ethereum, which can be used as the backbone for developing detection tools. First, we release a labelled data set with 4422 unique real-world smart contracts to address the problem of the unavailability of labelled data. Then, we show that our classifier outperforms the ones proposed in the literature when considering the AUC as a metric. Finally, we identify a small and effective set of features that ensures a good classification quality and investigate their impacts on the classification using eXplainable AI techniques.

Matteo Busi, Job Noorman, Jo Van Bulck et al.

Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features, brings a risk of introducing new such side-channel attacks. This paper studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. We propose to use full abstraction as a formal criterion for the security of a processor extension, and we instantiate that criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility of these enclaves. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor, and evaluate the cost of our design in terms of performance and hardware size.

Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Decentralized blockchain platforms have enabled the secure exchange of crypto-assets without the intermediation of trusted authorities. To this purpose, these platforms rely on a peer-to-peer network of byzantine nodes, which collaboratively maintain an append-only ledger of transactions, called blockchain. Transactions represent the actions required by users, e.g. the transfer of some units of crypto-currency to another user, or the execution of a smart contract which distributes crypto-assets according to its internal logic. Part of the nodes of the peer-to-peer network compete to append transactions to the blockchain. To do so, they group the transactions sent by users into blocks, and update their view of the blockchain state by executing these transactions in the chosen order. Once a block of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we develop a theory of transaction parallelism for blockchains, which is based on static analysis of transactions and smart contracts. We illustrate how blockchain nodes can use our theory to parallelize the execution of transactions. Initial experiments on Ethereum show that our technique can improve the performance of nodes.

Andrea Canidio, Gabriele Costa, Letterio Galletta

We propose PrYVeCT, a private-yet-verifiable contact tracing system. PrYVeCT works also as an authorization framework allowing for the definition of fine-grained policies, which a certain facility can define and apply to better model its own access rules. Users are authorized to access the facility only when they exhibit a contact trace that complies with the policy. The policy evaluation process is carried out without disclosing the personal data of the user. At the same time, each user can prove to a third party (e.g., a public authority) that she received a certain authorization. PrYVeCT takes advantage of oblivious automata evaluation to implement a privacy-preserving policy enforcement mechanism.

Matteo Busi, Pierpaolo Degano, Letterio Galletta

Obfuscating compilers protect a software by obscuring its meaning and impeding the reconstruction of its original source code. The typical concern when defining such compilers is their robustness against reverse engineering and the performance of the produced code. Little work has been done in studying whether the security properties of a program are preserved under obfuscation. In this paper we start addressing this problem: we consider control-flow flattening, a popular obfuscation technique used in industrial compilers, and a specific security policy, namely constant-time. We prove that this obfuscation preserves the policy, i.e., that every program satisfying the policy still does after the transformation.

Matteo Busi, Pierpaolo Degano, Letterio Galletta

Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is available to check if a compilation chain meets such requirements. Here, we outline our ongoing research inspired by translation validation, to effectively check one of those principles.

Chiara Bodei, Pierpaolo Degano, Gian-Luigi Ferrari et al.

The Internet of Things (IoT) is smartifying our everyday life. Our starting point is IoT-LySa, a calculus for describing IoT systems, and its static analysis, which will be presented at Coordination 2016. We extend the mentioned proposal in order to begin an investigation about security issues, in particular for the static verification of secrecy and some other security properties.