Formal Verification of Atomicity Requirements for Smart Contracts

Abstract

Smart contracts are notoriously vulnerable to bugs and loopholes. This is due largely to an unusual combination of features: re-entrant calls, transfer-triggered code execution, the way exceptions are propagated, etc. Numerous validation techniques have been developed to ensure the safety and security of smart contracts. An important class of problems dealt with is related to the atomic performance of actions such as contract calls and state updates. In this paper, we examine the major existing atomicity-related criteria for the safety and security of smart contracts. We then propose an atomicity criterion and argue about its advantages. Furthermore, we develop a Hoare-style program logic that is capable of verifying the fulfillment of safety requirements by smart contracts, including the satisfaction of the proposed criterion. The program logic is developed and proven sound for a core Solidity-like language, which supports reentrant calls, ether transfers, and exception handling.