A Scalable Bug Checking Framework for Smart Contracts

Michael Kong, Lexi Brent, Anton Jurisevic, Bernhard Scholz
University of Sydney

Ethereum is a recent application of blockchain technology, which retains Bitcoin-style externally-controlled accounts and introduces so-called "smart contracts", which are programmatically controlled by computer code. These programs determine how other entities in the network interact with them; a smart contract may define custom behaviour to be performed when receiving value or information from another account, and may respond by itself undertaking transactions with other accounts. Ethereum provides a Turing-complete virtual machine for executing smart contracts. Proof-of-concept implementations of smart contracts for various applications, including voting, financial auditing, sport betting, and music distributions are already available. One such contender was an entire organisation whose steering was determined with the use of smart contracts for voting on projects to be funded (the so-called DAO). Unfortunately, smart contracts are vulnerable if not coded correctly. Last year TheDAO was hacked, with the attacker taking the equivalent of $50 million USD. This hack was possible due to a buggy and ill-defined smart contract.

In this talk, we present a new bug-checking framework that pinpoints potential security vulnerabilities in smart contract bytecode. Unlike some other tools, our framework does not require a contract's original source code or metadata to be available, allowing for both pre-deployment checking of new contracts, and also empirical analyses of deployed contracts. Our bug-checking framework is an extensible research platform, in which new vulnerabilities can be specified easily; such as the vulnerability that was exploited in TheDAO hack. The security vulnerabilities are phrased in a declarative fashion using first-order logic. This permits a rapid-prototyping approach for identifying and reporting new security vulnerability with minimal development time.