An Empirical Evaluation of the Effectiveness of Smart Contract Verification Tools

Abstract

Blockchain has become popular due to its use in cryptocurrencies and potential to support different business-critical services (e.g., financial services, retail). The smart contract is at the center of blockchain systems and is a coded specification of an agreement between interacting partners in a transaction. Like other software artifacts, smart contracts are prone to carry residual faults. As many contracts are being used to handle financial transactions, huge losses may occur if a vulnerability is exploited. Also, a faulty contract cannot be corrected once it has been deployed on the blockchain, it can only be terminated and a new one must be deployed, which aggravates the cost of deploying contracts with faults and marks the reputation of the provider. Smart contract verification tools have been emerging, but limited knowledge is available regarding their real effectiveness. In this paper, we define a smart contract defect classification scheme based on the Orthogonal Defect Classification and apply it to a contract dataset, which has been extracted from multiple sources and holds different types of defects. We use the dataset to evaluate three state of the art verification tools regarding their fault detection performance. Results show the relatively low effectiveness of the tools and their complementarity.