Hallo zusammen,

Das ist das erste Update zu unserem Projekt EtherTrust, mit dem wir das Entwickeln und Nutzen von Etherum Smart Contracts sicherer machen wollen.

Nachdem wir Mitte November beim netidee Community Camp viele Ideen und Anregungen bekommen haben, haben wir uns dann im Dezember besonders motiviert an die Arbeit gemacht :)

Der erste Teil unserer Arbeit ist dabei hauptsächlich theoretisch. Denn weil wir schlussendlich ein Tool entwickeln wollen, das nicht nur leicht benutzbar ist, sondern auch mathematische Garantien liefert, arbeiten wir erst einmal an den formalen Grundlagen, die benötigt werden um ein solches Tool zu konstruieren. Warum dieser Teil so wichtig ist, wollen wir im Folgenden ein wenig genauer erklären.

Bei der Implementierung von smart contracts kann vieles schiefgehen - schon alleine, weil es für einen Programmierer schwer nachzuvollziehen ist, welche genauen Effekte die Ausführung seines Codes haben wird.Wir wollen den Programmierer durch ein automatischs Tool dabei unterstützen zu verstehen welche (negativen) Folgen das Ausführen eines Contracts haben kann. Aber um das sinnvoll tun zu können, muss das Tool natürlich selbst “wissen”, wie genau der Code des Contracts ausgeführt wird.

Konkret heißt das, dass die Ausführungseffekte (man sagt auch die Semantik) von EVM Bytecode (der Sprache in der Ethereum Smart Contracts geschrieben sind) zunächst einmal auf eine korrekte und für den Computer verständliche Art und Weise definiert werden müssen. Wenn dabei Fehler gemacht werden, kann es sein, dass die Ergebnisse des späteren Tools keinerlei Aussagekraft haben.

Der erste Schritt dazu ist es, die Programmausführung (Semantik) in mathematischer Notation aufzuschreiben. Das hat den Vorteil, das man zwar eine sehr präzise, aber dennoch für den Menschen leserliche Definition hat, die (im Idealfall ;)) dann genau mit dem tatsächlichen Verhalten der Smart Contracts übereinstimmt. Auch die Macher von Ethereum haben eine solche mathematische Spezifikation geschrieben - in ihrem so genannten Yellow Paper (wenn ihr daran interessiert seid und euch gerne durch ein paar Formeln kämpft, könnt ihr es hier nachlesen: https://github.com/ethereum/yellowpaper).

Dass das Erstellen einer korrekten Semantik alles andere als einfach ist, kann man daran sehen, dass selbst das Yellow Paper noch relativ viele Kinderkrankheiten hat: Es ist (auch für Menschen die gerne und häufig formale Semantiken lesen ;)) in Teilen sehr schwer zu verstehen, an einigen Stellen lässt es mehrere Interpretationen zu und manchmal beschreibt es schlichtweg ein anderes Verhalten als der EVM Bytecode bei der Ausführung dann tatsächlich zeigt.

Vor zwei Wochen waren wir kurzzeitig doch einmal ziemlich überrascht, weil wir auf genau so eine Stelle gestoßen sind: Die formale Semantik im Yellow Paper hat ein Verhalten beschrieben, dass es einem Ethereum-Nutzer ermöglicht sehr viel Geld von anderen Netzwerkteilnehmern zu stehlen!

Und trotzdem verfassen wir diesen Post gerade nicht auf unser Yacht vor den Bahamas ;). Das liegt nicht (nur) an unserer moralischen Integrität, sondern vor allem daran, dass die tatsächliche Ausführung von EVM Bytecode ein anderes Verhalten zeigt, das zum Glück sehr viel sicherer ist, als das was im Yellow Paper beschrieben wird.

Trotzdem zeigt dieses Beispiel, wie wichtig eine korrekte semantische Spezifikation ist! Vor allem, wenn man bedenkt, dass auch der umgekehrte Fall eintreten könnte: Ein sicheres Verhalten wird in der Semantik beschrieben, aber ein unsicheres tritt in der Realität auf. Ein Analysetool, das auf einer solchen Semantik basiert, könnte den Nutzer dann in keinem Fall vor der existierenden Gefahr warnen.

Damit wir eine gute Grundlage für unser Analysetool haben, arbeiten wir gerade an einer eigenen Semantik für Ethereum smart contracts, die wir dann auch gegen die echte Implementierung testen können.

Nach Weihnachten werden wir damit auch wieder tatkräftig weitermachen.

Bis dahin wünschen wir euch aber allen schöne Feiertage und einen guten Rutsch ins neue Jahr!

Euer EtherTrust Team