Static analysis of eWASM contracts

Abstract

In der heutigen Gesellschaft werden Kryptowährungen in den unterschiedlichsten Bereichen genutzt. Neben der klassischen Art von Kryptowährungen wie Bitcoin mit einem Schwerpunkt auf dem direkten Austausch von Coins, bieten andere Kryptowährungen die zusätzliche Möglichkeit Programme auszuführen. Ethereum ist eine derartige Kryptowährungsplattfrom, welche die Ausführung von Programmen, sogenannten Smart Contracts, als Teil der Blockchain ermöglicht. Derzeit werden Smart Contracts in Ethereum in der Ethereum Virtual Machine (EVM) ausgeführt. Das soll sich jedoch im nächsten großen Ethereum Update mit dem Nachfolger Ethereum flavored WebAssembly (eWASM) ändern. Obwohl viele Forschungsprojekte für die EVM Contract Sicherheit vorhanden sind, ist das Gebiet im Bereich von eWASM praktisch unerforscht. Aufgrund der erheblichen Unterschiede zwischen den beiden Ausführungstechnologien ist es wichtig die Sicherheitseigenschaften von eWASM Contracts zu untersuchen. Im Rahmen dieser Arbeit wurde eine statische Analyse von eWASM Contracts erstellt, welche es ermöglicht Sicherheitslücken in der Form von Wiedereintritten zu finden. Nachdem sich eWASM noch in der Entwicklungsphase befindet ist keine komplette Definition der Semantik der Sprache vorhanden. Infolgedessen bestand der erste Schritt daraus mehrere Ressourcen zu erforschen, um einen Einblick in das Verhalten von eWASM zu erhalten. Basierend auf der Forschung wurde eine vollständige und formale semantische Definition der Ausführung von eWASM Contracts formalisiert. Mithilfe der Semantik wurde eine abstrakte Formalisierung in der Zwischensprache HoRSt entwickelt, welche mit dem SMT-Solver Z3 ausgeführt wird. Gemeinsam mit der Entwicklung eines Parsingmechanismuses ermöglicht die Definition von Abfragen eine Analyse der Wiedereintrittsmöglichkeiten. Um die Gültigkeit der Abstraktion bezüglich der Formalisierung zu zeigen muss ein formaler Korrektheitsbeweis geführt werden. Eine Beweisskizze wurde erstellt, welche ein überzeugendes Argument dafür liefert, dass die Abstraktion tatsächlich korrekt ist. Neben der erfolgreichen statischen Analyse von kleineren eWASM Contracts liefert die Arbeit auch eine Einstiegsmöglichkeit für zukünftige Projekte in diesem Gebiet. Es wurde Wert darauf gelegt alle aufgetretenen Schwierigkeiten inklusive der Lösungsversuche und letztendlich ausgewählte Lösungen zu dokumentieren. In zukünftigen oder weiterführenden Projekten können diese Richtungen und deren Auswirkungen als Ausgangspunkt genutzt werden.

In todays society, cryptocurrencies are widely used in diverse fields. Besides the classical direction of cryptocurrencies like Bitcoin with the focus on direct coin exchanges, other cryptocurrencies provide the additional ability of executing complex programs. Ethereum is such a cryptocurrency platform, which supports the execution of programs, called smart contracts, on its blockchain. Currently, smart contracts in Ethereum are executed inside the Ethereum Virtual Machine. This however is planned to change in the next major Ethereum update with eWASM as the successor. While there are many research projects available for EVM contract security, in eWASM this field is virtually unexplored. Due to the substantial amount of differences between the two execution engines, it is vital to explore security properties of eWASM contracts. During this work a static analysis of eWASM contracts was created which is capable of finding reentrancy security vulnerabilities. Since eWASM is still under development, no complete definition of its behavior is available. As a result, the first step was to research several resources in order to gain an insight into the behavior of eWASM. Based on the research, a complete and formal semantic definition of eWASM contract execution was formalized. With the help of this semantics, an abstract formalization was developed in the intermediate language HoRSt which is executed with the SMT solver Z3. Together with the development of a contract parsing mechanism, the definition of reachability queries allows for checking reentrancy possibilities. In order for the abstraction of the formalization to give reliable guarantees, soundness of the abstraction has to be shown. A proof sketch was created, which provides a convincing argument that the abstraction is indeed sound. Besides the successful static analysis of smaller eWASM contracts, the work also represents a stepping stone for future work in this area. Emphasis was placed on highlighting all encountered pitfalls together with contemplated and chosen solutions. In future or continuing projects these directions and respective impacts can be revisited conveniently.