ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts

TL;DR

This paper introduces ESBMC-Solidity, an SMT-based model checker tailored for Solidity smart contracts, which efficiently detects vulnerabilities and provides counterexamples, outperforming other tools in speed and accuracy.

Contribution

The paper presents a novel Solidity frontend for ESBMC, enabling efficient verification of smart contracts with a new benchmark suite for evaluation.

Findings

ESBMC-Solidity detected all vulnerabilities in the benchmark suite.

It was the fastest among compared verification tools.

The tool provided a counterexample for each benchmark.

Abstract

Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.