Poster: VeriSol-MCE: Verification-Based Condition Coverage Analysis of Smart Contracts Using Model Checker Engines

Abstract

Advancements in blockchain technologies empower society with trust-based applications. Smart contracts, which are programs designed to facilitate activities on the blockchain, serve as important instruments for executing agreements. Smart contracts are established among involved parties to codify their respective requirements and commitments. In various situations, where a smart contract manages substantial and valuable transactions, the likelihood of encountering issues and asset losses increases significantly. Therefore, it becomes essential to verify and test smart contracts thoroughly. In this paper, we present a new tool to measure condition coverage criterion for smart contracts using Solidity-based model checkers. We demonstrate the process of annotating the original smart contract by the condition coverage properties and employ the model checker to validate the feasibility of the specified properties. Further, we assess the properties instrumented to compute the condition coverage score. We conducted experiments on 70 smart contracts, employing both the Bounded Model Checker (BMC) and Constrained Horn Clauses (CHC). Our findings demonstrate BMC's superior performance compared to CHC. The tool we propose assists smart contract developers in verifying their code through condition coverage analysis. Utilizing both model checkers in tandem contributes to enhancing the quality of smart contracts, as the outcome may vary, and either of the checkers might yield superior condition coverage. Video-cast: https://youtu.beI13kuIjpPGPI?si=YQIWYPJhp7vzORI4