Executing, verifying and enforcing credible transactions on permissionless blockchains is done using smart contracts. Smart contracts define and execute crucial agreements, and attacks exploiting their vulnerabilities can lead to huge losses, like the failure of the DAO smart contract that resulted in 50 million US Dollars worth of losses. A key challenge with smart contracts is ensuring their correctness and security.
To address this challenge, we present a fully automated technique, SolAnalyser, for vulnerability detection over Solidity smart contracts that uses both static and dynamic analysis. Analysis techniques for smart contracts in the literature rely on static analysis with a high rate of false positives or lack support for vulnerabilities like out of gas, unchecked send, timestamp dependency. We instrument the original smart contract with property checks and use dynamic analysis to tackle this problem. Our tool, SolAnalyser, supports automated detection of 8 different vulnerability types that currently lack wide support in existing tools, and can easily be extended to support other types. We also implemented a fault seeding tool that injects different types of vulnerabilities in smart contracts. We use the mutated contracts for assessing the effectiveness of different analysis tools.
Our experiment uses 1838 real contracts from which we generate 12866 mutated contracts by artificially seeding 8 different vulnerability types. We evaluate the effectiveness of our technique in revealing the seeded vulnerabilities and compare against five existing popular analysis tools – Oyente, Securify, Maian, SmartCheck and Mythril. This is the first large scale evaluation of existing tools that compares their effectiveness by running them on a common set of contracts. We find that our technique outperforms all five existing tools in supporting detection of all 8 vulnerability types and in achieving higher precision and recall rate. SolAnalyser was also faster in analysing the different vulnerabilities than any of the existing tools in our experiment. Among existing tools, Securify achieved high precision in detecting integer overflow, underflow, and division by zero but had poor recall rates.