University of Twente Student Theses

Login
This website will be unavailable due to maintenance December 1st between 8:00 and 12:00 CET.

Incremental symbolic execution

Honig, J.J. (2020) Incremental symbolic execution.

[img] PDF
875kB
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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:https://purl.utwente.nl/essays/81526
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page