Formal Verification of Smart Contracts

TLDR

Ethereum provides a blockchain-based platform where Solidity programs compile to EVM bytecode that executes smart contracts managing Ether, making security essential because public methods can be called by pseudonymous users, leading to risky compositions of trusted and untrusted code. An attack on TheDAO contract exploited subtle EVM semantics to transfer roughly $50 million of Ether to an attacker.

Abstract

Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM code; instead, they can program in a JavaScript-like language, called Solidity, that compiles to bytecode. Since the main purpose of EVM is to execute smart contracts that manage and transfer digital assets (called Ether), security is of paramount importance. However, writing secure smart contracts can be extremely difficult: due to the openness of Ethereum, both programs and pseudonymous users can call into the public methods of other programs, leading to potentially dangerous compositions of trusted and untrusted code. This risk was recently illustrated by an attack on TheDAO contract that exploited subtle details of the EVM semantics to transfer roughly $50M worth of Ether into the control of an attacker.