SmartFast: an accurate and robust formal analysis tool for Ethereum smart contracts

Recently, although state-of-the-art (SOTA) tools were designed and developed to analyze the vulnerabilities of smart contracts on Ethereum, security incidents caused by these vulnerabilities are still widespread. This can be attributed to the fact that each tool has various standards for judging the severity of vulnerabilities. More importantly, tools fail to identify all the vulnerabilities accurately and comprehensively as the evolution of vulnerabilities. To this end, we first propose a vulnerability assessment model to unify the vulnerability measurement standards. Next, we design a static analysis tool called SmartFast, which expresses the contract source code as a novel intermediate representation named SmartIR. Using preset rules and taint tracking technology, SmartFast matches SmartIR to locate the vulnerability code. Furthermore, SmartFast can recommend the optimization of the contract code automatically. Finally, we implement a prototype of SmartFast with 25K lines of code and compare it with 7 SOTA tools on three datasets (a total of 13,687 public contracts). The results indicate that SmartFast is efficient (only took a few seconds per contract) and robust (0.4% failure rate and resistance to the general code confusion methods). Besides, compared with other tools, SmartFast can detect more kinds of vulnerabilities (119) with a higher precision rate (98.43%) and a recall rate (85.12%), which confirms the conclusion of the theoretical analysis in the paper.