Verification of Ethereum Smart Contracts

Background

Blockchain-based cryptocurrencies like Bitcoin offer an alternative to traditional fiat currencies. Some of them, e.g. Ethereum, additionally support smart contracts, which offer a way to perform (monetary) transactions between mutually distrusting parties according to a fixed set of rules (the contract). These contracts are programs usually written in a high-level programming language like Solidity and subsequently compiled to bytecode that can be interpreted by the Ethereum Virtual Machine (EVM). Since the contracts potentially handle large sums of money and cannot be changed once deployed, their correct implementation is vital, and must be able to resist attacks by both users and miners. This is illustrated by the recent DAO vulnerability which led to the loss of 60 million dollars.

Project background

Creating a correct and secure smart contract implementation is complex due to, among other things, unforseeable interactions between different contract invocations, peculiar behavior of the EVM (e.g., with respect to handling exceptions), and the need to distrust even the execution context of a contract (which can be partly controlled by the miner). As a result, there has been an effort to develop static analysis and verification tools that prove correctness of such contracts. However, this is difficult because many desirable security properties are hyperproperties (i.e., properties of sets of executions as opposed to properties of single executions), making them difficult to analyze, or result from interleaved contract executions, which are notoriously hard to reason about. The Ethereum team is currently developing the Vyper language, an alternative to Solidity with a Python-like syntax that focuses on building secure and correct contracts; however, while this language removes some pitfalls present in Solidity, writing smart contracts remains challenging.

Goals

The goal of this project is to build a static verifier for Ethereum smart contracts written in the Vyper language. For this purpose, we want to build on our existing infrastructure for verifying (concurrent) Python programs, particularly with respect to hyperproperties, and adapt it to the special requirements of the Ethereum blockchain. This will require

identifying important security properties of smart contracts,
encoding these into machine-checkable assertions,
designing and implementing a verifier for the Vyper language along with a suitable specification language, building on our existing infrastructure, and
evaluating the resulting tool on real smart contracts written in Vyper.

Useful prerequisites

Experience with program verification, especially the Viper framework (not to be confused with the Vyper language), would be helpful but could also be learned during the project.

Opportunities

The project offers the following opportunities:

Gain an understanding of state-of-the-art blockchain technology
Contribute to making smart contracts reliable and secure
Work with and contribute to modern verification tools