Motivated by the immutable nature of Ethereum smart contracts and of their transactions, quite many approaches have been proposed to detect defects and security problems before smart contracts become persistent in the blockchain and they are granted control on substantial financial value.
Because smart contracts source code might not be available, static analysis approaches mostly face the challenge of analysing compiled Ethereum bytecode, that is available directly from the official blockchain. However, due to the intrinsic complexity of Ethereum bytecode (especially in jump resolution), static analysis encounters significant obstacles that reduce the accuracy of exiting automated tools.
This paper presents a novel static analysis algorithm based on the symbolic execution of the Ethereum operand stack that allows us to resolve jumps in Ethereum bytecode and to construct an accurate control-flow graph (CFG) of the compiled smart contracts. EtherSolve is a prototype implementation of our approach. Experimental results on a significant set of real world Ethereum smart contracts show that EtherSolve improves the accuracy of the execrated CFGs with respect to the state of the art available approaches.
Many static analysis techniques are based on the CFG representation of the code and would therefore benefit from the accurate extraction of the CFG. For example, we implemented a simple extension of EtherSolve that allows to detect instances of the re-entrancy vulnerability.
PDF version of the paper.