Hallo zusammen,

Im letzten Blogpost, haben wir euch erklärt, mit was für einer Art logischer Probleme ein sogenannter SMT-Solver zurecht kommt. Hier wollen wir euch nun zeigen, wie wir die Ausführung von Smart Contracts auf diese Art und Weise formulieren können.

Wie bereits in der Roadmap erklärt, ist es unser Ziel, dass wir eine abstrakte Semantik (also eine abstrahierte Beschreibung der Ausführung) von Smart contracts als Horn Clauses (also logische Zusammenhänge) definieren. Wie das generell funktioniert, wollen wir euch hier erkl¨åren. Wir hoffen, dass ihr so eine grobe Idee davon bekommt, welche Technik hinter unserem Projekt steht.

Wie wir euch in unserem ersten Blog-Post berichtet haben, wird auch die eigentliche Semantik (also die konkrete Ausführung) von Smart Contracts zunächst in mathematischer Sprache formuliert. Eine Möglichkeit dies zu tun, ist eine sogenannte small-step Semantik zu verwenden. Dabei beschreibt man jeden einzelnen Ausführungsschritt, den ein Smart Contract machen kann. Ein Ausführungsschritt ist dabei eigentlich nur eine Veränderung in der Konfiguration des Programmes bzw. in unserem Fall des Vertrages. Eine Konfiguration ist dabei ein allgemeiner Begriff um alle Aspekte zu beschreiben, die für die Ausführung eines Programmes interessant sind. Im Fall von Ethereum Smart Contracts sind dies sehr viele unterschiedliche Aspekte: Man muss wissen, wie der Zustand des eigenen Vertrags ist, was also in seinem Speicher steht, wie viel Geld er gerade hat und das gleiche muss man auch von den anderen Verträgen auf der Blockchain wissen. Darüber hinaus liegt der Ausführung von EVM-Code ein bestimmtes Berechnungsmodell zugrunde, welches modelliert werden muss. All dies steckt in der Konfiguration. Um die Ausführungsschritte formal zu beschreiben, benutzt man häufig Inferenzregeln. Eine solche Inferenzregel hat in diesem Fall die folgende Form

<Bedingungen für C1>

<Bedingungen für C2>

—————————-

C1 ➝ C2

und meint, dass falls die Bedingungen (über dem Schritt, häufig auch Prämissen genannt) erfüllt sind, dann kann das Programm in einem Schritt von Konfiguration C1 in die Konfiguration C2 übergehen.

Wenn wir nun eine solche Darstellung unserer Semantik haben, können wir uns überlegen, wie wir diese mithilfe von Horn Clauses darstellen können. Die generelle Idee ist gar nicht so schwer:

Angenommen, wir haben ein Prädikat isReachable(x), das beschreibt, ob eine Konfiguration x eine erreichbare Konfiguration eines bestimmten Smart Contracts ist, den wir analysieren und angenommen wir können alle Bedingungen für C1 durch ein Prädikat P(x) beschreiben und alle Bedingungen für C2 durch ein Prädikat Q(x). Dann können wir mithilfe eines Horn Clauses einen Ausführungsschritt wie folgt beschreiben:

∀ C1, C2, P(C1) /\ isReachable(C1) /\ Q(C2) → isReachable(C2)

Die Regel besagt, dass wenn C1 und C2 alle Bedingungen gemäß der obigen Regeln erfüllen und bekannt ist, dass man Konfiguration C1 bei Ausführung des Vertrags erreichen kann, so kann man auch Konfiguration C2 erreichen.

Falls wir nun die Konfiguration CI kennen, in der die Ausführung des Smart Contracts startet, dann können wir mithilfe eines SMT-solvers herausfinden, ob eine gewisse Zielkonfiguration CR erreichbar ist oder nicht. Um genauer zu sein müssen nicht einmal eine konkrete Startkonfiguration und Endkonfiguration angeben, sondern können leicht Mengen solcher Konfigurationen definieren.

Somit können wir beispielsweise Fragen stellen wie: “Ist es möglich, dass ein Vertrag der am Anfang 2000 Ether besessen hat, am Ende der Ausführung weniger Geld besitzt”?

Der Ansatz den wir zeigen ist stark vereinfacht, insbesondere haben wir nicht gezeigt wie die abstrakte Semantik “abstrakter” gemacht wird als die ursprüngliche Semantik. Darüber werden wir ein wenig mehr im nächsten Beitrag erzählen.

Bis zum nächsten Mal!

Euer EtherTrust Team