An Automated Analyzer for Financial Security of Ethereum Smart Contracts
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2022
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911788852838400 |
|---|---|
| author | Wang, Wansen Huang, Wenchao Meng, Zhaoyi Xiong, Yan Miao, Fuyou Fang, Xianjin Tu, Caichang Ji, Renjie |
| author_facet | Wang, Wansen Huang, Wenchao Meng, Zhaoyi Xiong, Yan Miao, Fuyou Fang, Xianjin Tu, Caichang Ji, Renjie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2208_12960 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | An Automated Analyzer for Financial Security of Ethereum Smart Contracts Wang, Wansen Huang, Wenchao Meng, Zhaoyi Xiong, Yan Miao, Fuyou Fang, Xianjin Tu, Caichang Ji, Renjie Cryptography and Security 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. |
| title | An Automated Analyzer for Financial Security of Ethereum Smart Contracts |
| topic | Cryptography and Security |
| url | https://arxiv.org/abs/2208.12960 |