At present, millions of Ethereum smart contracts are created per year and attract financially motivated attackers. However, existing analyzers do not meet the need to precisely analyze the financial security of large numbers of contracts. In this paper, we propose and implement FASVERIF, an automated analyzer for fine-grained analysis of smart contracts' financial security. On the one hand, FASVERIF automatically generates models to be verified against security properties of smart contracts. On the other hand, our analyzer automatically generates the security properties, which is different from existing formal verifiers for smart contracts. As a result, FASVERIF can automatically process source code of smart contracts, and uses formal methods whenever possible to simultaneously maximize its accuracy. We evaluate FASVERIF on a vulnerabilities dataset by comparing it with other automatic tools. Our evaluation shows that FASVERIF greatly outperforms the representative tools using different technologies, with respect to accuracy and coverage of types of vulnerabilities.

翻译：当前，每年有数百万个以太坊智能合约被创建，并吸引着受经济利益驱动的攻击者。然而，现有分析器无法满足对大量合约进行精确金融安全分析的需求。本文提出并实现了FASVERIF——一个用于智能合约金融安全细粒度分析的自动化分析器。一方面，FASVERIF能够自动生成待验证的模型，用于检查智能合约的安全属性；另一方面，与现有智能合约形式化验证工具不同，我们的分析器能自动生成安全属性。由此，FASVERIF可自动处理智能合约源代码，并在可能的情况下优先采用形式化方法以最大化分析精度。我们通过与其他自动化工具进行漏洞数据集对比评估发现，FASVERIF在漏洞类型的检测精度和覆盖率方面显著优于采用不同技术的代表性工具。