Ethereum introduced the smart contract concept that opened a new era of economy building on the blockchain. However, smart contracts are nothing more than code โ and is code is never bug-free. Many attacks have already been reported resulting in millions of ETH being stolen and security has become one of the biggest issues for smart contract deployments.
To discover smart contract vulnerabilities, many auditing tools were developed, but they all suffer from some drawbacks. Symbolic execution tools (such as Manticore & Mythril) can be used for auditing targeted smart contract binaries but require human setup for each binary. Pattern-based property behaviors analyzers (Securify) can only detect patterns bugs and fail on integer overflows and logical bugs. Call-path conditions based analyzers (Oyente) cannot handle bugs involved in multi-transactions calls.
This presentation introduces a new approach to finding bugs in smart contracts using symbolic execution that is not pattern-based. We developed a specialized tool we call RK87 to automatically verify ERC20 contracts without human interaction. Early results are promising: RK87 can accurately detect most bugs reported in 2018 and has helped us find many unpublished ones.
