Using Symbolic Model Execution to Detect Vulnerabilities of Smart Contracts

Smart contracts are programs that automate agreements between parties without the need for intermediaries. Embedded in a blockchain, they ensure transparency, immutability, and trustworthiness. While efficient, their immutable nature and reliance on internet-connected nodes make them susceptible to attacks. Identifying vulnerabilities before deployment is critical to mitigate risks, prevent catastrophic events, and avoid significant financial losses. This paper introduces a method for detecting vulnerabilities in smart contracts written in Solidity and deployed on the Ethereum blockchain. The approach models a smart contract as an Abstract State Machine (ASM), where the absence of specific vulnerabilities is encoded as invariants. An existing symbolic execution technique for ASM models was extended and improved to enable the processing of the ASM models of the smart contracts. By symbolically executing the ASM, the method identifies faulty execution paths that violate these invariants, exposing potential vulnerabilities in the contract’s behavior. Vulnerable execution scenarios of the smart contract can be generated using the symbolic execution results. As a proof of concept, we show the approach on a running case study, the Auction smart contract. Furthermore, we discuss the results of applying the technique to a number of Solidity smart contracts.