Paper Info
Title
Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling
Abstract
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.
Year
DOI
Venue
2021
10.1145/3412841.3442051
Symposium on Applied Computing
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Pedro R. G. Antonino1334.57
A. W. Roscoe21436247.82