FinanceFuzz: fuzzing smart contracts with financial properties

Smart contracts are Turing-complete programs that run on blockchain technology, capable of managing on-chain assets according to predefined logic, and become immutable once deployed on the blockchain. In recent years, the value of smart contracts on blockchains, notably Ethereum, has been on the rise. However, the hiding vulnerabilities made the substantial value of smart contracts a target of many hackers, leading to numerous attack incidents. Therefore, vulnerability detection in smart contracts before deployment is essential. Currently, many fuzzers for detecting smart contract vulnerabilities can only identify vulnerabilities based on the execution patterns of the underlying opcodes, overlooking the financial semantic properties of the contracts, which leads to many vulnerabilities being difficult to detect or resulting in a high rate of false positives. To this end, we focus on the financial characteristics of contracts, define contract vulnerability patterns starting from the high-level semantic properties of contracts, and combine fuzzers using evolutionary algorithms and symbolic constraint solving to detect vulnerabilities, culminating in the development of FinanceFuzz . Specifically, FinanceFuzz defines invariant and equivalence properties of finance that contracts should satisfy. Utilizing these properties, FinanceFuzz can generate transaction sequences for testing and identify vulnerable contracts that violate the properties. We conducted experiments on a dataset containing 437 smart contracts from the real world, the experimental results demonstrating that our tool outperforms other state-of-the-art tools in detecting vulnerabilities, achieving higher recall rate without false positive.