Towards Principled Compilation of Ethereum Smart Contracts (SoK)

A blockchain is a tamper-proof distributed transaction registry; first popularized by Bitcoin [1], it has now been extended to support storage of arbitrary state and computations in-ledger. Ethereum [2] and its smart contract model have proven to be a very popular choice for this task, routinely managing assets valued in the billions. However, development of such contracts has been anything but easy. While formally specified, the Ethereum execution platform is based on a low-level machine, quite similar to assembly; semantics for contract operations such as call are quite complex, and the need for resource management creates unanticipated modes of failure. The dominant day-to-day programming platform for Ethereum is Solidity [3], an Object-Oriented language that identifies contracts with objects. While reasoning about Solidity programs is much easier than for their bytecode counterparts, it is not extent of challenges either, and moreover, Solidity lacks a source-level semantics, which forces developers to reason over output bytecode again. In this short paper we explore the main barriers to lift in order to achieve a principled compilation strategy for Solidity. We will review the standard concepts on verified and secure compilation, and frame them in the context of the Ethereum platform.