论文标题
以太坊智能合约的财务安全自动分析仪
An Automated Analyzer for Financial Security of Ethereum Smart Contracts
论文作者
论文摘要
目前，每年创建数百万个以太坊智能合约，并吸引以财务动机的攻击者。但是，现有的分析仪并不满足精确分析大量合同的财务安全的需求。在本文中，我们提出并实施Fasverif，这是一种自动分析仪，用于对Smart Contracts的财务安全进行细粒度分析。一方面，Fasverif会自动生成用于针对智能合约的安全属性进行验证的模型。另一方面，我们的分析仪会自动生成安全性属性，这与现有的智能合约正式验证符不同。结果，Fasverif可以自动处理智能合约的源代码，并尽可能使用正式方法来同时最大程度地提高其准确性。 我们通过将Fasverif与其他自动工具进行比较来评估Fasverif。我们的评估表明，对于准确性和覆盖漏洞的范围，Fasverif大大优于代表性工具。
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.
