An ASM-Based Approach for Security Assessment of Ethereum Smart Contracts

Blockchain-based smart contracts are gaining widespread adoption due to their potential to automate complex transactions securely and transparently. However, ensuring the correctness and security of smart contracts remains a challenge. This paper proposes a novel approach to modeling and verifying Ethereum smart contracts’ exception-related vulnerabilities using Abstract State Machines (ASMs). ASMs provide a formal modeling language that enables the precise representation of system behavior and properties. We developed an ASM model of a Solidity smart contract and demonstrated its use on Unhandled Exception vulnerability identification and check contract correctness. Our approach offers a formal framework for smart contract modeling and verification. It leverages the power of ASM tools to identify vulnerabilities and ensure contract reliability, contributing to more secure and trustworthy blockchain-based applications.