Verifying liquidity of Bitcoin contracts

Massimo Bartoletti; Roberto Zunino

Paper 2018/1125

Verifying liquidity of Bitcoin contracts

Massimo Bartoletti and Roberto Zunino

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 160M USD within the contract, making this sum unredeemable by any user. We address the problem of verifying liquidity of Bitcoin contracts. Focussing on itML, 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 moves of the context. With respect to the chosen contracts, this abstraction in sound and complete. Our decision procedure for liquidity is then based on model-checking the finite space of states of the abstraction. The computational soundness of the BitML compiler allows to lift this result from the symbolic to the computational level: if our decision procedure establishes that a contract is liquid, then it will be such also under a computational adversary, and vice versa.

Metadata

Available format(s): PDF
Category: Applications
Publication info: Preprint.
Keywords: Bitcoin smart contracts verification
Contact author(s): bart @ unica it
History: 2019-02-18: revised; 2018-11-29: received; See all versions
Short URL: https://ia.cr/2018/1125
License: CC BY

BibTeX

@misc{cryptoeprint:2018/1125,
      author = {Massimo Bartoletti and Roberto Zunino},
      title = {Verifying liquidity of Bitcoin contracts},
      howpublished = {Cryptology {ePrint} Archive, Paper 2018/1125},
      year = {2018},
      url = {https://eprint.iacr.org/2018/1125}
}