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 two 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.

 

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