Verifying liquidity of recursive Bitcoin contracts
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 f...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6943/pdf |
| _version_ | 1797268507238334464 |
|---|---|
| author | Massimo Bartoletti Stefano Lande Maurizio Murgia Roberto Zunino |
| author_facet | Massimo Bartoletti Stefano Lande Maurizio Murgia Roberto Zunino |
| author_sort | Massimo Bartoletti |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:33:35Z |
| format | Article |
| id | doaj.art-9742699dfad74cb68d07b5acffb51928 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:35Z |
| publishDate | 2022-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-9742699dfad74cb68d07b5acffb519282024-03-08T10:36:53ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-02-01Volume 18, Issue 110.46298/lmcs-18(1:22)20226943Verifying liquidity of recursive Bitcoin contractsMassimo BartolettiStefano LandeMaurizio Murgiahttps://orcid.org/0000-0001-7613-621XRoberto ZuninoSmart 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.https://lmcs.episciences.org/6943/pdfcomputer science - cryptography and security |
| spellingShingle | Massimo Bartoletti Stefano Lande Maurizio Murgia Roberto Zunino Verifying liquidity of recursive Bitcoin contracts Logical Methods in Computer Science computer science - cryptography and security |
| title | Verifying liquidity of recursive Bitcoin contracts |
| title_full | Verifying liquidity of recursive Bitcoin contracts |
| title_fullStr | Verifying liquidity of recursive Bitcoin contracts |
| title_full_unstemmed | Verifying liquidity of recursive Bitcoin contracts |
| title_short | Verifying liquidity of recursive Bitcoin contracts |
| title_sort | verifying liquidity of recursive bitcoin contracts |
| topic | computer science - cryptography and security |
| url | https://lmcs.episciences.org/6943/pdf |
| work_keys_str_mv | AT massimobartoletti verifyingliquidityofrecursivebitcoincontracts AT stefanolande verifyingliquidityofrecursivebitcoincontracts AT mauriziomurgia verifyingliquidityofrecursivebitcoincontracts AT robertozunino verifyingliquidityofrecursivebitcoincontracts |