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.