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 novel UTXO-based blockchain model, named hybrid UTXO (hUTXO) , along with a technique to efficiently execute smart contracts on it. The key idea underlying hUTXO is the distribution of the contract state across multiple UTXOs, enabling transactions to access only the specific portions of the state they need, thereby reducing their size (and fees). Our hUTXO model also borrows features from account-based models (in particular, the handling of the contract balance), making it “hybrid” in nature. To simplify the development of smart contracts in hUTXO, we introduce a high-level smart contract language (named hURF), along with a compiler into hUTXO transactions. We show how to exploit our framework to parallelize the validation of transactions on multi-core CPUs. We implement our technique and provide an empirical validation of its effectiveness.

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. • We give an abstract overview of smart contract platforms, discussing the impact of different design choices. • We illustrate by examples how different design choices give rise to different programming styles for smart contracts. • We consider 6 leading smart contract languages: Solidity (Ethereum), Rust (Solana), Aiken (Cardano), PyTeal (Algorand), Move (Aptos), SmartPy (Tezos). • We develop an open-source benchmark of use cases of smart contracts, implemented in all the languages in our selection. • Based on our benchmark, we evaluate smart contract languages focussing on their security, code readability, usability, and functionalities.

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 Illumlevel. Hence, the compiler does not introduce new vulnerabilities that were not already present in the source Illumcontract. 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.

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 $\delta$, 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 $\delta$ and steps $n$, and $q$ is bisimilar to $q'$ up-to error $\delta'$ and enough steps, we prove that $q'$ also satisfies the formula up-to a suitable error $\delta"$ and steps $n$. The new error $\delta"$ is computed from $\delta$, $\delta'$ 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.

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.

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.

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.

We introduce BitML, a domain-specific language for specifying contracts that regulate transfers of bitcoins among participants, without relying on trusted intermediaries. We define a symbolic and a computational model for reasoning about BitML security. In the symbolic model, participants act according to the semantics of BitML, while in the computational model they exchange bitstrings, and read/append transactions on the Bitcoin blockchain. A compiler is provided to translate contracts into standard Bitcoin transactions. Participants can execute a contract by appending these transactions on the Bitcoin blockchain, according to their strategies. We prove the correctness of our compiler, showing that computational attacks on compiled contracts are also observable in the symbolic model.

Exact stochastic simulation is an indispensable tool for a quantitative study of biochemical reaction networks. The simulation realizes the time evolution of the model by randomly choosing a reaction to fire and update the system state according to a probability that is proportional to the reaction propensity. Two computationally expensive tasks in simulating large biochemical networks are the selection of next reaction firings and the update of reaction propensities due to state changes. We present in this work a new exact algorithm to optimize both of these simulation bottlenecks. Our algorithm employs the composition-rejection on the propensity bounds of reactions to select the next reaction firing. The selection of next reaction firings is independent of the number reactions while the update of propensities is skipped and performed only when necessary. It therefore provides a favorable scaling for the computational complexity in simulating large reaction networks. We benchmark our new algorithm with the state of the art algorithms available in literature to demonstrate its applicability and efficiency.

We study usage automata, a formal model for specifying policies on the usage of resources. Usage automata extend finite state automata with some additional features, parameters and guards, that improve their expressivity. We show that usage automata are expressive enough to model policies of real-world applications. We discuss their expressive power, and we prove that the problem of telling whether a computation complies with a usage policy is decidable. The main contribution of this paper is a model checking technique for usage automata. The model is that of usages, i.e. basic processes that describe the possible patterns of resource access and creation. In spite of the model having infinite states, because of recursion and resource creation, we devise a polynomial-time model checking technique for deciding when a usage complies with a usage policy.

We propose a model of events with circular causality, in the form of a conservative extension of Winskel's event structures. We study the relations between this new kind of event structures and Propositional Contract Logic. Provable atoms in the logic correspond to reachable events in our event structures. Furthermore, we show a correspondence between the configurations of this new brand of event structures and the proofs in a fragment of Propositional Contract Logic.

We propose a formal theory of contract-based computing. We model contracts as formulae in an intuitionistic logic extended with a "contractual'' form of implication. Decidability holds for our logic: this allows us to mechanically infer the rights and the duties deriving from any set of contracts. We embed our logic in a core calculus of contracting processes, which combines features from concurrent constraints and calculi for multiparty sessions, while subsuming several idioms for concurrency.

We consider the problem of statically deciding when a service always provides its functionality within a given amount of time. In a timed π-calculus, we propose a two-phases static analysis guaranteeing that processes enjoy both the maximal progress and the well-timedness properties. Exploiting this analysis, we devise a decision procedure for checking service deadlines.

An extension of the λ-calculus is proposed, to study resource usage analysis and verification. It features usage policies with a possibly nested, local scope, and dynamic creation of resources. We define a type and effect system that, given a program, extracts a history expression, that is, a sound overapproximation to the set of histories obtainable at runtime. After a suitable transformation, history expressions are model-checked for validity. A program is resource-safe if its history expression is verified valid: If such, no runtime monitor is needed to safely drive its executions.

We outline a methodology for designing and composing services in a secure manner. In particular, we are concerned with safety properties of service behaviour. Services can enforce security policies locally and can invoke other services respecting given security contracts. This call-by-contract mechanism offers a significant set of opportunities, each driving secure ways to compose services. We discuss how to correctly plan services compositions in several relevant classes of services and security properties. To this aim, we propose a graphical modelling framework, based on a foundational calculus called lambda-req. Our formalism features dynamic and static semantics, so allowing for formal reasoning about systems. Static analysis and model checking techniques provide the designer with useful information to assess and fix possible vulnerabilities.