Abstract

Symbolic execution is a popular analysis technique used for finding bugs in Ethereum smart contracts. However, symbolic execution is computationally expensive. Furthermore, during the development of smart contracts, analysis is started from scratch for each new version of the software, recomputing many redundant results. Many approaches exist for the optimisation of symbolic execution, one of which is the use of symbolic summaries. In this thesis, we design a technique which efficiently permits the re-use of symbolic summaries between analyses, allowing for incremental symbolic execution for smart contracts. In particular, the technique aims to permit the re-use of summaries for code with syntactic changes. First, we analyse the changes which occur in smart contracts for the design and evaluation of the summary checking approach. We formulate a set of three algorithms that use program normalisation and dataflow analysis to deal with the identified change types. We evaluate the performance of our summary checking approach through three benchmarks, focussing on particular change types, real-world scenarios, and compiler introduced changes. The results show that this technique can be applied effectively in real-world scenarios, allowing for the re-use of, on average, 81\% of symbolic summaries. Furthermore, the methods are particularly effective for program changes resulting from changes in the compiler, reaching a summary re-use rate of 98\%. Finally, in our experiments, summary validation requires an order of magnitude less time than the re-generation of the summaries which remain valid between program versions. In conclusion, the proposed normalisation based summary checking approach is an effective method for incremental symbolic execution by allowing the re-use of symbolic summaries.