A minimal core calculus for Solidity contracts

TL;DR

This paper introduces a minimal formal calculus for Solidity contracts, enabling reasoning about contract behaviors and common issues like re-entrancy on the Ethereum blockchain.

Contribution

It presents the first minimal formal semantics for Solidity, extending an imperative core with primitives for currency transfer and contract invocation.

Findings

The calculus can model Solidity's re-entrancy behavior.

It provides a basis for reasoning about Solidity contract semantics.

The formalization captures key Solidity features and quirks.

Abstract

The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we propose a minimal calculus for Solidity contracts, which extends an imperative core with a single primitive to transfer currency and invoke contract procedures. We build upon this formalisation to give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some typical quirks of Solidity, like e.g. re-entrancy.