Advancing symbolic execution tools with a transient storage model for vulnerability detection in smart contracts

Abstract

Diese Arbeit beschäftigt sich mit Transient Storage, welcher als Zwischenspeicher in Smart Contracts dient und Eigenschaften sowohl des flüchtigen Smart Contract Memory (insbesondere die Eigenschaft, nach jeder Transaktion zurückgesetzt zu werden) wie auch des permanenten Smart Contract Storage (insbesondere die Eigenschaft, innerhalb einer Transaktion über mehrere Smart Contract Frames hinweg bestehen zu bleiben) aufweist. Seine korrekte Modellierung ist entscheidend für die präzise Programmanalyse und Schwachstellenerkennung in Smart Contracts. Insbesondere untersucht diese Arbeit die geeignete Modellierung von Transient Storage für Symbolic Execution Tools, mit einem Fokus auf den Trade-off zwischen Genauigkeit und Recheneffizienz bei der Erkennung von Schwachstellen in Smart Contracts. Sie identifiziert Schlüsselfaktoren und deren Implikationen für die Implementierung des Modells, mit dem Ziel, den besten Ansatz zu finden. Wir führen eine vergleichende Analyse der existierenden State-of-the-Art Symbolic Execution Tools durch, gefolgt von der Entwicklung einer Erweiterung für das Symbolic Execution Tool Mythril, die aus der Modellierung des Transient Storage besteht. Die neu entwickelte Erweiterung wird dann systematisch evaluiert, um ihre Effektivität in der Verbesserung der Erkennung von Schwachstellen in Smart Contracts zu bewerten. Die Evaluation zeigt, dass unser Ansatz, ein Python Dictionary statt eines SMT Arrays für die Modellierung des Transient Storage zu verwenden, eine praktikable Alternative darstellt, die Recheneffizienz ohne Einbußen bei der Genauigkeit bietet.

This work focuses on Transient Storage, which serves as an intermediary storage in Smart Contracts and exhibits characteristics of both the volatile Smart Contract Memory (notably the property of being reset after each transaction) and the permanent Smart Contract Storage (notably the property of persisting across multiple Smart Contract frames within a transaction). Its accurate modeling is crucial for precise program analysis and vulnerability detection in Smart Contracts. Specifically, this thesis explores the appropriate modeling of transient storage for symbolic execution tools, focusing on achieving the right balance between accuracy and computational efficiency in detecting vulnerabilities in smart contracts. It identifies key factors and their implications for model implementation, aiming to identify the best approach. We conduct a comparative analysis of existing state-of-the-art symbolic execution tools, followed by the development of an extension to the symbolic execution tool Mythril, that consists of transient storage modeling. The newly developed extension is then systematically evaluated to assess its effectiveness in enhancing the detection of vulnerabilities in smart contracts. The evaluation illustrates that our approach, employing a Python dictionary instead of an SMT array for transient storage modeling, presents a viable alternative offering computational efficiency without compromising accuracy.