Formal Methods for Secure Bitcoin Smart Contracts

The notion of smart contracts was introduced in 1997 by Nick Szabo, to describe agreements among mutually distrusting parties that can be automatically enforced without resorting to a trusted intermediary. Then, the idea was mostly forgotten due to the technical impossibility to implement it. The advent of distributed ledger technologies, pioneered by Bitcoin, provided a technical foundation to reshape and develop smart contracts. Since smart contracts handle the ownership of valuable assets, attackers may be tempted to exploit vulnerabilities in their implementation to steal or tamper with these assets. For instance, a series of vulnerabilities in Ethereum contracts have been exploited, causing money losses in the order of hundreds of millions of dollars. Over the last years, a variety of smart contracts for Bitcoin have been proposed, both by the academic community and by that of developers. However, the heterogeneity in their treatment, the informal (often incomplete or imprecise) descriptions, and the use of poorly documented Bitcoin features, poses obstacles to the development of secure smart contracts. Using formal models and domain-specific languages to describe the behaviour of the underlying platform, and to model contracts, could help to overcome these security issues, by reducing the distance between the intended behaviour of a contract and the implementation. In this thesis, we propose a formal model of Bitcoin transactions, which is the foundation for a new process algebra for defining Bitcoin smart contracts. Furthermore, we present a toolchain for developing smart contracts in BitML, a domain-specific language based on the contributions of this thesis. Moreover, we propose a new extension to Bitcoin, called neighbourhood covenants, which extends its expressiveness as a smart contract platform. We then exploit neighbourhood covenants to implement fungible tokens on Bitcoin.