Detecting Standard Violation Errors in Smart Contracts.

We present Aloes, a new technique and system for automatically detecting software errors in smart contracts. Given the Ethereum Virtual Machine byte code of a smart contract and a user specified constraint or invariant, Aloes symbolically executes the smart contract, explores all possible execution paths, and checks whether it is possible to initiate a malicious transaction to cause the contract violating the specified constraint or invariant. Our experimental results show that Aloes is effective in finding new errors in smart contracts. We applied Aloes to check 779 ERC-20 smart contracts against the ERC-20 standard and Aloes finds 232 standard violation errors and 192 vulnerable contracts with no false positive. 26contracts contain more than one error. 213 out of the 232errors are zero-day errors that are not reported before.