Showing 1–43 of 43 results for author: Bartoletti, M

Scalable UTXO Smart Contracts via Fine-Grained Distributed State

Authors: Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino

Abstract: Current UTXO-based smart contracts face an efficiency bottleneck, requiring any transaction sent to a contract to specify the entire updated contract state. This requirement becomes particularly burdensome when the contract state contains dynamic data structures, such as maps, which are needed in many use cases for tracking users interactions with the contract. The problem is twofold: on the one h… ▽ More Current UTXO-based smart contracts face an efficiency bottleneck, requiring any transaction sent to a contract to specify the entire updated contract state. This requirement becomes particularly burdensome when the contract state contains dynamic data structures, such as maps, which are needed in many use cases for tracking users interactions with 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, which should be one of the main selling points of UTXO-based blockchains compared to 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 also 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. △ Less

Submitted 11 June, 2024; originally announced June 2024.

Solvent: liquidity verification of smart contracts

Authors: Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, Vadim Malvone

Abstract: Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to with… ▽ More Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts. △ Less

Submitted 20 June, 2024; v1 submitted 27 April, 2024; originally announced April 2024.

Smart Contract Languages: a comparative analysis

Authors: Massimo Bartoletti, Lorenzo Benetollo, Michele Bugliesi, Silvia Crafa, Giacomo Dal Sasso, Roberto Pettinau, Andrea Pinna, Mattia Piras, Sabina Rossi, Stefano Salis, Alvise Spanò, Viacheslav Tkachenko, Roberto Tonelli, Roberto Zunino

Abstract: Decentralized blockchain platforms support the secure exchange of assets among users without relying on trusted third parties. These exchanges are programmed with smart contracts, computer programs directly executed by blockchain nodes. Multiple smart contract languages are available nowadays to developers, each with its own distinctive features, strengths, and weaknesses. In this paper, we examin… ▽ More Decentralized blockchain platforms support the secure exchange of assets among users without relying on trusted third parties. These exchanges are programmed with smart contracts, computer programs directly executed by blockchain nodes. Multiple smart contract languages are available nowadays to developers, each with its own distinctive features, strengths, and weaknesses. In this paper, we examine the smart contract languages used in six major blockchain platforms: Ethereum, Solana, Cardano, Algorand, Aptos, and Tezos. Starting with a high-level overview of their design choices, we provide a comprehensive assessment that focuses on programming style, security, code readability, and usability, drawing on an original benchmark that encompasses a common set of use cases across all the smart contract languages under examination. △ Less

Submitted 5 April, 2024; originally announced April 2024.

Towards benchmarking of Solidity verification tools

Authors: Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, Franco Sainas

Abstract: Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockc… ▽ More Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockchains. Although bug detection tools for Solidity have been proliferating almost since the inception of Ethereum, only in the last few years we have seen verification tools capable of proving that a contract respects some desirable properties. An open issue is how to evaluate and compare the effectiveness of these tools: indeed, the existing benchmarks for general-purpose programming languages cannot be adapted to Solidity, given substantial differences in the programming model and in the desirable properties. We address this problem by proposing an open benchmark for Solidity verification tools. By exploiting our benchmark, we compare two leading tools, SolCMC and Certora, discussing their completeness, soundness and expressiveness limitations. △ Less

Submitted 16 February, 2024; originally announced February 2024.

Formalizing Automated Market Makers in the Lean 4 Theorem Prover

Authors: Daniele Pusceddu, Massimo Bartoletti

Abstract: Automated Market Makers (AMMs) are an integral component of the decentralized finance (DeFi) ecosystem, as they allow users to exchange crypto-assets without the need for trusted authorities or external price oracles. Although these protocols are based on relatively simple mechanisms, e.g., to algorithmically determine the exchange rate between crypto-assets, they give rise to complex economic beh… ▽ More Automated Market Makers (AMMs) are an integral component of the decentralized finance (DeFi) ecosystem, as they allow users to exchange crypto-assets without the need for trusted authorities or external price oracles. Although these protocols are based on relatively simple mechanisms, e.g., to algorithmically determine the exchange rate between crypto-assets, they give rise to complex economic behaviours. This complexity is witnessed by the proliferation of models that study their structural and economic properties. Currently, most of theoretical results obtained on these models are supported by pen-and-paper proofs. This work proposes a formalization of constant-product AMMs in the Lean 4 Theorem Prover. To demonstrate the utility of our model, we provide mechanized proofs of key economic properties like arbitrage, that at the best of our knowledge have only been proved by pen-and-paper before. △ Less

Submitted 8 February, 2024; originally announced February 2024.

DeFi composability as MEV non-interference

Authors: Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino

Abstract: 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 contr… ▽ More 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. △ Less

Submitted 8 January, 2024; v1 submitted 19 September, 2023; originally announced September 2023.

Secure compilation of rich smart contracts on poor UTXO blockchains

Authors: Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino

Abstract: 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 adversarie… ▽ More 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. △ Less

Submitted 22 April, 2024; v1 submitted 16 May, 2023; originally announced May 2023.

A theoretical basis for Blockchain Extractable Value

Authors: Massimo Bartoletti, Roberto Zunino

Abstract: Extractable Value 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 protocols, like e.g. decentralized exchanges, are massively targeted by these attacks, with detrimental effects on their users and on the blockch… ▽ More Extractable Value 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 protocols, like e.g. decentralized exchanges, are massively targeted by these attacks, with detrimental effects on their users and on the blockchain network. Despite the growing impact of these attacks in the real world, theoretical foundations are still missing. We propose a formal theory of Extractable Value, based on a general, abstract model of blockchains and smart contracts. Our theory is the basis for proofs of security against Extractable Value attacks. △ Less

Submitted 16 May, 2023; v1 submitted 4 February, 2023; originally announced February 2023.

Formal Analysis of Lending Pools in Decentralized Finance

Authors: Massimo Bartoletti, James Chiang, Tommi Junttila, Alberto Lluch Lafuente, Massimiliano Mirelli, Andrea Vandin

Abstract: Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi application… ▽ More Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi applications is essential to assess their safety. We have developed a tool for the formal analysis of one of the most widespread DeFi applications: Lending Pools (LP). This was achieved by leveraging an existing formal model for LPs, the Maude verification environment and the MultiVeStA statistical analyser. The tool supports several analyses including reachability analysis, LTL model checking and statistical model checking. In this paper we show how the tool can be used to analyse several parameters of LPs that are fundamental to assess and predict their behaviour. In particular, we use statistical analysis to search for threshold and reward parameters that minimize the risk of unrecoverable loans. △ Less

Submitted 16 September, 2022; v1 submitted 1 June, 2022; originally announced June 2022.

MSC Class: 68N30 ACM Class: I.6.4

Sound approximate and asymptotic probabilistic bisimulations for PCTL

Authors: Massimo Bartoletti, Maurizio Murgia, Roberto Zunino

Abstract: 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… ▽ More 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. △ Less

Submitted 30 March, 2023; v1 submitted 4 November, 2021; originally announced November 2021.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 1 (March 31, 2023) lmcs:10158

Maximizing Extractable Value from Automated Market Makers

Authors: Massimo Bartoletti, James Hsin-yu Chiang, Alberto Lluch-Lafuente

Abstract: Automated Market Makers (AMMs) are decentralized applications that allow users to exchange crypto-tokens without the need for a matching exchange order. AMMs are one of the most successful DeFi use cases: indeed, major AMM platforms process a daily volume of transactions worth USD billions. Despite their popularity, AMMs are well-known to suffer from transaction-ordering issues: adversaries can in… ▽ More Automated Market Makers (AMMs) are decentralized applications that allow users to exchange crypto-tokens without the need for a matching exchange order. AMMs are one of the most successful DeFi use cases: indeed, major AMM platforms process a daily volume of transactions worth USD billions. Despite their popularity, AMMs are well-known to suffer from transaction-ordering issues: adversaries can influence the ordering of user transactions, and possibly front-run them with their own, to extract value from AMMs, to the detriment of users. We devise an effective procedure to construct a strategy through which an adversary can maximize the value extracted from user transactions. △ Less

Submitted 19 July, 2022; v1 submitted 2 June, 2021; originally announced June 2021.

Comments: FC'22 proceedings version with proofs in appendix

MSC Class: 68N30 ACM Class: I.6.4

A theory of Automated Market Makers in DeFi

Authors: Massimo Bartoletti, James Hsin-yu Chiang, Alberto Lluch-Lafuente

Abstract: Automated market makers (AMMs) are one of the most prominent decentralized finance (DeFi) applications. AMMs allow users to trade different types of crypto-tokens, without the need to find a counter-party. There are several implementations and models for AMMs, featuring a variety of sophisticated economic mechanisms. We present a theory of AMMs. The core of our theory is an abstract operational mo… ▽ More Automated market makers (AMMs) are one of the most prominent decentralized finance (DeFi) applications. AMMs allow users to trade different types of crypto-tokens, without the need to find a counter-party. There are several implementations and models for AMMs, featuring a variety of sophisticated economic mechanisms. We present a theory of AMMs. The core of our theory is an abstract operational model of the interactions between users and AMMs, which can be concretised by instantiating the economic mechanisms. We exploit our theory to formally prove a set of fundamental properties of AMMs, characterizing both structural and economic aspects. We do this by abstracting from the actual economic mechanisms used in implementations, and identifying sufficient conditions which ensure the relevant properties. Notably, we devise a general solution to the arbitrage problem, the main game-theoretic foundation behind the economic mechanisms of AMMs. △ Less

Submitted 16 December, 2022; v1 submitted 22 February, 2021; originally announced February 2021.

MSC Class: 68N30 ACM Class: I.6.4

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 4 (December 19, 2022) lmcs:8955

SoK: Lending Pools in Decentralized Finance

Authors: Massimo Bartoletti, James Hsin-yu Chiang, Alberto Lluch-Lafuente

Abstract: Lending pools are decentralized applications which allow mutually untrusted users to lend and borrow crypto-assets. These applications feature complex, highly parametric incentive mechanisms to equilibrate the loan market. This complexity makes the behaviour of lending pools difficult to understand and to predict: indeed, ineffective incentives and attacks could potentially lead to emergent unwant… ▽ More Lending pools are decentralized applications which allow mutually untrusted users to lend and borrow crypto-assets. These applications feature complex, highly parametric incentive mechanisms to equilibrate the loan market. This complexity makes the behaviour of lending pools difficult to understand and to predict: indeed, ineffective incentives and attacks could potentially lead to emergent unwanted behaviours. Reasoning about lending pools is made even harder by the lack of executable models of their behaviour: to precisely understand how users interact with lending pools, eventually one has to inspect their implementations, where the incentive mechanisms are intertwined with low-level implementation details. Further, the variety of existing implementations makes it difficult to distill the common aspects of lending pools. We systematize the existing knowledge about lending pools, leveraging a new formal model of interactions with users, which reflects the archetypal features of mainstream implementations. This enables us to prove some general properties of lending pools, such as the correct handling of funds, and to precisely describe vulnerabilities and attacks. We also discuss the role of lending pools in the broader context of decentralized finance. △ Less

Submitted 24 December, 2020; originally announced December 2020.

Comments: 20 pages. Under submission

MSC Class: 68N30 ACM Class: I.6.4

Verifying liquidity of recursive Bitcoin contracts

Authors: Massimo Bartoletti, Stefano Lande, Maurizio Murgia, Roberto Zunino

Abstract: 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 a… ▽ More 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. △ Less

Submitted 31 January, 2022; v1 submitted 28 November, 2020; originally announced November 2020.

Comments: arXiv admin note: text overlap with arXiv:2003.00296

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (February 1, 2022) lmcs:6943

A theory of transaction parallelism in blockchains

Authors: Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Abstract: 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 cr… ▽ More 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. △ Less

Submitted 17 November, 2021; v1 submitted 27 November, 2020; originally announced November 2020.

Comments: arXiv admin note: text overlap with arXiv:1905.04366

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (November 18, 2021) lmcs:6935

Computationally sound Bitcoin tokens

Authors: Massimo Bartoletti, Stefano Lande, Roberto Zunino

Abstract: 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 negli… ▽ More 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. △ Less

Submitted 9 February, 2021; v1 submitted 3 October, 2020; originally announced October 2020.

A formal model of Algorand smart contracts

Authors: Massimo Bartoletti, Andrea Bracciali, Cristian Lepore, Alceste Scalas, Roberto Zunino

Abstract: 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 implem… ▽ More 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. △ Less

Submitted 26 January, 2021; v1 submitted 25 September, 2020; originally announced September 2020.

Bitcoin covenants unchained

Authors: Massimo Bartoletti, Stefano Lande, Roberto Zunino

Abstract: 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 forma… ▽ More 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. △ Less

Submitted 26 July, 2020; v1 submitted 6 June, 2020; originally announced June 2020.

Renegotiation and recursion in Bitcoin contracts

Authors: Massimo Bartoletti, Maurizio Murgia, Roberto Zunino

Abstract: 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… ▽ More 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. △ Less

Submitted 21 April, 2020; v1 submitted 29 February, 2020; originally announced March 2020.

Comments: Full version of the paper presented at COORDINATION 2020

Proceedings 12th Interaction and Concurrency Experience

Authors: Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou, Alceste Scalas

Abstract: This volume contains the proceedings of ICE'19, the 12th Interaction and Concurrency Experience, which was held in Copenhagen, Denmark on the 20th and 21st of June 2019, as a satellite event of DisCoTec'19. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past 11 editions, this interaction consider… ▽ More This volume contains the proceedings of ICE'19, the 12th Interaction and Concurrency Experience, which was held in Copenhagen, Denmark on the 20th and 21st of June 2019, as a satellite event of DisCoTec'19. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past 11 editions, this interaction considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The 2019 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three PC members, and altogether 9 papers were accepted for publication - plus 2 oral presentations which are not part of this volume. We were proud to host 4 invited talks, by Dilian Gurov, Fritz Henglein, Sophia Knight, and Hernán Melgratti. The abstracts of these talks are included in this volume together with the regular papers. Final versions of the contributions, taking into account the discussion at the workshop, are included. △ Less

Submitted 11 September, 2019; originally announced September 2019.

Journal ref: EPTCS 304, 2019

A minimal core calculus for Solidity contracts

Authors: Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Abstract: The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of E… ▽ More The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we propose a minimal calculus for Solidity contracts, which extends an imperative core with a single primitive to transfer currency and invoke contract procedures. We build upon this formalisation to give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some typical quirks of Solidity, like e.g. re-entrancy. △ Less

Submitted 6 August, 2019; originally announced August 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:1905.04366

Develo** secure Bitcoin contracts with BitML

Authors: Nicola Atzei, Massimo Bartoletti, Stefano Lande, Nobuko Yoshida, Roberto Zunino

Abstract: We present a toolchain for develo** 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 foreve… ▽ More We present a toolchain for develo** 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. △ Less

Submitted 2 August, 2019; v1 submitted 18 May, 2019; originally announced May 2019.

A true concurrent model of smart contracts executions

Authors: Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Abstract: The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (represent… ▽ More The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (representing the required actions on contracts), and execute them in some order. Once this sequence 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 propose a true concurrent model of smart contract execution. Based on this, we show how static analysis of smart contracts can be exploited to parallelize the execution of transactions. △ Less

Submitted 27 April, 2020; v1 submitted 10 May, 2019; originally announced May 2019.

Comments: Full version of the paper presented at COORDINATION 2020

Blockchain for social good: a quantitative analysis

Authors: Massimo Bartoletti, Tiziana Cimoli, Livio Pompianu, Sergio Serusi

Abstract: The rise of blockchain technologies has given a boost to social good projects, which are trying to exploit various characteristic features of blockchains: the quick and inexpensive transfer of cryptocurrency, the transparency of transactions, the ability to tokenize any kind of assets, and the increase in trustworthiness due to decentralization. However, the swift pace of innovation in blockchain… ▽ More The rise of blockchain technologies has given a boost to social good projects, which are trying to exploit various characteristic features of blockchains: the quick and inexpensive transfer of cryptocurrency, the transparency of transactions, the ability to tokenize any kind of assets, and the increase in trustworthiness due to decentralization. However, the swift pace of innovation in blockchain technologies, and the hype that has surrounded their "disruptive potential", make it difficult to understand whether these technologies are applied correctly, and what one should expect when trying to apply them to social good projects. This paper addresses these issues, by systematically analysing a collection of 120 blockchain-enabled social good projects. Focussing on measurable and objective aspects, we try to answer various relevant questions: which features of blockchains are most commonly used? Do projects have success in fund raising? Are they making appropriate choices on the blockchain architecture? How many projects are released to the public, and how many are eventually abandoned? △ Less

Submitted 2 November, 2018; originally announced November 2018.

Comments: In GOODTECHS 2018

Proceedings 11th Interaction and Concurrency Experience

Authors: Massimo Bartoletti, Sophia Knight

Abstract: This volume contains the proceedings of ICE'18, the 11th Interaction and Concurrency Experience, which was held in Madrid, Spain on the 20th and 21st of June 2018 as a satellite event of DisCoTec'18. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past ten editions, this interaction considerabl… ▽ More This volume contains the proceedings of ICE'18, the 11th Interaction and Concurrency Experience, which was held in Madrid, Spain on the 20th and 21st of June 2018 as a satellite event of DisCoTec'18. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past ten editions, this interaction considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. For the second time, the 2018 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three PC members, and altogether six papers were accepted for publication (the workshop also featured four oral presentations which are not part of this volume). We were proud to host three invited talks, by Elvira Albert, Silvia Crafa, and Alexey Gotsman. The abstracts of these talks are included in this volume together with the regular papers. Final versions of the contributions, taking into account the discussion at the workshop, are included. △ Less

Submitted 4 October, 2018; originally announced October 2018.

Journal ref: EPTCS 279, 2018

Data mining for detecting Bitcoin Ponzi schemes

Authors: Massimo Bartoletti, Barbara Pes, Sergio Serusi

Abstract: Soon after its introduction in 2009, Bitcoin has been adopted by cyber-criminals, which rely on its pseudonymity to implement virtually untraceable scams. One of the typical scams that operate on Bitcoin are the so-called Ponzi schemes. These are fraudulent investments which repay users with the funds invested by new users that join the scheme, and implode when it is no longer possible to find new… ▽ More Soon after its introduction in 2009, Bitcoin has been adopted by cyber-criminals, which rely on its pseudonymity to implement virtually untraceable scams. One of the typical scams that operate on Bitcoin are the so-called Ponzi schemes. These are fraudulent investments which repay users with the funds invested by new users that join the scheme, and implode when it is no longer possible to find new investments. Despite being illegal in many countries, Ponzi schemes are now proliferating on Bitcoin, and they keep alluring new victims, who are plundered of millions of dollars. We apply data mining techniques to detect Bitcoin addresses related to Ponzi schemes. Our starting point is a dataset of features of real-world Ponzi schemes, that we construct by analysing, on the Bitcoin blockchain, the transactions used to perform the scams. We use this dataset to experiment with various machine learning algorithms, and we assess their effectiveness through standard validation protocols and performance metrics. The best of the classifiers we have experimented can identify most of the Ponzi schemes in the dataset, with a low number of false positives. △ Less

Submitted 1 March, 2018; originally announced March 2018.

Proceedings 10th Interaction and Concurrency Experience

Authors: Massimo Bartoletti, Laura Bocchi, Ludovic Henrio, Sophia Knight

Abstract: This volume contains the proceedings of ICE 2017, the 10th Interaction and Concurrency Experience, which was held in Neuchâtel, Switzerland on the 21st and 22nd of June 2017 as a satellite event of DisCoTec'17. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose acce… ▽ More This volume contains the proceedings of ICE 2017, the 10th Interaction and Concurrency Experience, which was held in Neuchâtel, Switzerland on the 21st and 22nd of June 2017 as a satellite event of DisCoTec'17. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. For the first time, the 2017 edition of ICE included a double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. The gender balance of accepted papers was also more even than in past years. Each paper was reviewed by three PC members, and altogether five papers were accepted for publication (the workshop also featured five brief announcements which are not part of this volume). We were proud to host three invited talks, by Christian Cachin, Marieke Huismann, and Paweł Sobocinski. The abstracts of these talks are included in this volume together with the regular papers. △ Less

Submitted 29 November, 2017; originally announced November 2017.

Journal ref: EPTCS 261, 2017

Timed Session Types

Authors: Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia

Abstract: Timed session types formalise timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the progress-based compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one. Then, we show how to construct the most… ▽ More Timed session types formalise timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the progress-based compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one. Then, we show how to construct the most precise session type compliant with a given one, according to the subty** preorder induced by compliance. Decidability of subty** follows from these results. △ Less

Submitted 7 December, 2017; v1 submitted 15 October, 2017; originally announced October 2017.

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 4 (December 8, 2017) lmcs:4130

A general framework for blockchain analytics

Authors: Massimo Bartoletti, Andrea Bracciali, Stefano Lande, Livio Pompianu

Abstract: Modern cryptocurrencies exploit decentralised blockchains to record a public and unalterable history of transactions. Besides transactions, further information is stored for different, and often undisclosed, purposes, making the blockchains a rich and increasingly growing source of valuable information, in part of difficult interpretation. Many data analytics have been developed, mostly based on s… ▽ More Modern cryptocurrencies exploit decentralised blockchains to record a public and unalterable history of transactions. Besides transactions, further information is stored for different, and often undisclosed, purposes, making the blockchains a rich and increasingly growing source of valuable information, in part of difficult interpretation. Many data analytics have been developed, mostly based on specifically designed and ad-hoc engineered approaches. We propose a general-purpose framework, seamlessly supporting data analytics on both Bitcoin and Ethereum - currently the two most prominent cryptocurrencies. Such a framework allows us to integrate relevant blockchain data with data from other sources, and to organise them in a database, either SQL or NoSQL. Our framework is released as an open-source Scala library. We illustrate the distinguishing features of our approach on a set of significant use cases, which allow us to empirically compare ours to other competing proposals, and evaluate the impact of the database choice on scalability. △ Less

Submitted 6 November, 2017; v1 submitted 4 July, 2017; originally announced July 2017.

Comments: Authors' version of a paper presented at SERIAL'17

An empirical analysis of smart contracts: platforms, applications, and design patterns

Authors: Massimo Bartoletti, Livio Pompianu

Abstract: Smart contracts are computer programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resilience to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect certain agreed rules (like in financial services and in games). Over the last few… ▽ More Smart contracts are computer programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resilience to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect certain agreed rules (like in financial services and in games). Over the last few years many platforms for smart contracts have been proposed, and some of them have been actually implemented and used. We study how the notion of smart contract is interpreted in some of these platforms. Focussing on the two most widespread ones, Bitcoin and Ethereum, we quantify the usage of smart contracts in relation to their application domain. We also analyse the most common programming patterns in Ethereum, where the source code of smart contracts is available. △ Less

Submitted 18 March, 2017; originally announced March 2017.

Comments: WTSC 2017

Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact

Authors: Massimo Bartoletti, Salvatore Carta, Tiziana Cimoli, Roberto Saia

Abstract: Ponzi schemes are financial frauds which lure users under the promise of high profits. Actually, users are repaid only with the investments of new users joining the scheme: consequently, a Ponzi scheme implodes soon after users stop joining it. Originated in the offline world 150 years ago, Ponzi schemes have since then migrated to the digital world, approaching first the Web, and more recently ha… ▽ More Ponzi schemes are financial frauds which lure users under the promise of high profits. Actually, users are repaid only with the investments of new users joining the scheme: consequently, a Ponzi scheme implodes soon after users stop joining it. Originated in the offline world 150 years ago, Ponzi schemes have since then migrated to the digital world, approaching first the Web, and more recently hanging over cryptocurrencies like Bitcoin. Smart contract platforms like Ethereum have provided a new opportunity for scammers, who have now the possibility of creating "trustworthy" frauds that still make users lose money, but at least are guaranteed to execute "correctly". We present a comprehensive survey of Ponzi schemes on Ethereum, analysing their behaviour and their impact from various viewpoints. △ Less

Submitted 12 August, 2019; v1 submitted 10 March, 2017; originally announced March 2017.

An analysis of Bitcoin OP_RETURN metadata

Authors: Massimo Bartoletti, Livio Pompianu

Abstract: The Bitcoin protocol allows to save arbitrary data on the blockchain through a special instruction of the scripting language, called OP_RETURN. A growing number of protocols exploit this feature to extend the range of applications of the Bitcoin blockchain beyond transfer of currency. A point of debate in the Bitcoin community is whether loading data through OP_RETURN can negatively affect the per… ▽ More The Bitcoin protocol allows to save arbitrary data on the blockchain through a special instruction of the scripting language, called OP_RETURN. A growing number of protocols exploit this feature to extend the range of applications of the Bitcoin blockchain beyond transfer of currency. A point of debate in the Bitcoin community is whether loading data through OP_RETURN can negatively affect the performance of the Bitcoin network with respect to its primary goal. This paper is an empirical study of the usage of OP_RETURN over the years. We identify several protocols based on OP_RETURN, which we classify by their application domain. We measure the evolution in time of the usage of each protocol, the distribution of OP_RETURN transactions by application domain, and their space consumption. △ Less

Submitted 1 March, 2017; v1 submitted 3 February, 2017; originally announced February 2017.

Comments: BITCOIN 2017

Proceedings 9th Interaction and Concurrency Experience

Authors: Massimo Bartoletti, Ludovic Henrio, Sophia Knight, Hugo Torres Vieira

Abstract: This volume contains the proceedings of ICE 2016, the 9th Interaction and Concurrency Experience, which was held in Heraklion, Greece on the 8th and 9th of June 2016 as a satellite event of DisCoTec 2016. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is re… ▽ More This volume contains the proceedings of ICE 2016, the 9th Interaction and Concurrency Experience, which was held in Heraklion, Greece on the 8th and 9th of June 2016 as a satellite event of DisCoTec 2016. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. For the first time, the 2016 edition of ICE included a feature targeting review transparency: reviews of accepted papers were made public on the workshop website and workshop participants in particular were able to access them during the workshop. Each paper was reviewed by three PC members, and altogether nine papers were accepted for publication (the workshop also featured three brief announcements which are not part of this volume). We were proud to host two invited talks, by Alexandra Silva and Uwe Nestmann. The abstracts of these two talks are included in this volume together with the regular papers. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Journal ref: EPTCS 223, 2016

Combining behavioural types with security analysis

Authors: Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira

Abstract: Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforc… ▽ More Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties. △ Less

Submitted 8 October, 2015; originally announced October 2015.

Journal ref: Journal of Logical and Algebraic Methods in Programming, Elsevier, 2015, pp.18

The LTS WorkBench

Authors: Alceste Scalas, Massimo Bartoletti

Abstract: Labelled Transition Systems (LTSs) are a fundamental semantic model in many areas of informatics, especially concurrency theory. Yet, reasoning on LTSs and relations between their states can be difficult and elusive: very simple process algebra terms can give rise to a large (possibly infinite) number of intricate transitions and interactions. To ease this kind of study, we present LTSwb, a flex… ▽ More Labelled Transition Systems (LTSs) are a fundamental semantic model in many areas of informatics, especially concurrency theory. Yet, reasoning on LTSs and relations between their states can be difficult and elusive: very simple process algebra terms can give rise to a large (possibly infinite) number of intricate transitions and interactions. To ease this kind of study, we present LTSwb, a flexible and extensible LTS toolbox: this tutorial paper discusses its design and functionalities. △ Less

Submitted 19 August, 2015; originally announced August 2015.

Comments: In Proceedings ICE 2015, arXiv:1508.04595

ACM Class: D.2.2; D.3.1; F.3.2

Journal ref: EPTCS 189, 2015, pp. 86-98

A note on two notions of compliance

Authors: Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna

Abstract: We establish a relation between two models of contracts: binary session types, and a model based on event structures and game-theoretic notions. In particular, we show that compliance in session types corresponds to the existence of certain winning strategies in game-based contracts. We establish a relation between two models of contracts: binary session types, and a model based on event structures and game-theoretic notions. In particular, we show that compliance in session types corresponds to the existence of certain winning strategies in game-based contracts. △ Less

Submitted 27 October, 2014; originally announced October 2014.

Comments: In Proceedings ICE 2014, arXiv:1410.7013

Journal ref: EPTCS 166, 2014, pp. 86-93

Contract agreements via logic

Authors: Massimo Bartoletti, Tiziana Cimoli, Paolo Di Giamberardino, Roberto Zunino

Abstract: 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. 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. △ Less

Submitted 17 October, 2013; v1 submitted 31 May, 2013; originally announced June 2013.

Comments: In Proceedings ICE 2013, arXiv:1310.4019

Journal ref: EPTCS 131, 2013, pp. 5-19

An event-based model for contracts

Authors: Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna, Roberto Zunino

Abstract: We introduce a basic model for contracts. Our model extends event structures with a new relation, which faithfully captures the circular dependencies among contract clauses. We establish whether an agreement exists which respects all the contracts at hand (i.e. all the dependencies can be resolved), and we detect the obligations of each participant. The main technical contribution is a corresp… ▽ More We introduce a basic model for contracts. Our model extends event structures with a new relation, which faithfully captures the circular dependencies among contract clauses. We establish whether an agreement exists which respects all the contracts at hand (i.e. all the dependencies can be resolved), and we detect the obligations of each participant. The main technical contribution is a correspondence between our model and a fragment of the contract logic PCL. More precisely, we show that the reachable events are exactly those which correspond to provable atoms in the logic. Despite of this strong correspondence, our model improves previous work on PCL by exhibiting a finer-grained notion of culpability, which takes into account the legitimate orderings of events. △ Less

Submitted 26 February, 2013; originally announced February 2013.

Comments: In Proceedings PLACES 2012, arXiv:1302.5798

Journal ref: EPTCS 109, 2013, pp. 13-20

Lending Petri nets and contracts

Authors: Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna

Abstract: Choreography-based approaches to service composition typically assume that, after a set of services has been found which correctly play the roles prescribed by the choreography, each service respects his role. Honest services are not protected against adversaries. We propose a model for contracts based on a extension of Petri nets, which allows services to protect themselves while still realizing… ▽ More Choreography-based approaches to service composition typically assume that, after a set of services has been found which correctly play the roles prescribed by the choreography, each service respects his role. Honest services are not protected against adversaries. We propose a model for contracts based on a extension of Petri nets, which allows services to protect themselves while still realizing the choreography. We relate this model with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification. △ Less

Submitted 30 May, 2013; v1 submitted 15 November, 2012; originally announced November 2012.

Honesty by Ty**

Authors: Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino

Abstract: We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by kee** 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 decidabl… ▽ More We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by kee** 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. △ Less

Submitted 27 December, 2016; v1 submitted 12 November, 2012; originally announced November 2012.

ACM Class: D.2.4; D.3.1; D.3.2; F.3.1; F.3.2

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2619

On the realizability of contracts in dishonest systems

Authors: Massimo Bartoletti, Emilio Tuosto, Roberto Zunino

Abstract: We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types. We consider the contracts of \cite{CastagnaPadovaniGesbert09toplas}, and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the… ▽ More We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types. We consider the contracts of \cite{CastagnaPadovaniGesbert09toplas}, and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts. △ Less

Submitted 30 January, 2012; originally announced January 2012.

Contracts in distributed systems

Authors: Massimo Bartoletti, Emilio Tuosto, Roberto Zunino

Abstract: We present a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among principals happens… ▽ More We present a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among principals happens via multi-party sessions, which are created once agreements are reached. We present two instances of our calculus, by modelling contracts as (i) processes in a variant of CCS, and (ii) as formulae in a logic. With the help of a few examples, we discuss the primitives of our calculus, as well as some possible variants. △ Less

Submitted 1 August, 2011; originally announced August 2011.

Comments: In Proceedings ICE 2011, arXiv:1108.0144

Journal ref: EPTCS 59, 2011, pp. 130-147

Primitives for Contract-based Synchronization

Authors: Massimo Bartoletti, Roberto Zunino

Abstract: We investigate how contracts can be used to regulate the interaction between processes. To do that, we study a variant of the concurrent constraints calculus presented in [1], featuring primitives for multi-party synchronization via contracts. We proceed in two directions. First, we exploit our primitives to model some contract-based interactions. Then, we discuss how several models for concurrenc… ▽ More We investigate how contracts can be used to regulate the interaction between processes. To do that, we study a variant of the concurrent constraints calculus presented in [1], featuring primitives for multi-party synchronization via contracts. We proceed in two directions. First, we exploit our primitives to model some contract-based interactions. Then, we discuss how several models for concurrency can be expressed through our primitives. In particular, we encode the pi-calculus and graph rewriting. △ Less

Submitted 27 October, 2010; originally announced October 2010.

Comments: In Proceedings ICE 2010, arXiv:1010.5308

Journal ref: EPTCS 38, 2010, pp. 67-82