Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling

ABSTRACTThe exploitation of smart-contract vulnerabilities can lead to catastrophic losses. Formal verification can be a useful tool in identifying these vulnerabilities before deployment. We present an encoding of Solidity and the Ethereum blockchain using Boogie, an intermediate verification language. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. Distinctive features of our encoding are precisely capturing Solidity's unorthodox memory model, a notion of lazy blockchain exploration, and memory-precise verification harnesses. Unlike much of the work in this area, our modus operandi is not matching contracts against specific known behavioural patterns that might lead to vulnerabilities. Rather, we provide a tool to find errors/bad states - be they vulnerabilities or not - that might be reached through behaviours that might not follow such a pattern.