Classification Method of Ethereum Smart Contracts Based on Statistical Model Checking

Abstract

The integration of blockchain and smart contracts facilitates efficient and secure data exchange and value transfer. Nevertheless, the reliability of smart contracts has emerged as a critical concern. The vulnerabilities in contracts are intricately linked to their categories, emphasizing the significance of smart contract classification for enhancing code, user, and system security. Formal verification methods offer a robust means to validate the accuracy of contract classification and mitigate vulnerabilities. However, conventional machine learning approaches often lack precision and overlook the impact of account transaction behavior on classification during contract execution. This study introduces an Ethereum smart contract classification methodology based on statistical model detection. Through an examination of five smart contract types and ensuring the logical exclusivity of each, we delineate and formalize the internal logic of each contract type. We establish the contract automata network, devise conversion rules from contract source code to the automata network, and verify class properties using the statistical model detection tool UPPAAL-SMC. Lastly, we showcase the efficacy of our proposed methodology through a practical contract case.