Formal Verification of Smart Contracts

Smart contracts are programs that can be deployed on specific blockchain platforms. Due to the nature of their application, they often hold and manipulate significant financial assets, which marks them as tentative targets for attackers. In addition, their execution in blockchain platforms leads to costs that need to be managed properly, otherwise, users can incur a significant financial loss. In this project, we investigate the application of formal verification in tackling both contracts' safety and execution costs.

The three tracks of this project are:

Safety verification of smart contracts via direct modelling

Existing verification approaches targeting smart contracts often rely on general verification frameworks, which lead to loss of precision and efficiency. We propose a novel approach to smart contracts verification based on the direct encoding of the contracts, natively handling their peculiarities, in a formalism suitable for reasoning engines. Our approach is implemented for Solidity contracts in the constrained Horn clauses (CHC) engine of SMTChecker.

Estimation of smart contracts execution costs

The execution of smart contracts incurs costs based on the computation's complexity, commonly referred to as gas consumption, that is not easily estimated beforehand. Uncertainty in gas consumption may result in inefficiency, loss of money, and, in extreme cases, funds being locked for an indeterminate duration. We propose novel methods, influenced by symbolic model checking, for gas consumption estimation for Ethereum based contracts.

Automated formal-based synthesis of tests

Complete verification of smart contracts might be too costly and the test suite might require a significant amount of human effort to develop. One of the ways to address it is to synthesize tests automatically. We implemented a new tool that enables the formal-based test synthesis of test suite for Solidity smart contracts. It utilises symbolic model checking to attempt reachability of specific locations in the smart contract structure, and aims to gain the highest coverage possible.

 

Publications:

  1. Computing Exact Worst-Case Gas Consumption for Smart Contracts, Marescotti, Matteo, Blicha Martin, Hyvärinen Antti E. J., Asadi Sepideh, and Sharygina Natasha, ISoLA 2018
  2. Accurate Smart Contract Verification through Direct Modelling, Marescotti, Matteo, Otoni Rodrigo, Alt Leonardo, Eugster Patrick, Hyvärinen Antti E. J., and Sharygina Natasha, ISoLA 2020 [ Presentation | Slides | Extended Version ]
  3. SolCMC: Solidity Compiler’s Model Checker, Alt Leonardo, Blicha Martin, Hyvärinen Antti E. J., and Sharygina Natasha, CAV 2022
  4. A Solicitous Approach to Smart Contract Verification, Otoni Rodrigo, Marescotti, Matteo, Alt Leonardo, Eugster Patrick, Hyvärinen Antti E. J., and Sharygina Natasha, TOPS
  5. SolTG: A CHC-based Solidity Test Case Generator, Britikov, Konstantin, Zlatkin Ilia, Fedyukovich Grigory, Alt Leonardo, and Sharygina Natasha , Computer Aided Verification, (2024).