Towards benchmarking of Solidity verification tools

TL;DR

This paper introduces an open benchmark for Solidity verification tools to evaluate and compare their effectiveness, addressing the lack of specialized benchmarks for smart contract verification.

Contribution

It proposes a dedicated benchmark for Solidity verification tools and compares two leading tools, SolCMC and Certora, highlighting their strengths and limitations.

Findings

Benchmark reveals differences in tool completeness and soundness.

SolCMC and Certora vary in expressiveness and verification capabilities.

The benchmark facilitates fair comparison of Solidity verification tools.

Abstract

Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockchains. Although bug detection tools for Solidity have been proliferating almost since the inception of Ethereum, only in the last few years we have seen verification tools capable of proving that a contract respects some desirable properties. An open issue is how to evaluate and compare the effectiveness of these tools: indeed, the existing benchmarks for general-purpose programming languages cannot be adapted to Solidity, given substantial differences in the programming model and in the desirable properties. We address this problem by proposing an open benchmark for Solidity verification tools. By exploiting our benchmark, we compare two leading tools, SolCMC and Certora, discussing their completeness, soundness and expressiveness limitations.