EthVer: Formal Verification of Randomized Ethereum Smart Contracts

Despite the great potential capabilities and the mature technological solutions, the smart contracts have never been used at a large scale, one of the reasons being the lack of good methods to verify the correctness and security of the contracts-although the technology itself (e.g. the Ethereum platform) is well studied and secure, the actual smart contracts are human-made and thus inherently error-prone. As a consequence, critical vulnerabilities in the contracts are discovered and exploited every few months. The most prominent example of a buggy con- tract was the infamous DAO attack-a successful attack on the largest Ethereum contract in June 2016 resulting in $70 min-worth Ether stolen and the hard fork of the Ethereum network (80% of Ethereum users decided to revert the transaction and hence two parallel transaction histories exist from that event). The main contribution of this work is the automatic method of formal verification of randomized Ethereum smart contracts. We formally define and implement the translation of the contracts into MDP (Markov decision process) formal models which can be verified using the PRISM model checker-a state of the art tool for formal verification of models. As a proof of concept, we use our tool, EthVer, to verify two smart contracts from the literature: the Rock-Paper-Scissors protocol from K. Delmolino et al., Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab. and the Micropay 1 protocol from R. Pass, a. shelat, Micropayments for decentralized currencies.