One of the main goals of this series is to provide smart contract developers and auditors a comprehensive guide on options to leverage program analysis during their day to day work. In the following we will discuss the tools and techniques available so far aiming at Ethereum smart contracts analysis.
We decided to focus on approaches that can be used to find errors in already developed contracts; especially those with published or comprehensive papers, open source code, or mature projects. These selected approaches will be presented according to a classification inspired in a work by Grishchenko et al.[1]. Each category will be divided according to the main techniques employed; we provide an introduction to each general technique, and finally expand on the works oriented to smart contract that use it. Some works are just mentioned briefly, while we develop others in their own subsection, because we consider those specially interesting or mature.
Structure
Automated analysis for bug finding
-
Fuzzing
-
Others
Automated analysis for verification of properties
-
Datalog
-
Abstract interpretation
-
Model checking
Frameworks for semi-automated proofs of properties
References
[1] I. Grishchenko, M. Maffei, and C. Schneidewind, “Foundations and tools for the static analysis of ethereum smart contracts,” in International Conference on Computer Aided Verification, pp. 51–78, Springer, 2018.