Identifying semantic properties in the bytecode of smart contracts using symbolic execution

Abstract

Diese Masterarbeit konzentriert sich auf Programme, die für die Ethereum-Blockchain entwickelt wurden (sogenannte Smart Contracts) und ihren Bytecode. Ethereum’s quasiTuring-vollständige Maschinensprache ermöglicht die Schaffung dezentralisierter Anwendungen durch Smart Contracts. Das große Volumen an täglich eingesetzten SmartContracts stellt jedoch eine Herausforderung dar, sie aufgrund ihrer Funktionalitäten zuanalysieren und zu kategorisieren.Dieses Werk hat das Ziel, Bytecodes basierend auf ihren semantischen Eigenschaften zuerfassen und zu kennzeichnen, wobei Aspekte wie Autorisierung und verschiedene Muster im Fokus stehen. Durch das Identifizieren dieser Merkmale strebt die Arbeit an, einen charakteristischen Fingerabdruck für Verträge zu erstellen, der ihre Klassifikation und Untersuchung vereinfacht.Die angewandte Methodik beinhaltet eine Literaturrecherche, Definition der Eigenschaften,Beschreibung der Analyseansätze und Tools (wie z.B. symbolische Ausführung) sowie die Entwicklung und Bewertung eines Proof-of-Concept-Prototyps. Diese Forschung leistet einen Beitrag zum umfassenderen Verständnis von Ethereum Smart Contracts und gibt Einblicke in ihr Verhalten und mögliche Anwendungen.

This master’s thesis focuses on programs developed for the Ethereum blockchain (socalled smart contracts) and their bytecode. Ethereum’s quasi Turing-complete machinelanguage enables the creation of decentralized applications through smart contracts.However, the sheer volume of smart contracts being deployed daily makes it challenging to analyze and categorize them based on their functionalities.This work aims to detect and tag bytecodes according to their semantic properties,encompassing aspects like authorization and different patterns. By identifying these properties, the thesis endeavors to provide a characteristic fingerprint for contracts,facilitating their classification and exploration.The methodology adopted encompasses a literature review, property definition, describing the analysis approaches and tools (like symbolic execution) as well as the development and evaluation of a proof-of-concept prototype. The research contributes to the broader understanding of Ethereum smart contracts, offering insights into their behavior and potential applications.