Sound Static Analysis of Smart Contracts
Bugs in smart contracts can cause huge financial losses. We developed an analysis that can guarantee the absence of a dangerous class of such bugs.
In 2020 our team published two papers on the static analysis of Ethereum smart contracts: one, presented at ACM CCS 2020, introduced eThor, our sound static analysis tool for Ethereum smart contracts; the second, presented in the Reliable Smart Contracts Track of ISoLA 2020, summarized our experiences developing eThor and laid out our recommendations for future developers of sound static analyses.
Smart contracts are a novel technology that allows mutually distrusting parties to reach a consensus on the result of a computation, with the most prominent use case being modelling transactions of financial assets. The entirety of the behaviours of such a smart contract is given as program code, which is then executed in a distributed fashion with no single authority being able to intervene on behalf of any of the contracting parties. These properties make bugs in smart contracts potentially devastating and practically impossible to patch after being deployed.
Static analysis allows to analyse the behaviour of smart contracts before deploying them. While existing static analysis tools were able to find certain cases of problematic behaviour, they were not able to guarantee the absence of problematic behaviours. eThor is the first static analysis tool for Ethereum smart contracts that comes with a mathematical proof of soundness, meaning that it can give such a guarantee.
A summary of the contributions of eThor is given in our CCS 2020 talk: watch at youtube
Our ISoLA 2020 talk describes in detail what difficulties we encountered while designing a sound static analysis and where previous tools failed: watch at youtube
For a humorous summary of the project’s history, check out our CCS 2020 Teaser! watch at youtube