Post date: 12-Apr-2019 08:02:19
Upcoming paper (to be presented at Principles of Security and Trust, 2019)
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 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 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.