Hallo zusammen,

Bisher haben wir euch viel über unsere theoretischen Ideen und die Garantien erzählt, die wir mit unserem Tool erreichen wollen. Aber natürlich bringt das alles nichts, wenn wir am Ende nicht auch ein funktionierendes Tool haben, mit dem ihr eure Smart Contracts analysieren könnt!

Deshalb haben wir damit begonnen einen Prototypen zu implementieren, in dem wir die gezeigten Ideen umsetzten. In der Praxis bedeutet das natürlich eine erhebliche Menge an Mehraufwand, da wir zunächst eine ganze Reihe an Infrastrukturen aufbauen müssen.

Das folgende Bild gibt einen Überblick über die einzelnen Schritte unseres Prototypen:

Zunächst müssen wir dafür sorgen, dass wir Smart Contracts (die in EVM Bytecode geschrieben sind) überhaupt einlesen können. Der Input, den wir erhalten ist eine simple Folge von Hexadezimalzahlen, diese muss zu nächst in die entsprechende Folge von Instruktionen umgewandelt werden. Dieser Prozess wird auch Disassembling genannt. In einem nächsten Schritt müssen wir aus dem Vertragscode seine abstrakte Ausführungssemantik generieren. Dabei folgen wir der Theorie, die wir in den letzten Beiträgen erklärt haben. Sobald wir dies getan haben, müssen wir die abstrakte Ausführungssemantik noch in ein Format umwandeln, dass für SMT-Solver lesbar ist. Glücklicherweise gibt es dazu ein standardisiertes Format namens smt-lib. Sobald dies getan ist, können wir nun endlich den SMT-Solver (gemeinsam mit einer abstrakten Sicherheitseigenschaft) aufrufen, um die Analyse des Smart Contracts zu starten.

Wir haben unseren Prototypen in Java programmiert. Dies hat sich in unserem Fall sehr angeboten, da diese Programmiersprache weiterverbreitet ist und sich somit interessierte Leute schnell in unseren Code einarbeiten können.

Auch wenn ein Prototyp ein guter Weg ist, um eine erste Einschätzung zur Praktikabilität unseres Ansatzes zu bekommen, ist dieser leider noch weit weg von einem vollständigen und stabilen Tool. Mit welchen Problemen wir bei der Entwicklung des Prototyps kämpfen, werden wir euch in unserem nächsten Post erzählen!

Euer EtherTrust Team