Model Checking Concurrency in Smart Contracts with a Case Study of Safe Remote Purchase

Blockchain technology has evolved beyond its initial role in supporting cryptocurrencies like Bitcoin, with Ethereum introducing smart contracts for decentralised applications in various domains. However, ensuring the safety and security of smart contracts remains a critical challenge, particularly concerning concurrency issues. This is of paramount importance because the smart contract ecosystem is concurrent by nature as its underlying blockchain is decentralised, and the concurrency-related vulnerabilities within smart contracts have resulted in substantial financial losses.We observe that in the literature, concurrency is handled with two strong assumptions, leading to either undetected attacks or false alarms. Taking the Safe Remote Purchase smart contract as a case study, we investigated the root causes and introduced a novel method that incorporates blockchain-specific characteristics into the verification process. Our contributions include a formal framework, an automated model generator, and a compelling case study that illustrates a reduction in false attacks, thus advancing the state of smart contract security in blockchain ecosystems. The formal models and the framework generator are available online at https://github.com/FormalVerificationBlockchain/Concurrency .