Developing secure Bitcoin
contracts withBitML
Stefano Lande
Nicola Atzei
Massimo Bartoletti
University of Cagliari

Nobuko Yoshida
Imperial College London

Roberto Zunino
University of Trento

Contracts as programs vs contracts as protocols
Contracts as programs

Contracts as protocols

Complexity ofblockchain design

High

Low

(gas, VM, compilers,…)(well understood security)

Ease of programming

High

Low

(Solidity, …)(Protocols + redeem scripts)

YesNo(sound ⇒ not complete)(1 contract → 1 proof)

Automatic verification

Can we get the best of both?
(without creating a new coin)2Smart contracts on Bitcoin

Revealwit: s sigA(Reveal)

Commitout: 1 BTC:
fun x σ . ( H(x)=h and verA(σ) )or afterAbs t: verB(σ)

Timeout
wit: * sigB(Timeout)
absLock: tProtocol quoted from: Andrychowicz et al. "Secure multiparty computations on Bitcoin."3

Languages for Bitcoin scripts
Balzac (UniCa)

Ivy (Chain)transaction T_commit(h, deadline) {contract Commit(kApub,kBpub: PublicKey,input = A_funds: sig(kA)

deadline: Time,output = this.input.value:h: Sha256(Bytes),v: Value) {fun(x,s:string) .

clause reveal(s: Bytes, x: Signature) {sha256(s) == h && versig(kApub;x)verify sha256(s) == h|| checkDate deadline: versig(kBpub;x)}verify checkSig(kApub, x)
unlock v

Miniscript (Blockstream)}clause timeout(x: Signature) {or(verify after(deadline)and(pk(A), sha256(H)),

verify checkSig(kBpub, x)and(pk(B), after(deadline))

unlock v)}}

4

BitML: Bitcoin Modelling Language
C ::= D1 + ⋯ + Dn

contract

D ::=guarded contract

withdraw A

transfer balance to A

split v1→C1|⋯|vn→Cn

split balance

A : D

wait for A’s authorization

after t : D

wait until time t

put x . C

collect deposit x

reveal a b … if p . C

reveal secrets a, b, ...
5A basic example
Precondition: A must put a 1฿:{A:!1฿}Contract:
PayOrRefund = A:withdraw B + B:withdraw A
Problem: if neither A nor B give their authorization, the 1฿ deposit is frozen

6Mediating disputes (with oracles)
Resolve disputes via a mediator M (paid 0.2฿)Escrow =A:withdraw B + B:withdraw A+ A:Resolve+ B:Resolve

Resolve = split
0.2฿ → withdraw M|

0.8฿ → M:withdraw A + M:withdraw B

7

The timed commitment in BitML
Precondition:{A:!1฿ | A:secret a}
Contract:

reveal a. withdraw A+ after t : withdraw B
8

The compiled timed commitment

TA
Tinit
out: 1 BTC:
fun x σ σ’ . ( H(x)=h and verA,B(σ,σ’) )or afterAbs t: verA,B(σ,σ’)

wit: s sigA sigB
out: 1 BTC:
fun σ . verA(σ)
TB
wit: 0 sigA sigB
out: 1 BTC:
fun σ . verB(σ)
absLock: t

9

A 2-players lottery{A:!3฿ | A:secret a | B:!3฿ | B:secret b}

split
2฿ → reveal b . withdraw B+ after t: withdraw A|2฿ → reveal a . withdraw A+ after t: withdraw B|2฿ → reveal a b if a=b . withdraw A+ reveal a b if a≠b . withdraw B
10

A 2-players lottery (fair version){A:!3฿ | A:secret a | B:!3฿ | B:secret b}

split
2฿ → reveal b if 0≤b≤1 . withdraw B+ after t: withdraw A|2฿ → reveal a . withdraw A+ after t: withdraw B|2฿ → reveal a b if a=b . withdraw A+ reveal a b if a≠b . withdraw B11

Compiler security

BitML

Bitcoin12Veriﬁcation
BitML supports the automatic verification of contract properties.
■

Contract-dependent properties (expressed as LTL formulae)
TimedCommitment ⊨ □ ♢(B knows a or B has 1 BTC)■

Liquidity: funds are never “frozen” in the contract (⇒ Eth Parity Wallet)
A:B:withdraw C+

A:B:withdraw DNo liquid strategy for A, because A requires the cooperation of B
13

BitML toolchain

https://github.com/bitml-lang/14

Benchmarks & tool demo
Contract# Part# Tx

Ver. time

Mutual timedcommitment

21583 ms

Escrow

3128s

Coupon Bond

3

18

1.3 s

Lottery

28142 ms

Lottery

4587

67 h

Rock Paper Scissors

223781 ms

Morra240674 ms

Auction2423s...

All the tx are standard ( → they respect the 520-bytes constraint)
15

BitML wishlist #1
Bitcoin completeness: extend BitML to make it expressive as Bitcoin■ Find participants at runtime■ SIGHASH modesadd 1 BTC. C■ Relative timelocks

in 3 days: C■ Dynamic stipulation of subcontracts

A: B: new C(x)16BitML wishlist #2

Currently, each step in the execution of a contract
corresponds to an on-chain transaction
BitML layer 2:■ Execute BitML contracts oﬀ-chain■ In case of dispute, revert to on-chain execution

17

BitML wishlist #3

BitML over Taproot■ Exploit forthcoming MAST and Schnorr signatures■ Unexecuted script branches remain oﬀ-chain● More space eﬀicient● Increases expressivity (520 bytes limit)■ Private: hides unexecuted script branches
18

“Thank you
BitML toolchainlande@unica.it

19

Balzac online editorReferences
N. Atzei, M. Bartoletti, S. Lande, N. Yoshida, R. Zunino
Developing secure Bitcoin contracts with BitML. ESEC/FSE, 2019
M. Bartoletti, R. Zunino.
BitML: a calculus for Bitcoin smart contracts. ACM CCS, 2018
M. Bartoletti, R. Zunino
Verifying liquidity of Bitcoin contracts. POST 2019
M. Bartoletti, T. Cimoli, R. Zunino.
Fun with Bitcoin smart contracts. ISOLA 2018
N. Atzei, M. Bartoletti, T. Cimoli, S. Lande, R. Zunino.
SoK: unraveling Bitcoin smart contracts. POST 2018
N. Atzei, M. Bartoletti, S. Lande, R. Zunino.
A formal model of Bitcoin transactions. Financial Cryptography, 201820

The BitML toolchain■

Paper:

https://arxiv.org/abs/1905.07639■

Tutorial: https://blockchain.unica.it/bitml

■

Demo:

■

Github: https://github.com/bitml-lang

https://youtu.be/bxx3bM5Pm6c21