Modeling and verification of smart contracts with Abstract State Machines

Blockchain is a decentralized and distributed ledger system that records and verifies transactions across a network of computers and ensures transparency, immutability, and trustworthiness. Smart contracts are programs or protocols embedded into the distributed ledgers and are used to automate agreements between parties of a blockchain. Smart contracts are vulnerable to attacks due to their immutable and public nature, thus, it is important to guarantee the correctness of contracts already at design-time in order to avoid catastrophic events and huge loss of money.In this paper, we investigate the usage of the Abstract State Machine (ASM) formal method for the specification, validation and verification of Ethereum smart contracts. We present the ASM model of the Ethereum virtual machine, and we define a set of ASM libraries that simplify smart contracts modeling. We also provide models of malicious contracts in terms of ASM libraries that can be used to check if a given smart contract is vulnerable to a certain attack. As a proof of concept, we show our approach by exploiting the DAO smart contract and its vulnerability to a reentrancy attack.