ETHBMC: A Bounded Model Checker for Smart Contracts


Research Hub

Research Hub C: Sichere Systeme

Research Challenges

RC 8: Security with Untrusted Components


The introduction ofsmart contractshas significantly advancedthe state-of-the-art in cryptocurrencies. Smart contracts areprograms who live on the blockchain, governing the flow ofmoney. However, the promise of monetary gain has attractedmiscreants, resulting in spectacular hacks which resulted inthe loss of millions worth of currency. In response, severalpowerful static analysis tools were developed to address theseproblems. We surveyed eight recently proposed static ana-lyzers for Ethereum smart contracts and found that none ofthem captures all relevant features of the Ethereum ecosystem.For example, we discovered that a precise memory model ismissing and inter-contract analysis is only partially supported.Based on these insights, we present the design and im-plementation ofETHBMC, a bounded model checker basedon symbolic execution which provides a precise model ofthe Ethereum network. We demonstrate its capabilities in aseries of experiments. First, we compare against the eightaforementioned tools, showing that even relatively simple toyexamples can obstruct other analyzers. Further proving thatprecise modeling is indispensable, we leverageETHBMCca-pabilities for automatic vulnerability scanning.We perform alarge-scale analysis of roughly 2.2 million accounts currentlyactive on the blockchain and automatically generate 5,905valid inputs which trigger a vulnerability. From these, 1,989can destroy a contract at will (so calledsuicidal contracts)and the rest can be used by an adversary to arbitrarily extractmoney. Finally, we compare our large-scale analysis againsttwo previous analysis runs, finding significantly more inputs(22.8%) than previous approaches.


Software Security
Program Analysis