Developing secure bitcoin contracts with BitML

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

Abstract

We present a toolchain for developing 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.

BibTeX

@inproceedings{Atzei-al:FSE19,
  author    = {Nicola Atzei and
               Massimo Bartoletti and
               Stefano Lande and
               Nobuko Yoshida and
               Roberto Zunino},
  title     = {Developing secure bitcoin contracts with {BitML}},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {1124--1128},
  publisher = {{ACM}},
  year      = {2019},
}

Developing secure bitcoin contracts with BitML

Abstract

Related papers