EthBMC

View On Github

ETHBMC

Authors:

Joel Frank, Cornelius Aschermann, Thorsten Holz

In this paper we present EthBMC, a highly precise bounded model checker for the Ethereum VM used to implement smart contracts on the blockchain. It is able to check almost arbitrary properties and provide counterexamples for even the most complex smart contracts used in the real world. For example, when expressing the property “at the end of a sequence of transaction, my own account should always have less money than before”, a counter example is a series of transatcions that result in stealing money. EthBMC able to find such exploits automatically for almost three thousand contracts on the block chain. Our modelling is much more precise when handeling complex features of the EVM such as inter contract communication, arbitrary length memory copy operations and cryptographic checksums. Konsquently, we are the first to generate such exploits for unmodified versions of the Parity Wallet.