Building trustworthy smart contracts using interactive theorem proving

Abstract

There are varying approaches to the verification of smart contracts using formal methods. This thesis advocates for the use of high-level specifications coupled with a verified compiler to low-level bytecode, such as for the Ethereum Virtual Machine. Taking this approach allows for specifications to more closely match natural language, while ensuring that the specifications apply to the real bytecode executed on-chain.

Interactive theorem proving can provide the foundation for developing provably correct smart contracts. Due to the immutable nature of smart contracts and their potential to manage highly valuable assets and tokens representing power, techniques to ensure their correctness are of paramount importance.

This thesis extends the DeepSEA (Deep Simulation of Executable Abstractions) smart contract language targeting the Ethereum Virtual Machine by mitigating the issues associated with reentrancy and introducing a model of relevant aspects of a blockchain. This enables the specification and verification of two case studies which exemplify the approach of developing provably correct smart contracts.

The specifications for the case studies are written in the language of the Coq Proof Assistant, making arbitrary mathematical statements expressible. The blockchain model enables stating and proving temporal properties relating to the execution of smart contract over time.

While smart contracts are an ideal application area for formal methods in general and interactive theorem proving in particular, the techniques exemplified in this thesis could be applied throughout software engineering. The relatively young age of smart contract languages and typically small size of smart contract programs makes the application of interactive theorem proving more tractable. Future work could involve demonstrating the applicability to many interrelated smart contracts and to larger software projects in different domains.

The first three chapters of this thesis cover introductory and background material. This is followed by the contributions to the DeepSEA system. The two case studies and the proof themes arising from them are then presented. Finally, concluding remarks and future work are discussed.