arXiv subjects

Roberto Zunino

Publications and source records attributed to Roberto Zunino.

At least 19 recordsLinked to original sources

arXiv2026

A formal framework for the economic security of DeFi compositions

Decentralized Finance (DeFi) services are usually constructed by composing a variety of smart contracts. While composability is a key driver of the success of DeFi, it also creates security risks: adversaries may exploit interactions between newly deployed contracts and the pre-existing ones to inflict economic losses. We introduce MEV non-interference, a formal security notion for DeFi composability requiring that the maximal extractable value from a set of newly deployed contracts is not increased by interactions with the existing blockchain state. To support this notion, we define local MEV, a novel measure of economic attacks that focusses on the loss of a given set of victim contracts. We study two adversarial models, with bounded and unbounded wealth, and establish sufficient conditions and locality principles that enable modular reasoning about secure composability. We apply the framework to representative DeFi compositions, including exchanges, AMMs, options, lending pools, routers, and arbitrage contracts, showing how it distinguishes secure compositions from vulnerable ones. Our results provide a formal foundation for reasoning about the economic security of DeFi compositions.

cs.CR↗

arXiv2025

Certifying optimal MEV strategies with Lean

Maximal Extractable Value (MEV) refers to a class of attacks to decentralized applications where the adversary profits by manipulating the ordering, inclusion, or exclusion of transactions in a blockchain. Decentralized Finance (DeFi) protocols are a primary target of these attacks, as their logic depends critically on transaction sequencing. To date, MEV attacks have already extracted billions of dollars in value, underscoring their systemic impact on blockchain security. Verifying the absence of MEV attacks requires determining suitable upper bounds, i.e. proving that no adversarial strategy can extract more value (if any) than expected by protocol designers. This problem is notoriously difficult: the space of adversarial strategies is extremely vast, making empirical studies and pen-and-paper reasoning insufficiently rigorous. In this paper, we present the first mechanized formalization of MEV in the Lean theorem prover. We introduce a methodology to construct machine-checked proofs of MEV bounds, providing correctness guarantees beyond what is possible with existing techniques. To demonstrate the generality of our approach, we model and analyse the MEV of two paradigmatic DeFi protocols. Notably, we develop the first machine-checked proof of the optimality of sandwich attacks in Automated Market Makers, a fundamental DeFi primitive.

cs.CR↗

arXiv2025

How To Save Fees in Bitcoin Smart Contracts: a Simple Optimistic Off-chain Protocol

We consider the execution of smart contracts on Bitcoin. There, every contract step corresponds to appending to the blockchain a new transaction that spends the output representing the old contract state, creating a new one for the updated state. This standard procedure requires the contract participants to pay transaction fees for every execution step. In this paper, we introduce a protocol that moves most of the execution of a Bitcoin contract off-chain. When all participants follow this protocol, they are able to save on transaction fees, drastically reducing them. By contrast, whenever adversaries try to disrupt the off-chain execution, any honest participant is still able to enforce the correct contract behaviour, by continuing its execution on-chain.

cs.CR↗

arXiv2025

A theoretical basis for MEV

Maximal Extractable Value (MEV) refers to a wide class of economic attacks to public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from smart contracts. Empirical research has shown that mainstream DeFi protocols are massively targeted by these attacks, with detrimental effects on their users and on the blockchain network. Despite the increasing real-world impact of these attacks, their theoretical foundations remain insufficiently established. We propose a formal theory of MEV, based on a general, abstract model of blockchains and smart contracts. Our theory is the basis for proofs of security against MEV attacks.

cs.CR↗

arXiv2025

Scalable UTXO Smart Contracts via Fine-Grained Distributed State

UTXO-based smart contract platforms face an efficiency bottleneck, in that any transaction sent to a contract must specify the entire updated contract state. This requirement becomes particularly burdensome when the contract state contains dynamic data structures, as needed in many use cases to track interactions between users and the contract. The problem is twofold: on the one hand, a large state in transactions implies a large transaction fee; on the other hand, a large centralized state is detrimental to the parallelization of transactions - a feature that is often cited as a key advantage of UTXO-based blockchains over account-based ones. We propose a technique to efficiently execute smart contracts on an extended UTXO blockchain, which allows the contract state to be distributed across multiple UTXOs. In this way, transactions only need to specify the part of the state they need to access, reducing their size (and fees). We show how to exploit our model to parallelize the validation of transactions on multi-core CPUs. We implement our technique and provide an empirical validation of its effectiveness.

cs.CR↗

arXiv2024

Smart Contract Languages: a comparative analysis

Smart contracts have played a pivotal role in the evolution of blockchains and Decentralized Applications (DApps). As DApps continue to gain widespread adoption, multiple smart contract languages have been and are being made available to developers, each with its distinctive features, strengths, and weaknesses. In this paper, we examine the smart contract languages used in major blockchain platforms, with the goal of providing a comprehensive assessment of their main properties. Our analysis targets the programming languages rather than the underlying architecture: as a result, while we do consider the interplay between language design and blockchain model, our main focus remains on language-specific features such as usability, programming style, safety and security. To conduct our assessment, we propose an original benchmark which encompasses a wide, yet manageable, spectrum of key use cases that cut across all the smart contract languages under examination.

cs.CR↗

arXiv2024

Secure compilation of rich smart contracts on poor UTXO blockchains

Most blockchain platforms from Ethereum onwards render smart contracts as stateful reactive objects that update their state and transfer crypto-assets in response to transactions. A drawback of this design is that when users submit a transaction, they cannot predict in which state it will be executed. This exposes them to transaction-ordering attacks, a widespread class of attacks where adversaries with the power to construct blocks of transactions can extract value from smart contracts (the so-called MEV attacks). The UTXO model is an alternative blockchain design that thwarts these attacks by requiring new transactions to spend past ones: since transactions have unique identifiers, reordering attacks are ineffective. Currently, the blockchains following the UTXO model either provide contracts with limited expressiveness (Bitcoin), or require complex run-time environments (Cardano). We present ILLUM , an Intermediate-Level Language for the UTXO Model. ILLUM can express real-world smart contracts, e.g. those found in Decentralized Finance. We define a compiler from ILLUM to a bare-bone UTXO blockchain with loop-free scripts. Our compilation target only requires minimal extensions to Bitcoin Script: in particular, we exploit covenants, a mechanism for preserving scripts along chains of transactions. We prove the security of our compiler: namely, any attack targeting the compiled contract is also observable at the ILLUM level. Hence, the compiler does not introduce new vulnerabilities that were not already present in the source ILLUM contract. We evaluate the practicality of ILLUM as a compilation target for higher-level languages. To this purpose, we implement a compiler from a contract language inspired by Solidity to ILLUM, and we apply it to a benchmark or real-world smart contracts.

cs.CR↗

arXiv2024

DeFi composability as MEV non-interference

Complex DeFi services are usually constructed by composing a variety of simpler smart contracts. The permissionless nature of the blockchains where these smart contracts are executed makes DeFi services exposed to security risks, since adversaries can target any of the underlying contracts to economically damage the compound service. We introduce a new notion of secure composability of smart contracts, which ensures that adversaries cannot economically harm the compound contract by interfering with its dependencies.

cs.CR↗

arXiv2023

Sound approximate and asymptotic probabilistic bisimulations for PCTL

We tackle the problem of establishing the soundness of approximate bisimilarity with respect to PCTL and its relaxed semantics. To this purpose, we consider a notion of bisimilarity inspired by the one introduced by Desharnais, Laviolette, and Tracol, and parametric with respect to an approximation error $δ$, and to the depth $n$ of the observation along traces. Essentially, our soundness theorem establishes that, when a state $q$ satisfies a given formula up-to error $δ$ and steps $n$, and $q$ is bisimilar to $q'$ up-to error $δ'$ and enough steps, we prove that $q'$ also satisfies the formula up-to a suitable error $δ"$ and steps $n$. The new error $δ"$ is computed from $δ$, $δ'$ and the formula, and only depends linearly on $n$. We provide a detailed overview of our soundness proof. We extend our bisimilarity notion to families of states, thus obtaining an asymptotic equivalence on such families. We then consider an asymptotic satisfaction relation for PCTL formulae, and prove that asymptotically equivalent families of states asymptotically satisfy the same formulae.

cs.LO↗

arXiv2022

Verifying liquidity of recursive Bitcoin contracts

Smart contracts - computer protocols that regulate the exchange of crypto-assets in trustless environments - have become popular with the spread of blockchain technologies. A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some assets remain frozen, i.e. not redeemable by anyone. The relevance of this issue is witnessed by recent liquidity attacks to Ethereum, which have frozen hundreds of USD millions. We address the problem of verifying liquidity on BitML, a DSL for smart contracts with a secure compiler to Bitcoin, featuring primitives for currency transfers, contract renegotiation and consensual recursion. Our main result is a verification technique for liquidity. We first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of a chosen set of contracts, abstracting from the moves of the context. With respect to the chosen contracts, this abstraction is sound, i.e. if the abstracted contract is liquid, then also the concrete one is such. We then verify liquidity by model-checking the finite-state abstraction. We implement a toolchain that automatically verifies liquidity of BitML contracts and compiles them to Bitcoin, and we assess it through a benchmark of representative contracts.

cs.CR↗

arXiv2021

Computationally sound Bitcoin tokens

We propose a secure and efficient implementation of fungible tokens on Bitcoin. Our technique is based on a small extension of the Bitcoin script language, which allows the spending conditions in a transaction to depend on the neighbour transactions. We show that our implementation is computationally sound: that is, adversaries can make tokens diverge from their ideal functionality only with negligible probability.

cs.CR↗

arXiv2021

A formal model of Algorand smart contracts

We develop a formal model of Algorand stateless smart contracts (stateless ASC1.) We exploit our model to prove fundamental properties of the Algorand blockchain, and to establish the security of some archetypal smart contracts. While doing this, we highlight various design patterns supported by Algorand. We perform experiments to validate the coherence of our formal model w.r.t. the actual implementation.

cs.CR↗

arXiv2020

Bitcoin covenants unchained

Covenants are linguistic primitives that extend the Bitcoin script language, allowing transactions to constrain the scripts of the redeeming ones. Advocated as a way of improving the expressiveness of Bitcoin contracts while preserving the simplicity of the UTXO design, various forms of covenants have been proposed over the years. A common drawback of the existing descriptions is the lack of formalization, making it difficult to reason about properties and supported use cases. In this paper we propose a formal model of covenants, which can be implemented with minor modifications to Bitcoin. We use our model to specify some complex Bitcoin contracts, and we discuss how to exploit covenants to design high-level language primitives for Bitcoin contracts.

cs.PL↗

arXiv2020

Renegotiation and recursion in Bitcoin contracts

BitML is a process calculus to express smart contracts that can be run on Bitcoin. One of its current limitations is that, once a contract has been stipulated, the participants cannot renegotiate its terms: this prevents expressing common financial contracts, where funds have to be added by participants at run-time. In this paper, we extend BitML with a new primitive for contract renegotiation. At the same time, the new primitive can be used to write recursive contracts, which was not possible in the original BitML. We show that, despite the increased expressiveness, it is still possible to execute BitML on standard Bitcoin, preserving the security guarantees of BitML.

cs.CR↗

arXiv2019

Developing secure Bitcoin contracts with BitML

We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.

cs.PL↗

arXiv2018

Efficient Finite Difference Method for Computing Sensitivities of Biochemical Reactions

Sensitivity analysis of biochemical reactions aims at quantifying the dependence of the reaction dynamics on the reaction rates. The computation of the parameter sensitivities, however, poses many computational challenges when taking stochastic noise into account. This paper proposes a new finite difference method for efficiently computing sensitivities of biochemical reactions. We employ propensity bounds of reactions to couple the simulation of the nominal and perturbed processes. The exactness of the simulation is reserved by applying the rejection-based mechanism. For each simulation step, the nominal and perturbed processes under our coupling strategy are synchronized and often jump together, increasing their positive correlation and hence reducing the variance of the estimator. The distinctive feature of our approach in comparison with existing coupling approaches is that it only needs to maintain a single data structure storing propensity bounds of reactions during the simulation of the nominal and perturbed processes. Our approach allows to computing sensitivities of many reaction rates simultaneously. Moreover, the data structure does not require to be updated frequently, hence improving the computational cost. This feature is especially useful when applied to large reaction networks. We benchmark our method on biological reaction models to prove its applicability and efficiency.

q-bio.MN↗

arXiv2016

Honesty by Typing

We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises made, or not. Type safety guarantees that a typeable process is honest - that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidable, and it allows to safely approximate the honesty of processes using either synchronous or asynchronous communication.

cs.PL↗

arXiv2013

Contract agreements via logic

We relate two contract models: one based on event structures and game theory, and the other one based on logic. In particular, we show that the notions of agreement and winning strategies in the game-theoretic model are related to that of provability in the logical model.

cs.LO↗