Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity

02/07/2020
by   Pedro Antonino, et al.
0

The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that they have been fixed. In this paper, we present a formalisation of Solidity and the Ethereum blockchain using the Solid language and its blockchain; a Solid program is obtained by explicating/desugaring a Solidity program. We make some abstractions that over-approximate the way in which Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. It translates Solid into Boogie, an intermediate verification language, that is later verified using Corral, a bounded model checker for Boogie. Unlike much of the work in this area, we do not try to find specific behavioural/code patterns that might lead to vulnerabilities. Instead, we provide a tool to find errors/bad states, i.e. program states that do not conform with the intent of the developer. Such a bad state, be it a vulnerability or not, might be reached through the execution of specific known code patterns or through behaviours that have not been anticipated.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset