Automated Inference on Financial Security of Ethereum Smart Contracts


Wansen Wang and Wenchao Huang, University of Science and Technology of China; Zhaoyi Meng, Anhui University; Yan Xiong and Fuyou Miao, University of Science and Technology of China; Xianjin Fang, Anhui University of Science and Technology; Caichang Tu and Renjie Ji, University of Science and Technology of China


Nowadays millions of Ethereum smart contracts are created per year and become attractive targets for financially motivated attackers. However, existing analyzers are not sufficient to analyze the financial security of a large number of contracts precisely. In this paper, we propose and implement FASVERIF, an automated inference system for fine-grained analysis of smart contracts. FASVERIF automatically generates models to be verified against security properties of smart contracts. Besides, different from existing approaches of formal verifications, our inference system also automatically generates the security properties. Specifically, we propose two types of security properties, invariant properties and equivalence properties, which can be used to detect various types of finance-related vulnerabilities and can be automatically generated based on our statistical analysis. As a result, FASVERIF can automatically process source code of smart contracts, and uses formal methods whenever possible to simultaneously maximize its accuracy. We also prove the soundness of verifying our properties using our translated model based on a custom semantics of Solidity.

We evaluate FASVERIF on a vulnerabilities dataset of 549 contracts 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. We also evaluate FASVERIF on a real-world dataset of 1700 contracts, and find 13 contracts with bugs that can still be leveraged by adversaries online.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {290993,
author = {Wansen Wang and Wenchao Huang and Zhaoyi Meng and Yan Xiong and Fuyou Miao and Xianjin Fang and Caichang Tu and Renjie Ji},
title = {Automated Inference on Financial Security of Ethereum Smart Contracts},
booktitle = {32nd USENIX Security Symposium (USENIX Security 23)},
year = {2023},
isbn = {978-1-939133-37-3},
address = {Anaheim, CA},
pages = {3367--3383},
url = {},
publisher = {USENIX Association},
month = aug

Presentation Video