Finding smart contract vulnerabilities with ConCert's property-based testing framework

TL;DR

This paper demonstrates how property-based testing within the ConCert framework can identify vulnerabilities in smart contracts, including a novel ICO example, by combining formal verification with practical testing methods.

Contribution

It introduces a new property-based testing approach integrated with ConCert for detecting smart contract vulnerabilities, including a previously missed ICO case.

Findings

Property-based testing identified vulnerabilities in three case studies.

The approach successfully detected a new vulnerability in Brave's BAT ICO.

ConCert enables generating verified smart contracts in multiple blockchain languages.

Abstract

We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new, and was missed in the auditing process. We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium's rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.