Model Checking of Vulnerabilities in Smart Contracts: A Solidity-to-CPN Approach

Despite the benefits that the Blockchain technology brings to many application fields, its adoption does not come without challenges. Smart contracts, which are at the core of 2nd generation blockchains, can often be riddled with vulnerabilities that can be exploited to attack the platform and threaten its security. It is therefore crucial for the protection of the designed systems to prove the correctness of the smart contracts to be deployed. Approaches have been proposed to detect generic vulnerabilities like reentrancy, but the results would often include false positives where the detected bug is either non existent or not exploitable. Besides, such approaches do not offer to check contract-specific properties. The work presented in this paper is situated as part of a formal approach that we have proposed in an attempt to bridge this gap. This previously outlined approach is based on the transformation of Solidity smart contracts into Coloured Petri nets, which provides the possibility to verify smart contracts with reference to properties expressed as Linear Temporal Logic (LTL) formulae. Herein we extend our previous work on mainly two levels: first, by taking into account the concept of function calls in the transformation and second, by focusing on the LTL properties that can define the correctness of a smart contract. Such properties can be specific to the control- or data-flow of the contracts being checked. They can also be used to express vulnerabilities as we showcase by proposing LTL formalizations for six vulnerabilities from the literature. We then leverage the capability of the Helena model checker to detect these vulnerabilities while discerning their exploitability, as well as check temporal-based contract-specific properties.