TLDR:
- The paper introduces BitML, a novel, domain-specific language for writing smart contracts which are realized as protocols on top of Bitcoin.
- A BitML contract can be compiled to a set of standard Bitcoin transactions that enable a contract’s execution.
- It is guaranteed that the execution of these transactions on the Bitcoin blockchain faithfully mimics the behavior of the high-level BitML contract. As a result, one can reason about the correctness of the BitML contract instead of analyzing the resulting Bitcoin protocol.
Core Research Question
How to securely design complex Bitcoin smart contracts?
Citation
Background
- A process calculus is a form of programming language used to model concurrent (communicating) systems. Standard primitives of such calculi include the nondeterministic choice between subprocesses and the parallel execution of several processes.
- A small-step semantics is an operational semantics that describes the behavior of a system by characterizing its individual execution steps.
- Reasoning about cryptographic systems is usually done in the computational model. The term computational refers to the fact that all actors (including attackers) are assumed to be subject to computational restrictions (more precisely, they must run in probabilistic polynomial time). So they are assumed not to have unbounded computational power that would allow for breaking standard cryptographic assumptions (such as RSA). Such assumptions are usually required to prove meaningful security notions of a cryptographic system.
- Since reasoning in the computational model is often cumbersome and lends itself only poorly to automatic verification, one approach is to reason about cryptographic systems in a symbolic model. Symbolic models abstract from cryptographic primitives (with computational security guarantees) by replacing them with syntactic transformations that characterize their behavior when assuming perfect security.
- A computational soundness statement establishes the relation between a symbolic model and a computational model. In this way, it specifies which properties shown to hold in the symbolic model carry over to the computational model.
Summary
The paper presents BitML, a new domain-specific language for programming smart contracts in Bitcoin. Such smart contracts are realized in the form of cryptographic protocols, which can be executed on the blockchain.
The authors first present the BitML language, a process calculus without recursion or communication primitives. A BitML program consists of preconditions and a contract specification. The preconditions determine the coins to be deposited into the contract by the different contract parties. Further, they specify the secrets, to which the parties need to commit prior to contract execution. The contract specification itself describes the rules for the distribution process of the deposited coins. This distribution process may depend on (computation over) the priorly committed secrets.
The authors provide several examples of smart contracts written in BitML. They show how to realize several forms of escrow services, as well as games such as a coin-toss, a Rock-Paper-Scissors game, or a zero-collateral lottery.
The semantics of the BitML language is given in form of a small-step semantics that describes the individual execution steps of a BitML program, which finally lead to a (re)distribution of the deposited coins. During the execution, the initial coins can be split and the different shares can be governed by subcontracts. Also, it is possible that (sub) contracts could get stuck (e.g., when the conditions for advancing the execution of the contract are non-satisfiable).
The authors define a compiler for the BitML language. The compiler, given a BitML contract, generates a set of Bitcoin transactions, which enable any user to advance the BitML contract according to the small-step semantics. These transactions, in particular, include an initial funding transaction that consumes all deposits specified in the contract preconditions, and which needs to be signed by all contract participants
The core result of the paper is BitML’s computational soundness: The authors formally define a computational execution model for Bitcoin, modeling the blockchain and how users can interact with it. Next, they prove that in this computational model (even in the presence of an adversary), each possible run corresponds to a small-step execution (with overwhelming probability). In particular, this correspondence implies that whenever a transaction that was generated by the compiler is appended to the blockchain, this can be reflected by a corresponding execution step in the (compiled) BitML contract. A consequence of this result is that all reasoning about executions on the level of the BitML semantics carries over to the computational model.
Method
The paper lays the foundations for principled generation and reasoning about Bitcoin smart contracts. To this end it:
- develops a new domain-specific language.
- formally defines a semantics for this language.
- formally models the blockchain and how users can interact with it (computational model).
- formally defines a compiler from the domain-specific language (BitML) to a set of Bitcoin transactions.
- formally proves a computational soundness statement between the symbolic model (executions of the small-step semantics) and the computational model (blockchain interactions).
Results
The main results of this work are the design of a novel domain-specific smart contract language, a compiler from smart contracts written in this language into Bitcoin transactions, and a computational soundness statement, which shows compiler correctness.
BitML language is a simple process calculus in its essence. A smart contract advertisement {G} C consists of preconditions G and the contract specification {C} as given by the following grammar:
The language is expressive enough to formulate smart contracts such as escrow services, lotteries or games.
The BitML compiler takes as input a contract advertisement and returns a set of Bitcoin transactions that implements the contract.
The correctness of the compiler is formally established by a computational soundness statement:
The statement, intuitively, says that for every execution on the blockchain (potentially involving the transactions produced by the compiler), with overwhelming probability there is an execution in the symbolic execution of the original BitML contract, which relates to the (computational) execution. Or, put simply, whatever can happen on the blockchain finds a correspondence in the execution of the BitML contract in the formal (symbolic) model.
Discussion and Key Takeaways
The BitML language can express many Bitcoin smart contracts from the literature, but it is not complete. This means that BitML is not capable of expressing all smart contracts that are realizable as Bitcoin protocols. For example, it is not possible to express contingent payments (via off-chain protocols) or to model smart contracts for which the participants or the number of execution steps are not finite and known upfront. E.g., it would not be possible to express a crowdfunding smart contract where the set of participants will only be known at the time of the execution.
The soundness statement of the paper allows for proving safety properties about Bitcoin smart contracts written in BitML. Therefore, every safety property proven in the symbolic model for a BitML contract is guaranteed to hold in the computational model (so for the concrete blockchain execution). Safety properties are properties that can be formulated in terms of the contract execution not entering certain bad states. Since BitML only supports finite executions, safety properties actually span all properties that concern a single execution of the contract.
Implications and Follow-ups
The main goal and implication of the work presented in the paper is that users can write smart contracts for Bitcoin in a high-level language and reason about the properties of those contracts at the level of that language. This promises to make the development of Bitcoin smart contracts much less error-prone. For example, it is possible to design a Bitcoin smart contract in BitML and then show that this contract can never get stuck (which would then imply that an execution of the contract can never burn coins). This proof can be conducted on the level of the BitML language, which comes with well-defined semantics. Thanks to the computational soundness statement, this property is guaranteed to also hold in real blockchain executions.
The symbolic execution model of BitML has the potential for tool assistance in proving properties on the level of BitML:
In a follow-up work, the authors propose a toolchain for automatically verifying BitML smart contracts for the liquidity property - the property that excludes that coins may be frozen during the contract execution.
In another follow-up work, it is shown how BitML can be extended with recursion. This increases the expressiveness of BitML, hence allowing for realizing a broader class of Bitcoin smart contracts using BitML.
Applicability
By providing the specifications of the BitML language and its semantics, as well as showing a practical tool-chain leveraging this results in follow-up work, the authors give a clear perspective of how BitML can be used to write and verify Bitcoin smart contracts in practice.
BitML can be used as a specification format that automatically compiles into Bitcoin transactions. The verification of the contract can be performed on the level of BitML and can make use of automatic verification tools (e.g., model checking).