Advertisement

Verifying Liquidity of Bitcoin Contracts

  • Massimo BartolettiEmail author
  • Roberto Zunino
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11426)

Abstract

A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some funds remain frozen. The relevance of this issue is witnessed by a recent liquidity attack to the Ethereum Parity Wallet, which has frozen \({\sim }160M\) USD within the contract, making this sum unredeemable by any user. We address the problem of verifying liquidity of Bitcoin contracts. Focussing on BitML, a contracts DSL with a computationally sound compiler to Bitcoin, we study various notions of liquidity. Our main result is that liquidity of BitML contracts is decidable, in all the proposed variants. To prove this, we first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of any given set of contracts, abstracting the context moves. With respect to the chosen contracts, this abstraction is sound and complete. Our decision procedure for liquidity is then based on model-checking the finite space of states of the abstraction.

Keywords

Bitcoin Smart contracts Verification 

1 Introduction

Decentralized ledgers like Bitcoin and Ethereum [19, 32] enable the trustworthy execution of smart contracts—computer protocols which regulate the exchange of assets among mutually untrusted users. The underlying protocols used to update the ledger (which defines the state of each contract) ensure that, even without trusted intermediaries, the execution of contracts is correct with respect to the contract rules. However, it may happen that the rules themselves are not correct with respect to the behaviour expected by the users. Indeed, all the attacks to smart contracts successfully carried out so far, which have plundered or frozen millions of USD in Ethereum [1, 2, 3, 8, 27, 30], exploit some discrepancy between the intended and the actual behaviour of a contract.

To counteract these attacks, the research community has recently started to formalize smart contracts and their security properties [22, 23, 24], and to develop automated verification tools based on these models [21, 27, 31, 35]. As a matter of fact, most of this research is targeted to Ethereum, the most widespread (and attacked) platform for smart contracts: for this reason, the security properties addressed by current tools focus on specific features of Solidity, the high-level language for smart contracts in Ethereum. For instance, some vulnerability patterns checked by these tools are reentrancy and mishandled exceptions, whose peculiar implementation in Solidity has led to attacks, like to one to the DAO [1]. Only a few tools verify general security properties of smart contracts, that would be meaningful also outside the realm of Ethereum. Among these works, [35] checks a property called liquidity, which holds when the contract always admits a trace where its balance is decreased (so, the funds stored within the contract do not remain frozen). This has been inspired from a recent attack to Ethereum [2], which has frozen \(\sim \)160M USD within a contract, exploiting a bug in a library. While being capable of classifying this particular contract as non-liquid, any contract where the adversary can lock some funds and redeem them at a later moment would be classified as liquid. Stronger notions of liquidity may rule out these unsafe contracts, e.g. by checking that funds are never frozen for all possible strategies of the adversary. Studying liquidity in a more general setting would be important for various reasons. First, taking into account adversaries would allow to detect more security issues w.r.t. those checked by the current verification tools. Second, platform-agnostic notions of liquidity could be applied to the forthcoming blockchain technologies, e.g. [20, 34]. Third, studying liquidity in simpler settings than Ethereum could simplify the verification problem, which is undecidable in Turing-powerful languages like those supported by Ethereum.

Contributions. We study several notions of liquidity for smart contracts, in a general setting where their behaviour is defined as a transition system. We then consider the special case where contracts are expressed in BitML, a high-level DSL for smart contracts which compiles into Bitcoin [14]. In such setting, we develop a verification technique for liquidity of smart contracts. We can summarise our main contributions as follows:
  1. 1.

    We formalize a notion of liquidity (Definition 2), and we illustrate several meaningful variants. Our notion of liquidity takes into account both the contract and the strategy that a participant follows to perform contract actions. Roughly, a strategy is liquid when following it ensures that funds do not remain frozen within the contract, even in the presence of adversaries.

     
  2. 2.

    We introduce an abstraction of the semantics of BitML which is finite-state (Theorem 1), and sound and complete w.r.t. the concrete (infinite-state) semantics, given a set of contracts under observation (Theorems 2 and 3).

     
  3. 3.

    We devise a verification technique for liquidity in BitML. Our technique can establish whether a strategy is liquid for a given contract, and also to synthesise a liquid strategy, when it exists (Theorem 4).

     

Our finite-state abstraction is general-purpose: verifying liquidity is only one of its possible applications (some other applications are discussed in Sect. 6).

Related Works. Several recent works study security issues related to Ethereum smart contracts. A few papers address EVM, the bytecode language which is the target of compilation of Solidity. Among them, [27] introduces an operational semantics of a simplified version of EVM, and develops Oyente, a tool to detect some vulnerability patterns of EVM contracts through symbolic execution. Securify [35] checks vulnerability patterns by analysing dependency graphs extracted from EVM code. As mentioned before, this tool also addresses a form of liquidity, which essentially assumes a cooperating adversary. EtherTrust [21] is a framework for the static verification of EVM contracts, which can establish e.g. the absence of reentrancy vulnerabilities. This tool is based on the detailed formalisation of EVM provided in [22], which is validated against the official Ethereum test suite. The work [23] introduces an executable semantics of EVM, specified in the \(\mathbb {K}\) framework. The tool in [18] translates Solidity and EVM code into \(\mathsf {F}^*\), and use its verification tools to detect vulnerabilities of contracts; further, the tool verifies the equivalence between a Solidity program and an alleged compilation of it into EVM. The work [24] verifies EVM code through the Isabelle/HOL proof assistant [33], proving that, upon an invocation of a specific contract, only its owner can decrease the balance.

Smart contracts in Bitcoin have a completely different flavour compared to Ethereum, since they are usually expressed as cryptographic protocols, rather than as programs. Despite the limited expressiveness of the scripts in Bitcoin transactions [10], several kinds of contracts for Bitcoin have been proposed [9]: they range from lotteries [6, 7, 13, 29], to general multiparty computations [4, 17, 26], to contingent payments [11, 28], etc. All these works focus on proving the security of a fixed contract, unlike the above-mentioned works on Ethereum, where the goal is to verify arbitrary contracts. As far as we know, only a couple of works pursue this goal for Bitcoin. The tool in [25] analyses Bitcoin scripts, in order to find under which conditions the enclosing transaction can be redeemed. Compared to [25], our work verifies contracts spanning among many transactions, rather than single scripts. The work [5] models contracts as timed automata, and then uses the Uppaal model checker [16] to verify their properties. The contracts modelled as in [5] cannot be directly translated to Bitcoin, while in our approach we can exploit the BitML compiler to translate contracts to standard Bitcoin transactions. Note also that the properties considered in [5] are specific to the modelled contract, while in this work we are interested in verifying general properties of contracts, like liquidity.

2 Overview

In this section we briefly overview BitML; we then give some intuition about liquidity and our verification technique. Because of space limits, we refer to [14] for a detailed treatment of BitML, and to [12] for a more gentle introduction.

We assume a set of participants, ranged over by Open image in new window , and a set of names, of two kinds: Open image in new window denote deposits of Open image in new window , while \(\mathord {{a}_{}}, \mathord {{b}_{}}, \ldots \) denote secrets. We write Open image in new window (resp. \(\varvec{\mathord {{a}_{}}}\)) for a finite sequence of deposit (resp. secrets) names.

2.1 BitML in a Nutshell

BitML is a domain-specific language for Bitcoin smart contracts, which allows participants to exchange cryptocurrency according to pre-agreed contract rules. In BitML, any participant can broadcast a contract advertisement Open image in new window , where Open image in new window is the actual contract, specifying the rules to transfer bitcoins ( Open image in new window ), while Open image in new window is a set of preconditions to its execution.

Preconditions (Fig. 1, left) may require participants to deposit some Open image in new window in the contract (either upfront or at runtime), or to commit to some secret. More in detail, Open image in new window requires Open image in new window to own Open image in new window in a deposit Open image in new window , and to spend it for stipulating a contract Open image in new window . Instead, Open image in new window only requires Open image in new window to pre-authorize the spending of Open image in new window , which can be gathered by the contract at run-time. The precondition Open image in new window requires Open image in new window to commit to a secret \(\mathord {{a}_{}}\) before Open image in new window starts.

After Open image in new window has been advertised, each participant can choose whether to accept it, or not. When all the preconditions Open image in new window have been satisfied, and all the involved participants have accepted, the contract Open image in new window becomes stipulated. The contract starts its execution with a balance, initially set to the sum of the !-deposits required by its preconditions. Running Open image in new window will affect this balance, when participants deposit/withdraw funds to/from the contract.
Fig. 1.

Syntax of BitML contracts and preconditions.

Fig. 2.

Syntax of predicates.

A contract Open image in new window is a choice among zero or more branches. Each branch is a guarded contract (Fig. 1, right) which enables an action, and possibly proceeds with a continuation  Open image in new window . The guarded contract Open image in new window transfers the whole balance to Open image in new window , while Open image in new window decomposes the contract into n parallel components Open image in new window , each one with balance \(v_{i}\). The guarded contract Open image in new window atomically performs the following: (i) spend all the ?-deposits Open image in new window , adding their values to the contract balance; (ii) check that all the secrets \(\varvec{\mathord {{a}_{}}}\) have been revealed and satisfy the predicate \(\mathord {p_{}}\) (Fig. 2). When enabled, the above-mentioned actions can be fired by anyone, at anytime. To restrict who can execute actions and when, one can use the decoration Open image in new window , which requires the authorization of Open image in new window , and the decoration Open image in new window , which requires to wait until time \(t_{}\).

A Basic Example. As a first example, we express in BitML the timed commitment [6], a basic protocol to construct more complex contracts, like e.g. lotteries and other games [7]. In the timed commitment, a participant Open image in new window wants to choose a secret, and promises to reveal it before some time \(t_{}\). The contract ensures that if Open image in new window does not reveal the secret in time, then she will pay a penalty of Open image in new window to Open image in new window (e.g., the opponent player in a game). In BitML, this is modelled as follows:The precondition requires Open image in new window to pay upfront Open image in new window , and to commit to a secret \(\mathord {{a}_{}}\). The contract (hereafter, named Open image in new window ) is a non-deterministic choice between two branches. Only Open image in new window can choose the first branch, by performing Open image in new window (syntactic sugar for Open image in new window ). Subsequently, anyone can transfer Open image in new window to Open image in new window . Only after \(t_{}\), if the \(\texttt {reveal} \) has not been fired, any participant can fire Open image in new window in the second branch, moving Open image in new window to Open image in new window . So, before \(t_{}\), Open image in new window has the option to reveal \(\mathord {{a}_{}}\) (avoiding the penalty), or to keep it secret (paying the penalty). If no branch is taken by \(t_{}\), the first one who fires its Open image in new window gets Open image in new window .

2.2 BitML Semantics

We briefly recall from [14] the semantics of BitML. The semantics is a labelled transition system between configurations of the following form:

We now illustrate the BitML semantics by examples; when time is immaterial, we only show the steps of the untimed semantics. We omit labels on transitions.

Deposits. When Open image in new window owns a deposit Open image in new window , she can use it in various ways: she can divide the deposit into two smaller deposits, or join it with another deposit of hers to form a larger one; the deposit can also be transferred to another participant, or destroyed. For instance, to donate a deposit Open image in new window to Open image in new window , Open image in new window must first issue the authorization Open image in new window ; then, anyone can transfer the money to Open image in new window :We assume that whenever a participant authorizes an operation on some deposit Open image in new window , then she is also authorising a self-donation Open image in new window of such deposit.1

Advertisement. Any participant can advertise a new contract Open image in new window (with preconditions Open image in new window ). This is obtained by performing the step Open image in new window .

Stipulation. Stipulation turns a contract advertisement into an active contract. For instance, let Open image in new window . Given a contract Open image in new window , the stipulation of Open image in new window is done in a few steps:Above, the funds in the deposit Open image in new window are transferred to the newly created contract, to fulfill the precondition Open image in new window . Instead, the deposit \(y_{}\) remains in the configuration, to be possibly spent after some time. The component Open image in new window represents the secret committed to by Open image in new window , with its length N.
Withdraw. Executing Open image in new window terminates the contract, and transfers its whole balance to  Open image in new window by creating a fresh deposit owned by Open image in new window :Above, Open image in new window is executed as a branch within a choice: as usual, taking a branch discards the other ones (denoted as Open image in new window ).
Split. The \(\texttt {split} \) primitive can be used to spawn several new concurrent contracts, dividing the balance among them. For instance:Put & Reveal. A prefix Open image in new window can be fired when the previously committed secret Open image in new window (satisfying the predicate Open image in new window ) has been revealed, and the deposit Open image in new window is available in the configuration. For instance:In the first step, Open image in new window reveals her secret Open image in new window . In the second step, any participant fires the prefix; doing so rakes the deposit Open image in new window within the contract.
Authorizations. When a branch is decorated by Open image in new window it can be taken only after Open image in new window has provided her authorization. For instance:In the first step, Open image in new window authorizes to take the branch Open image in new window . After that, any participant can fire such branch.
Time. We always allow time \(t_{}\) to advance by a delay \(\delta >0\), through a transition \( {\varGamma _{}} \mid {t_{}} \xrightarrow {} {\varGamma _{}} \mid {t_{}+\delta } \). Advancing time can enable branches decorated with \(\texttt {after}\, t_{}\). For instance, if \(t_{0}+\delta \ge t_{}\), we have the following computation:Runs and Strategies. A run \(\mathcal {R}_{}\) is a (possibly infinite) sequence:where \(\ell _{i}\) are the transition labels, \(\varGamma _{0}\) contains only deposits, and \(t_{0}=0\). If \(\mathcal {R}_{}\) is finite, we write \(\varGamma _{\mathcal {R}_{}}\) for its last untimed configuration, and \(\delta _{\mathcal {R}_{}}\) for its last time. A strategy Open image in new window is a PPTIME algorithm which allows Open image in new window to select which actions to perform (possibly, time delays), among those permitted by the BitML semantics. The choice among these actions is controlled by the adversary strategy Open image in new window , which acts on behalf of all the dishonest participants. Given the strategies of all participants (including Open image in new window ), there is a unique run conforming to all of them.

2.3 Liquidity

A desirable property of smart contracts is liquidity, which requires that the contract balance is always eventually transferred to some participant. In a non-liquid contract, funds can be frozen forever, unavailable to anyone, hence effectively destroyed. There are many possible flavours of liquidity, depending e.g. on which participants are assumed to be honest, and on which are their strategies. The simplest form of liquidity is to consider the case where everyone cooperates: i.e. a contract is liquid if there exists some strategy for each participant such that no funds are ever frozen. However, this notion does not capture the essence of smart contracts, i.e. to allow mutually untrusted participants to safely interact.

For instance, consider the following contract, where Open image in new window and Open image in new window contribute Open image in new window each for a donation of Open image in new window to either Open image in new window or Open image in new window (we omit the preconditions for brevity):In order to unlock the funds, Open image in new window and Open image in new window must agree on the recipient of the donation, by giving their authorization on the same branch. This contract would be liquid only by assuming the cooperation between Open image in new window and Open image in new window : indeed, Open image in new window alone cannot guarantee that the Open image in new window will eventually be donated, as Open image in new window can choose a different recipient, or even refuse to give any authorization. Consequently, unless Open image in new window trusts Open image in new window , it makes sense to consider this contract as non-liquid, from the point of view of Open image in new window (and for similar reasons, also from that of Open image in new window ).
Consider now the timed commitment contract discussed before:This contract is liquid from Open image in new window ’s point of view (even if Open image in new window is dishonest), because Open image in new window can reveal the secret and then redeem the funds from the contract. The timed commitment is also liquid from Open image in new window ’s point of view: if Open image in new window does not reveal the secret (making the first branch stuck), the funds in the contract can be redeemed through the second branch, after time \(t_{}\).
In a mutual timed commitment contract, where Open image in new window and Open image in new window have to exchange their secrets or pay a Open image in new window penalty, achieving liquidity is a bit more challenging. We first consider a wrong attempt:Intuitively, Open image in new window has only the following strategies, according to when she decides to reveal her secret \(\mathord {{a}_{}}\): (i) Open image in new window chooses to reveal \(\mathord {{a}_{}}\) unconditionally, and to perform the Open image in new window action. This strategy is not liquid: indeed, if Open image in new window does not reveal \(\mathord {{b}_{}}\), the contract is stuck. (ii) Open image in new window chooses to reveal \(\mathord {{a}_{}}\) only after Open image in new window has revealed \(\mathord {{b}_{}}\). This strategy is not liquid: indeed, if Open image in new window chooses not to reveal \(\mathord {{b}_{}}\), the contract will never advance. (iii) Open image in new window chooses to wait until Open image in new window reveals secret \(\mathord {{b}_{}}\), or until time \(t'_{}\ge t_{}\), whichever comes first. If \(\mathord {{b}_{}}\) was revealed, Open image in new window reveals \(\mathord {{a}_{}}\), and splits the contract balance between Open image in new window and Open image in new window . Otherwise, if the deadline \(t'_{}\) is expired, Open image in new window transfers the whole balance to Open image in new window . Note that, although this strategy is liquid, it is not satisfactory for Open image in new window , since in the second case she will lose money.
This example highlights a crucial point: participants’ strategies have to be taken into account when defining liquidity. Indeed, the mere fact that a liquid strategy exists does not imply that it is the ideal strategy for the honest participant. To fix this issue, we revise the mutual timed commitment as follows:where \(t_{}< t'_{}\). Now, Open image in new window has a liquid strategy where she does not pay the penalty. First, Open image in new window reveals \(\mathord {{a}_{}}\) before time \(t_{}\). After that, if Open image in new window reveals \(\mathord {{b}_{}}\), then Open image in new window can execute the \(\texttt {split} \), transferring Open image in new window to herself and Open image in new window to Open image in new window (note that this does not require Open image in new window ’s cooperation); otherwise, after time \(t'_{}\), Open image in new window can withdraw Open image in new window by executing the Open image in new window in the Open image in new window branch.

These examples, albeit elementary, show that detecting if a strategy is liquid for a contract is not straightforward, in general. The problem of determining a liquid strategy for a given contract seems even more demanding. Automatic techniques for the verification and inference of liquid strategies can be useful tools for the developers of smart contracts.

2.4 Verifying Liquidity

One of the main contributions of this paper is a verification technique for the liquidity of BitML contracts. Our technique is based on a more general result, i.e. a strict correspondence between the semantics of BitML in [14] (hereafter, called concrete semantics) and a new abstract semantics, which is finite-state (Theorem 1). Our abstraction is a correct and complete approximation of the concrete semantics with respect to a given set of contracts (Theorems 2 and 3). To obtain a finite-state abstraction, we need to cope with three sources of infiniteness of the concrete semantics of BitML: the unbounded passing of time, the advertisement/stipulation of new contracts, and the operations on deposits. Our abstraction replaces the time \(t_{}\) in concrete configurations with a finite number of time intervals \(T_{}= [t_{0},t_{1})\), and it disables the transitions to advertise new contracts. Further, the only operations on deposits allowed by the abstract semantics are the ones for transferring them to contracts and for destroying them. The latter is needed e.g. to properly model the situation where a participant spends a ?-deposit.

The intended use of our abstraction is to start from a configuration containing an arbitrary (but finite) set of contracts, and then analyse their possible evolutions in the presence of an honest participant and an adversary. This produces a finite set of (finite) traces, which we can model-check for liquidity. Soundness and completeness of the abstraction are exploited to prove that liquidity is decidable (Theorem 4). The computational soundness of the BitML compiler [14] guarantees that if a contract is verified to be liquid according to our analysis, this property is preserved when executing it on Bitcoin.

3 Liquidity

In this section we formalise a notion of liquidity of contracts, and we suggest some possible variants. Aiming at generality, liquidity is parameterised over (i) a set Open image in new window of contract names, uniquely identifying the contracts under observation; (ii) a participant Open image in new window (with her strategy Open image in new window ), which we assume to be the only honest participant in the system. Roughly, we want that the funds stored within the contracts Open image in new window are eventually transferred to some participant, in any run conforming to Open image in new window ’s strategy. The actual definition is a bit more complex, because the other participants may play against Open image in new window , e.g. avoiding to reveal their secrets, or to give their authorizations for some branch.

We start by introducing an auxiliary partial function Open image in new window that, given a contract name Open image in new window and an extension \(\mathcal {R}_{}\) of a run \(\mathcal {R}_{0}\), determines the ancestor \(y_{}\) of Open image in new window in the last configuration of \(\mathcal {R}_{0}\), if any. Intuitively, Open image in new window means that \(y_{}\) has evolved into \(\mathcal {R}_{}\), eventually leading to Open image in new window (and possibly to other contracts).

In BitML, there are only two ways to make a contract evolve into another contract. First, a Open image in new window can spawn new contracts, e.g.:Here, both \(y_{1}\) and \(y_{2}\) have Open image in new window as ancestor. Second, \( \texttt {put} \& \texttt {reveal} \) reduces as follows:In this case, the ancestor of \(y_{}\) is Open image in new window .

Definition 1

Let \(\mathcal {R}_{}\) be a run extending some run \(\mathcal {R}_{0}\), and let Open image in new window be a contract name. We define Open image in new window by induction on the length of \(\mathcal {R}_{}\) in Fig. 3, where Open image in new window denotes the set of contract names in \(\varGamma _{}\).

Fig. 3.

Origin of a contract name within a run.

Example 1

Let \(\mathcal {R}_{0}\) be a run with last configuration Open image in new window , and let \(\mathcal {R}_{}\) be the following extension of \(\mathcal {R}_{0}\), where the contracts Open image in new window and Open image in new window are immaterial, but for the fact that they enable the displayed moves:We have that Open image in new window , since the corresponding contracts have been obtained through a split of the ancestor y, which was in the last configuration of Open image in new window . Instead, Open image in new window is undefined, because its ancestor x is not in Open image in new window . Further, Open image in new window , while Open image in new window is undefined.

We now formalise liquidity. Assume that we want to observe a single contract Open image in new window , occurring in the last configuration of some run Open image in new window (note that Open image in new window has been stipulated at some point during Open image in new window ). A participant Open image in new window wants to know if the strategy Open image in new window allows her to make Open image in new window evolve so that funds are never frozen within the contract. We require that Open image in new window can do this without the help of the other participants, which therefore we model as a single adversary Open image in new window . More precisely, we say that Open image in new window is liquid for Open image in new window when, after any extension \(\mathcal {R}_{}\) of Open image in new window , Open image in new window can choose a sequence of moves so to make all the descendant contracts of Open image in new window terminate, transferring their funds to some participant (possibly not Open image in new window ). Note that such moves can not reveal secrets of other participants, or generate authorizations for them: Open image in new window must be able to unfreeze the funds on her own, using her strategy. By contrast, \(\mathcal {R}_{}\) can also involve such moves, but it must conform to Open image in new window ’s strategy. The actual definition of liquidity generalises the above to sets Open image in new window of contract names.

Definition 2

(Liquidity). Let Open image in new window be an honest participant, with strategy Open image in new window , let Open image in new window be a run, and let Open image in new window be a set of contract names in Open image in new window . We say that Open image in new window is liquid w.r.t. Open image in new window in Open image in new window if, for all finite extensions \(\mathcal {R}_{}\) of Open image in new window conforming to Open image in new window and to some Open image in new window , there exists an extension \(\mathcal {R}'_{}= \mathcal {R}_{}\xrightarrow {\ell _{1}} \cdots \xrightarrow {\ell _{n}}\) of \(\mathcal {R}_{}\) such that:

Condition (1) requires that all the moves after \(\mathcal {R}_{}\) can be taken by Open image in new window alone, conforming to her strategy. Condition (2) checks that \(\mathcal {R}'_{}\) no longer contains descendants of the contracts \(X_{0}\): since in BitML active contracts always store some funds, this is actually equivalent to checking that funds are not frozen.

We remark that, although Definition 2 is instantiated on BitML, the basic concepts it relies upon (runs, strategies, termination of contracts) are quite general. Hence, our notion of liquidity, as well as the variants proposed below, can be applied to other languages for smart contracts, using their transition semantics.

Example 2

Recall the timed commitment contract Open image in new window from Sect. 2. Assume that Open image in new window ’s strategy is to wait until time \(t_{}- 1\) (i.e., one time unit before the deadline), then reveal the secret and fire Open image in new window . Let Open image in new window be a run with final configuration Open image in new window , for some length N. We have that Open image in new window is liquid w.r.t. Open image in new window in Open image in new window , while it is not liquid w.r.t. the strategy where Open image in new window does not reveal the secret, or reveals it without firing Open image in new window . Indeed, under these strategies Open image in new window alone cannot make x terminate.

Example 3

Consider the following two contracts, which both require as precondition that Open image in new window put a deposit of Open image in new window and commits to a secret \(\mathord {{a}_{}}\), and where \(\mathord {p_{}}\) is an arbitrary predicate on \(\mathord {{a}_{}}\):Assume that Open image in new window ’s strategy is to reveal the secret, and then fire any enabled Open image in new window . Under this strategy, Open image in new window is liquid, because one of the \(\texttt {reveal} \) branches is enabled, and the corresponding Open image in new window is fired, transferring Open image in new window either to Open image in new window or to Open image in new window . Instead, no strategy of Open image in new window can make Open image in new window liquid. If Open image in new window does not reveal the secret, then the Open image in new window are frozen; otherwise, if Open image in new window reveals the secret, then only one of the two descendents of Open image in new window can fire the \(\texttt {reveal} \), and so Open image in new window remains frozen.

Example 4

(Lottery). Consider a lottery between two players. The preconditions require Open image in new window and Open image in new window to commit to one secret each (\(\mathord {{a}_{}}\) and \(\mathord {{b}_{}}\), respectively), and to put a deposit of Open image in new window each ( Open image in new window as a bet, and Open image in new window as a penalty for dishonest behaviour):The contract splits the balance in three parts, of Open image in new window each. The first part allows Open image in new window to reveal \(\mathord {{b}_{}}\) and then redeem Open image in new window ; otherwise, after the deadline Open image in new window can redeem Open image in new window ’s penalty (as in the timed commitment). Similarly, the second part allows Open image in new window to redeem Open image in new window by revealing \(\mathord {{a}_{}}\). To determine the winner we compare the secrets, in the subcontract Open image in new window : Open image in new window wins if the secrets have the same length, otherwise Open image in new window wins. This lottery is fair, since: (i) if both players are honest, then they will reveal their secrets within the deadlines (redeeming Open image in new window each), and then they will have a 1 / 2 probability of winning2; (ii) if a player is dishonest, not revealing the secret, then the other player has a positive payoff, since she can redeem Open image in new window .
Although fair, Open image in new window is non-liquid w.r.t. any strategy of Open image in new window . Indeed, if Open image in new window does not reveal his secret, then the Open image in new window stored in the Open image in new window subcontract are frozen. We can recover liquidity by replacing Open image in new window with the following:where \(t'_{}> t_{}\). In this case, even if Open image in new window does not reveal \(\mathord {{b}_{}}\), Open image in new window can use a strategy firing any enabled Open image in new window at time \(t'_{}\), to unfreeze the Open image in new window stored in Open image in new window .

We now present some variants of the notion of liquidity presented before.

Multiparty Liquidity. A straightforward generalisation of liquidity is to assume a set of honest participants (rather than just one). In this case, we can extend Definition 2 by requiring that the run \(\mathcal {R}_{}\) conforms to the strategies of all honest participants, and the moves in (1) can be taken by any honest participant.

We illustrate this notion through the following escrow contract between two participants Open image in new window and Open image in new window , where the precondition requires Open image in new window to deposit Open image in new window :After the contract has been stipulated, Open image in new window can choose to pay Open image in new window , by authorizing the first branch. Similarly, Open image in new window can allow Open image in new window to take her money back, by authorizing the second branch. If they do not agree, any of them can invoke a mediator Open image in new window to resolve the dispute, invoking a Open image in new window branch. There, the Open image in new window deposit is split in two parts: Open image in new window go to the mediator, while Open image in new window are assigned either to Open image in new window and Open image in new window , depending on Open image in new window ’s choice.

Assuming that only Open image in new window is honest, this contract does not admit any liquid strategy for Open image in new window , according to Definition 2. This is because Open image in new window can invoke the mediator, who can refuse to act, freezing the funds within the contract. Similarly, Open image in new window alone has no liquid strategy, as well as Open image in new window . Instead, Open image in new window admits a liquid multiparty strategy for any pair of honest participants. For instance, if Open image in new window and Open image in new window are honest, their strategies could be the following. Open image in new window chooses whether to authorize the first branch or not; in the first case, she fires Open image in new window ; otherwise, if Open image in new window gives his authorization within a certain deadline, then Open image in new window withdraws Open image in new window ; if not, after the deadline Open image in new window invokes Open image in new window . The strategy of Open image in new window is to authorize some participant to redeem the Open image in new window , and to fire all the Open image in new window within Open image in new window .

Strategyless Liquidity. Another variant of liquidity can be obtained by inspecting only the contract, neglecting Open image in new window ’s strategy. In this case, we consider the contract as liquid when there exists some strategy of Open image in new window which satisfies the constraints in Definition 2. For instance, the contract Open image in new window is non-liquid from Open image in new window ’s point of view, according to this notion, while it would be liquid for Open image in new window .

Quantitative Liquidity. Definition 2 requires that no funds remain frozen within the contract. However, in some cases Open image in new window could accept the fact that a portion of the funds remain frozen, especially when these funds would be ideally assigned to other participants. Following this intuition, we could define a contract \(v_{}\)-liquid w.r.t. Open image in new window if at least \(v_{}\) bitcoins are guaranteed to be redeemable. If the contract uses only !-deposits, the special case where \(v_{}\) is the sum of all these deposits corresponds to the notion in Definition 2. For instance, Open image in new window from Example 4 is non-liquid for any strategy of Open image in new window , but it is Open image in new window -liquid if Open image in new window ’s strategy is to reveal her secret, and perform all the enabled Open image in new window . Instead, Open image in new window is Open image in new window -liquid, and then also liquid, under this strategy.

A refinement of this variant could require that at least Open image in new window are transferred to Open image in new window , rather than to any participant. Under this notion, both Open image in new window and Open image in new window would be Open image in new window -liquid for Open image in new window . Further, Open image in new window would be Open image in new window -liquid in case Open image in new window wins the lottery.

Liquidity with Unknown Secrets. All the notions of liquidity proposed so far depend on the initial run Open image in new window , which contains the lengths of the committed secrets. For instance, consider the run ending with the following configuration:Since the length of \(\mathord {{b}_{}}\) is zero, the \(\texttt {reveal} \) branch cannot be taken, so Open image in new window has a liquid strategy (e.g., fire the Open image in new window ). Instead, in an alternative initial run where Open image in new window chooses a secret of length 1, Open image in new window has no liquid strategy, since Open image in new window can reveal the secret and then deny his authorization, freezing Open image in new window .

In practice, when Open image in new window performs the liquidity analysis, she does not know the secrets of other participants. To be safe, Open image in new window should use a worst-case analysis, which would regard the contract Open image in new window as non-liquid. We can obtain such worst-case analysis by verifying liquidity (in the flavour of Definition 2) for all possible choices of the lengths of Open image in new window ’s secrets. Although there is an infinite set of such lengths, each contract only checks a finite set of \(\texttt {if} \) conditions. Hence, the infinite set of lengths can be partitioned into a finite set of regions, which can be used as samples for the analysis. In this way, the basic liquidity analysis is performed a finite number of times.

Similar worst-case analyses can be obtained for all the other above-mentioned variants of liquidity. An average-case analysis can be obtained by assuming to know the probability distribution of Open image in new window ’s secrets lengths, partitioning secrets lengths like in the worst-case analysis.

Other Variants. Mixing multiparty and strategyless liquidity, we obtain the notion of liquidity used in [35], in the context of Ethereum smart contracts. This notion considers a contract liquid if there exists a collaborative strategy of all participants that never freezes funds. Other variants may take into account the time when funds become liquid, the payoff of strategies (e.g., ruling out irrational adversaries), or fairness issues. Note indeed that Definition 2 already assumes a sort of fairness, by effectively forbidding the adversary to interfere when the honest participant attempts to unfreeze some funds. Technically, this is implemented in item (1) of Definition 2, requiring that the moves \(\ell _{1} \ldots \ell _{n}\) are performed atomically. Atomicity might be realistic in some settings, but not in others. For instance, in Ethereum a sequence \(\ell _{1} \ldots \ell _{n}\) of method calls can be performed atomically: this requires to deploy a new contract with a suitable method which performs the calls \(\ell _{1} \ldots \ell _{n}\) in sequence, and then to invoke it. BitML, instead, does not allow participants to perform an atomic sequence of moves: an honest participant could start to perform the sequence, but at some point in the middle the adversary interferes. To make the contract liquid, the honest participant must still have a way to unfreeze the funds from the contract. Of course, the adversary could interfere once again, and so on. This could lead to an infinite trace where each attempt by the honest player is hindered by the adversary. However, this is not an issue in BitML, for the following reason. Since the moves \(\ell _{1} \ldots \ell _{n}\) make the contract terminate, we can safely assume that each of these moves makes the contract progress (as moves which do not affect the contract can be avoided). Since a BitML contract can not progress forever without terminating (and unfreezing its funds), the honest participant just needs to be able to make a step at a time (with possible interferences by the adversary, which may affect the choice of the next step). Defining liquidity beyond BitML and Ethereum may require to rule out unfair runs, where the adversary prevents honest participants to perform the needed sequences of moves.

4 A Finite-State Semantics of BitML

The concrete BitML semantics is infinite-state because participants can always create new contracts and deposits, and can advance the current time (a natural number). In this section we introduce an abstract semantics for BitML, which focuses on both these features so to reduce the state space to a finite one. More specifically, for a concrete configuration \({\varGamma _{}} \mid {t_{}}\):
Fig. 4.

Abstraction of configurations.

We start by defining the abstraction of configurations.

Definition 3

(Abstraction of configurations). We define the function Open image in new window on concrete configurations in Fig. 4, where \(y^{\star }\) denotes a fixed name not present in any concrete configuration. We write Open image in new window for Open image in new window , where:where we denote with Open image in new window the set of deposit names in some \(\texttt {put} \) within Open image in new window , and with Open image in new window the set of secrets names in some \(\texttt {reveal} \) within  Open image in new window .

The abstraction removes from \(\varGamma _{}\) all the deposits not in Open image in new window , all the (committed or revealed) secrets not in Open image in new window , and all the authorizations enabling branches of some contracts not in Open image in new window . All the other authorizations—but the deposit authorizations, which are handled in a special way—are removed. This is because, in the concrete semantics, deposits move into fresh ones which are no longer relevant for the contracts Open image in new window . Note that if we precisely tracked such irrelevant deposits and their authorizations, our abstract semantics would become infinite-state. To cope with this issue, the abstract semantics will render deposit moves as “destroy” moves, removing the now irrelevant deposits from the configuration. As anticipated in Sect. 2.2, an authorization of a deposit move can only be performed after a “self-donate” authorization Open image in new window , which lets Open image in new window transfer the funds in x to another of her deposits. Our abstraction maps such Open image in new window into an “abstract destroy” authorization Open image in new window . In this way, in abstract configurations, deposits can be destroyed when, in concrete configurations, they are no longer relevant.

The abstraction of time Open image in new window is parameterised over a finite set of naturals \(\mathcal {T}_{}\), which partitions \(\mathbb {N}\) into a finite set of non-overlapping intervals3. Each time \(t_{}\) is abstracted as Open image in new window , which is the unique interval containing \(t_{}\).

Definition 4

(Abstraction of time). Let \(\mathcal {T}_{}\in \wp _{ fin}(\mathbb {N})\). We define the function Open image in new window as Open image in new window where:
Abstract Semantics. We now describe the abstract semantics of BitML (the detailed formalisation is deferred to Definition 7 in Appendix A). An abstract configuration is a term of the form Open image in new window , where Open image in new window is a concrete untimed configuration, and Open image in new window . We then define the relation Open image in new window between abstract configurations by differences w.r.t. the concrete relation \(\xrightarrow {}\):
  1. 1.

    the rule to advertise contracts is removed.

     
  2. 2.

    the rules for deposits are replaced by two rules, which authorize and perform the destroy of deposits. In these rules we use the fixed name \(y^{\star }\), unlike the fresh names in the concrete semantics, so to avoid infinite branching.

     
  3. 3.

    the rule for delays is replaced by a new rule, which allows for transitions Open image in new window . The delay \(\delta \) is the least positive integer which makes Open image in new window (in the earliest moment) step to \(T'_{}\), i.e. Open image in new window .

     
  4. 4.

    the rule for making a contract Open image in new window reduce to a deposit Open image in new window is replaced so that Open image in new window reduces to \(0\) (the empty configuration).

     
  5. 5.

    the rule for making branches Open image in new window evolve is adapted to time intervals. The new rule requires that the current time interval \(T_{}\) is later than \(t_{}\).

     
Abstract Runs. Given an arbitrary abstract configuration \({\varGamma _{0}} \mid {T_{0}}\), an abstract run \(\mathcal {R}^{\sharp }_{}\) is a (possibly infinite) sequence Open image in new window . While concrete runs always start (at time 0) from configurations which contain only deposits, abstract runs can start from arbitrary configurations.

Abstract Strategies. An abstract strategy Open image in new window is a PPTIME algorithm which allows Open image in new window to select which actions to perform, among those permitted by the abstract semantics. Conformance between abstract runs and strategies is defined similarly to the concrete case [14].

Concretisation of Strategies. Each abstract strategy Open image in new window can be transformed into a concrete strategy Open image in new window as follows. The transformation is parameterised over a concrete run Open image in new window and a set of contract names Open image in new window : intuitively, Open image in new window is the concrete counterpart of the initial abstract configuration \({\varGamma _{0}} \mid {T_{0}}\), and Open image in new window is the set of contracts under observation. The strategy Open image in new window receives as input a concrete run \(\mathcal {R}_{}\), and it must output the next actions. If \(\mathcal {R}_{}\) is a prefix of Open image in new window , the next move is chosen as in Open image in new window . The case where \(\mathcal {R}_{}\) is not an extension of Open image in new window is immaterial. Assuming that \(\mathcal {R}_{}\) extends Open image in new window , we first abstract the part of \(\mathcal {R}_{}\) exceeding Open image in new window , so to obtain an abstract run \(\mathcal {R}^{\sharp }_{}\). This is done by abstracting every configuration in the run: times are abstracted with Open image in new window , while untimed configurations are abstracted with Open image in new window , where Open image in new window is the set of the descendants of Open image in new window in the configuration at hand. The moves of \(\mathcal {R}_{}\) are mapped to abstract moves in a natural way: moves not affecting the descendents of Open image in new window , nor their relevant deposits or secrets, are not represented in the abstract run. Once the abstract run \(\mathcal {R}^{\sharp }_{}\) has been constructed, we apply Open image in new window to obtain the next abstract actions. Open image in new window is defined as the concretisation of these actions. The concretisation of the adversary strategy Open image in new window can be defined in a similar way.

Theorem 1

Starting from any abstract configuration, the relation Open image in new window is finitely branching, and it admits a finite number of runs.

A direct consequence of Theorem 1 is that the abstract semantics is finite-state, and that each abstract run is finite. This makes the abstract LTS amenable to model checking.

Correspondence Between the Semantics. We now establish a correspondence between the abstract and the concrete semantics of BitML. Assume that we have a concrete run Open image in new window , representing the computation done so far. We want to observe the behaviour of a set of contracts Open image in new window in \(\varGamma _{\mathcal {R}_{0}}\) (the last untimed configuration of Open image in new window ). To this purpose, we run the abstract semantics, starting from an initial configuration \(\varGamma _{0}^{\sharp }\), whose untimed component is Open image in new window . The time component is obtained by abstracting the last time Open image in new window in the concrete run. The parameter \(\mathcal {T}_{0}\) used to abstract time is any finite superset of the deadlines occurring in contracts Open image in new window within Open image in new window . Hereafter we denote this set of deadlines as Open image in new window (see Definition 8 in Appendix A).

When the contracts in Open image in new window evolve, the run Open image in new window is extended to a run \(\mathcal {R}_{}\), which contains the descendents of Open image in new window , i.e. those contracts whose origin belongs to Open image in new window . These descendents are denoted with Open image in new window .

Definition 5

For all concrete runs Open image in new window such that \(\mathcal {R}_{}\) extends Open image in new window , and set of deposit names Open image in new window , we define the set of deposit names Open image in new window as follows:

The following theorem states that the abstract semantics is a sound approximation of the concrete one. Every abstract run (conforming to Open image in new window ’s abstract strategy Open image in new window ) has a corresponding concrete run (conforming to the concrete strategy derived from Open image in new window ). More precisely, each configuration \({\varGamma _{}^{\sharp }} \mid {T_{}}\) in the abstract run has a corresponding configuration in the concrete run, containing the concretization \(\varGamma _{}\) of \(\varGamma _{}^{\sharp }\), besides a term \(\varDelta _{}\) containing the parts unrelated to \(X_{0}\). Further, each move in the abstract run corresponds to an analogous move in the concrete run.

Theorem 2

(Soundness). Let Open image in new window be a concrete run, let Open image in new window , let Open image in new window , let Open image in new window , let Open image in new window . Let Open image in new window and Open image in new window be the abstract strategies of Open image in new window and of Open image in new window , and let Open image in new window and Open image in new window be the corresponding concrete strategies. For each abstract run Open image in new window conforming to Open image in new window and Open image in new window , there exists a concrete run:such that: (i) \(\mathcal {R}_{}\) conforms to Open image in new window and Open image in new window ; (ii) \(\varDelta _{}\) contains all the subterms of Open image in new window which are mapped to \(0\) when evaluating Open image in new window ; (iii) Open image in new window , where Open image in new window ; (iv) Open image in new window ; (v) the labels in \(\mathcal {R}_{}\) are the same as in \(\mathcal {R}^{\sharp }_{}\), except for the occurrences of \(y^{\star }\).

Note that soundness only guarantees the existence of some concrete runs, which are a strict subset of all the possible concrete runs. For instance, the concrete semantics also allows the non-observed part \(\varDelta _{}\) to progress, and it contains configurations with a time \(t_{}\ne \min T_{}\), for any \(T_{}\) in any abstract run. Still, these concrete runs have an abstract counterpart, as established by the following completeness result (Theorem 3). This is almost dual to our soundness result (Theorem 2). Completeness maps concrete configurations to abstract ones using our abstraction functions for untimed configurations and time. Moreover, this run correspondence holds when the concrete strategy of Open image in new window is derived from an abstract strategy, while no such restriction is required for the adversary strategy.

Theorem 3

(Completeness). Let Open image in new window be a concrete run, let Open image in new window , let Open image in new window , let Open image in new window , and let Open image in new window . Let Open image in new window be the abstract strategy of Open image in new window , and let Open image in new window be the corresponding concrete strategy. For each concrete run Open image in new window conforming to Open image in new window and to some Open image in new window , there exists an abstract run:such that: (i) \(\mathcal {R}^{\sharp }_{}\) conforms to Open image in new window and to some Open image in new window ; (ii) Open image in new window ; (iii) if Open image in new window and Open image in new window , then there exists \(\ell '_{}\) such that Open image in new window where Open image in new window and Open image in new window .

Example 5

Let Open image in new window , and let \(\mathcal {R}_{}\) be the following concrete run, where the prefix \(\cdots \) is immaterial (for simplicity, we also omit labels, times, and participants’ strategies):By Theorem 3, this concrete run has the following corresponding abstract run w.r.t. Open image in new window . The initial configuration \(\varGamma _{0}\) is abstracted w.r.t. \(X_{0}\) and Open image in new window . This causes deposit Open image in new window to be neglected in the abstraction.We now compare the two runs. The concrete authorization for a self-donate of \(y_{}\) is abstracted as an authorization for destroying \(y_{}\). Instead, the concrete authorization for donating \(y_{}\) to Open image in new window has no abstract counterpart. The concrete reveal of secret Open image in new window and the subsequent contract move have identical abstract moves, which reach the abstract configuration \(\varGamma _{}^{\sharp }\). Technically, \(\varGamma _{}^{\sharp }\) is the result of abstracting the concrete configuration \(\varGamma _{}\) w.r.t. Open image in new window and Open image in new window : here, we no longer abstract w.r.t. \(X_{0}\), but instead use the set of its descendents Open image in new window . By contrast, the set Open image in new window is unchanged. Note that, if we instead abstracted with respect to \(X_{0}\), we would discard the contract Open image in new window , in which case we could not perform the abstract step, because the abstract semantics does not discard Open image in new window . Similarly, if we instead used Open image in new window we would discard the secret \(\mathord {{a}_{}}\) and the deposit \(y_{}\), invalidating the abstract steps. When \(\varGamma _{}\) performs the next move (a donation) this is abstracted as a destroy move. Finally, the last concrete Open image in new window move is mapped to an abstract Open image in new window move, which does not create the deposit \(x''_{}\).

5 Verifying Liquidity

In this section we devise a verification technique for liquidity of BitML contracts, exploiting our abstract semantics. The first step is to give an abstract counterpart of liquidity: this is done in Definition 6, which mimics Definition 2, replacing concrete objects with abstract ones.

Definition 6

(Abstract liquidity). Let Open image in new window be an honest participant, with abstract strategy Open image in new window , let \(\mathcal {R}^{\sharp }_{0}\) be an abstract run, and let \(X_{0}\) be a set of contract names in \(\varGamma _{\mathcal {R}^{\sharp }_{0}}\). We say that \(X_{0}\) is \(\sharp \)-liquid w.r.t. Open image in new window in \(\mathcal {R}^{\sharp }_{0}\) if for all extensions \(\mathcal {R}^{\sharp }_{}\) of \(\mathcal {R}^{\sharp }_{0}\) conforming to Open image in new window and to some Open image in new window , there exists an extension \( \dot{\mathcal {R}^{\sharp }}_{}= \mathcal {R}^{\sharp }_{}\xrightarrow {\ell _{1}} \cdots \xrightarrow {\ell _{n}} \) of \(\mathcal {R}^{\sharp }_{}\) such that:

To verify liquidity of a set of contracts \(X_{0}\) in a concrete run Open image in new window , we will choose \(\mathcal {R}^{\sharp }_{0}\) to be the run containing a single configuration \(\varGamma _{0}^{\sharp }\), obtained by abstracting with Open image in new window the last configuration of Open image in new window . In such case, the condition (4) above can be simplified by just requiring that Open image in new window .

The following lemma states that abstract and concrete liquidity are equivalent. For this, it suffices that the abstraction is performed with respect to the contract names \(X_{0}\), and to the set of deadlines occurring in the contracts \(X_{0}\).

Lemma 2

(Abstract vs. concrete liquidity). Let Open image in new window be a concrete run, let Open image in new window , and let Open image in new window . Let Open image in new window . Let Open image in new window be an abstract strategy (w.r.t. \(\mathcal {T}_{0}\) and \(\varGamma _{0}^{\sharp }\)), and let Open image in new window . Let \(\mathcal {R}^{\sharp }_{0}= \varGamma _{0}^{\sharp }\) (i.e., the run with no moves). Then:

The following lemma states that if a contract is liquid w.r.t. some concrete strategy, then is also liquid w.r.t. some abstract strategy, and vice versa. Intuitively, this holds since if it is possible to make a contract evolve with a sequence of moves conforming to any concrete strategy, then the same moves can be also be generated by an abstract strategy.

Lemma 3

Let Open image in new window be a concrete run, and let Open image in new window . \(X_{0}\) is liquid w.r.t. some Open image in new window in Open image in new window iff \(X_{0}\) is liquid w.r.t. Open image in new window in Open image in new window , for some Open image in new window .

Our main technical result follows. It states that liquidity is decidable, and that it is possible to automatically infer liquid strategies for a given contract.

Theorem 4

(Decidability of liquidity). Liquidity is decidable. Furthermore, for any Open image in new window and \(X_{0}\), it is decidable whether there exists a strategy Open image in new window such that \(X_{0}\) is liquid w.r.t. Open image in new window in Open image in new window . If such strategy exists, then it can be automatically inferred given Open image in new window and \(X_{0}\).

Proof

Let Open image in new window be an honest participant with strategy Open image in new window , let Open image in new window be a concrete run, and let \(X_{0}\) be a set of contract names in Open image in new window . By Lemma 3, \(X_{0}\) is liquid w.r.t. Open image in new window iff there exists some abstract strategy Open image in new window such that \(X_{0}\) is liquid w.r.t. Open image in new window . By Lemma 2, \(X_{0}\) is liquid w.r.t. Open image in new window iff \(X_{0}\) is \(\sharp \)-liquid w.r.t. Open image in new window . By Theorem 1, the abstract semantics is finite, and so the possible abstract strategies are finite. Therefore, \(\sharp \)-liquidity is decidable, and consequently also liquidity is decidable. Note that this procedure also finds a liquid strategy, if there exists one.    \(\square \)

6 Conclusions

We have developed a theory of liquidity for smart contracts, and a verification technique which is sound and complete for contracts expressed in BitML. Our finite-state abstraction can be applied, besides liquidity, to verify other properties of smart contracts. For instance, we could decide whether a strategy allows a participant to always terminate a contract within a certain deadline. Additionally, we could infer a strategy which guarantees that the contract terminates before a certain time (if any such strategy exists), or infer the strategy that terminates in the shortest time, etc. Although our theory is focussed on BitML, the various notions of liquidity we have proposed could be applied to more expressive languages for smart contracts, like e.g. Solidity (the high-level language used by Ethereum). To the best of our knowledge, the only form of liquidity verified so far in Ethereum is the “strategyless multiparty” variant, which only requires the existence of a cooperative strategy to unfreeze funds (this property is analysed, e.g., by the Securify tool [35]). Since Ethereum contracts are Turing-powerful, verifying their liquidity is not possible in a sound and complete manner; instead, the reduced expressiveness of BitML makes liquidity decidable in that setting.

Footnotes

  1. 1.

    This assumption, while helpful to simplify the subsequent technical development, does not allow an adversary to steal money; at worst, the adversary can use the authorization to transfer the money back to the original owner.

  2. 2.

    Note that Open image in new window could increase his probability to win the lottery by choosing a secret with length \(N>1\). However, doing so will make Open image in new window lose his Open image in new window deposit in the first part of \(\texttt {split} \), and so Open image in new window ’s average payoff would be negative.

  3. 3.

    A specific choice of \(\mathcal {T}_{}\), which considers all the deadlines in the contracts Open image in new window under observation, is defined later on (Definition 8).

Notes

Acknowledgements

Massimo Bartoletti is partially supported by Aut. Reg. of Sardinia projects Sardcoin and Smart collaborative engineering. Roberto Zunino is partially supported by MIUR PON Distributed Ledgers for Secure Open Communities.

References

  1. 1.
    Understanding the DAO attack, June 2016. http://www.coindesk.com/understanding-dao-hack-journalists/
  2. 2.
    Parity Wallet security alert, July 2017. https://paritytech.io/blog/security-alert.html
  3. 3.
    A Postmortem on the Parity Multi-Sig library self-destruct, November 2017. https://goo.gl/Kw3gXi
  4. 4.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: Fair two-party computations via Bitcoin deposits. In: Böhme, R., Brenner, M., Moore, T., Smith, M. (eds.) FC 2014. LNCS, vol. 8438, pp. 105–121. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44774-1_8CrossRefGoogle Scholar
  5. 5.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, Ł.: Modeling Bitcoin contracts by timed automata. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 7–22. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10512-3_2CrossRefzbMATHGoogle Scholar
  6. 6.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Secure multiparty computations on Bitcoin. In: IEEE S & P, pp. 443–458 (2014). First appeared on Cryptology ePrint Archive. http://eprint.iacr.org/2013/784
  7. 7.
    Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Secure multiparty computations on Bitcoin. Commun. ACM 59(4), 76–84 (2016)CrossRefGoogle Scholar
  8. 8.
    Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum Smart Contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54455-6_8CrossRefGoogle Scholar
  9. 9.
    Atzei, N., Bartoletti, M., Cimoli, T., Lande, S., Zunino, R.: SoK: unraveling bitcoin smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 217–242. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_9CrossRefGoogle Scholar
  10. 10.
    Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of Bitcoin transactions. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957, pp. 541–560. Springer, Heidelberg (2018).  https://doi.org/10.1007/978-3-662-58387-6_29CrossRefGoogle Scholar
  11. 11.
    Banasik, W., Dziembowski, S., Malinowski, D.: Efficient zero-knowledge contingent payments in cryptocurrencies without scripts. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 261–280. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-45741-3_14CrossRefGoogle Scholar
  12. 12.
    Bartoletti, M., Cimoli, T., Zunino, R.: Fun with Bitcoin smart contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 432–449. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-03427-6_32CrossRefGoogle Scholar
  13. 13.
    Bartoletti, M., Zunino, R.: Constant-deposit multiparty lotteries on Bitcoin. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 231–247. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_15CrossRefGoogle Scholar
  14. 14.
    Bartoletti, M., Zunino, R.: BitML: a calculus for Bitcoin smart contracts. In: ACM SIGSAC CCS, pp. 83–100. ACM (2018)Google Scholar
  15. 15.
    Bartoletti, M., Zunino, R.: Verifying liquidity of Bitcoin contracts. Cryptology ePrint Archive, Report 2018/1125 (2018). https://eprint.iacr.org/2018/1125
  16. 16.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30080-9_7. http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdfCrossRefGoogle Scholar
  17. 17.
    Bentov, I., Kumaresan, R.: How to use Bitcoin to design fair protocols. In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014. LNCS, vol. 8617, pp. 421–439. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44381-1_24CrossRefGoogle Scholar
  18. 18.
    Bhargavan, K., et al.: Formal verification of smart contracts. In: PLAS (2016)Google Scholar
  19. 19.
    Buterin, V.: Ethereum: a next generation smart contract and decentralized application platform (2013). https://github.com/ethereum/wiki/wiki/White-Paper
  20. 20.
    Gilad, Y., Hemo, R., Micali, S., Vlachos, G., Zeldovich, N.: Algorand: scaling byzantine agreements for cryptocurrencies. In: Symposium on Operating Systems Principles, pp. 51–68 (2017)Google Scholar
  21. 21.
    Grishchenko, I., Maffei, M., Schneidewind, C.: Foundations and tools for the static analysis of Ethereum smart contracts. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 51–78. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_4CrossRefGoogle Scholar
  22. 22.
    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243–269. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_10CrossRefGoogle Scholar
  23. 23.
    Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum Virtual Machine. In: IEEE Computer Security Foundations Symposium (CSF), pp. 204–217. IEEE Computer Society (2018)Google Scholar
  24. 24.
    Hirai, Y.: Defining the Ethereum Virtual Machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_33CrossRefGoogle Scholar
  25. 25.
    Klomp, R., Bracciali, A.: On symbolic verification of Bitcoin’s script language. In: Garcia-Alfaro, J., Herrera-Joancomartí, J., Livraga, G., Rios, R. (eds.) DPM/CBT -2018. LNCS, vol. 11025, pp. 38–56. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-00305-0_3CrossRefGoogle Scholar
  26. 26.
    Kumaresan, R., Bentov, I.: How to use Bitcoin to incentivize correct computations. In: ACM CCS, pp. 30–41 (2014)Google Scholar
  27. 27.
    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM CCS, pp. 254–269 (2016)Google Scholar
  28. 28.
    Maxwell, G.: The first successful zero-knowledge contingent payment (2016). https://bitcoincore.org/en/2016/02/26/zero-knowledge-contingent-payments-announcement/
  29. 29.
    Miller, A., Bentov, I.: Zero-collateral lotteries in Bitcoin and Ethereum. In: EuroS&P Workshops, pp. 4–13 (2017)Google Scholar
  30. 30.
    Miller, A., Cai, Z., Jha, S.: Smart contracts and opportunities for formal methods. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 280–299. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-03427-6_22CrossRefGoogle Scholar
  31. 31.
  32. 32.
    Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/bitcoin.pdf
  33. 33.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higherorderlogic, vol. 2283. Springer Science & Business Media, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar
  34. 34.
    Rocket, T.: Snowflake to avalanche: a novel metastable consensus protocol family for cryptocurrencies (2018). https://avalanchelabs.org/avalanche.pdf
  35. 35.
    Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: ACM CCS, pp. 67–82 (2018)Google Scholar

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Università degli Studi di CagliariCagliariItaly
  2. 2.Università degli Studi di TrentoTrentoItaly

Personalised recommendations