一种用于以太坊智能合约财务安全性的自动化分析器
密码学与安全
2024-03-06 v3
摘要
目前，每年有数百万个以太坊智能合约被创建，并吸引受利益驱动的攻击者。然而，现有分析器无法满足精确分析大量合约财务安全性的需求。本文中，我们提出并实现了FASVERIF，一种用于对智能合约财务安全性进行细粒度分析的自动化分析器。一方面，FASVERIF自动生成模型，以针对智能合约的安全属性进行验证。另一方面，与现有的智能合约形式化验证器不同，我们的分析器自动生成安全属性。因此，FASVERIF能够自动处理智能合约的源代码，并尽可能使用形式化方法以同时最大化其准确性。我们在一个漏洞数据集上将FASVERIF与其他自动化工具进行比较来评估它。我们的评估表明，在准确性和漏洞类型覆盖方面，FASVERIF大幅优于使用不同技术的代表性工具。
引用
@article{arxiv.2208.12960,
title = {An Automated Analyzer for Financial Security of Ethereum Smart Contracts},
author = {Wansen Wang and Wenchao Huang and Zhaoyi Meng and Yan Xiong and Fuyou Miao and Xianjin Fang and Caichang Tu and Renjie Ji},
journal= {arXiv preprint arXiv:2208.12960},
year = {2024}
}