Abstract

Running on top of blockchain systems, smart contracts enable developers to build decentralized applications with rich functionalities. Many of the contracts are financial-related, which makes code audit rather important. Quantities of static analysis tools have been developed to automate the audit process, but not all of them take account of two special features of smart contracts: (1) The internal variables in contracts persist between executions; (2) The external variables, like time and assets, are constrained by real-world factors. Since these features bring implicit constraints on contract variables, they significantly affect the performance of static analysis tools, such as causing errors in reachability analysis and resulting in false positives, etc. Although a few recent works discussed these features, little is known about their impact on the wildly used tools. In this paper, we conduct a systematic study on such constraints from three aspects. First, we summarize the implicit constraints due to the special features of smart contracts. Second, we evaluate the impact of such constraints on the state-of-the-art static tools used in smart contract audits. The tools we select include both the industrial and academic ones. The experiment results show that six out of seven tools, including the latest verifiers, will be obviously affected by such constraints. Third, we propose a simple but effective method named ConSym to recognize such constraints. It can be easily integrated into existing symbolic execution based solutions to improve their performance. We integrate ConSym into OSIRIS and evaluate it with real-world contracts. The result shows that ConSym can filter out 96% of false positives reported by OSIRIS and achieve 3 times fewer false negatives than OSIRIS.