Hallo zusammen,

In unserem letzten Beitrag haben wir euch bereits davon berichtet, welchen Zweck unsere neue Spezifikationssprache HoRSt erfüllt. Heute wollen wir euch ein bisschen mehr dazu erzählen, wie genau unser neues Design in der Praxis aussieht (vor allem im Vergleich zu früher).

Vielleicht erinnert ihr euch noch an das Design unseres Prototyps, das wir euch in einem unserer älteren Blogposts gezeigt haben:

Im Gegensatz dazu hat sich unser Design nun wie folgt geändert:

Die generelle Idee ist, dass wir nun anstatt direkt aus einem Vertrag seine abstrakte Semantik zu generieren, einen Vertrag und eine HoRSt-Spezifikation der abstrakten Semantik von Smart Contracts im Allgemeinen als Input nehmen und daraus die Abstrakte Vertragssemantik eines konkreten Vertrages in einer Zwischenrepräsentation generieren.

Auf dieser Zwischenrepräsentation können dann zahlreiche Optimierungen durchgeführt werden (um die Semantik zu vereinfachen, falls dies möglich ist). Anschließend wird - wie zuvor - ein Output im smt-lib-Format generiert, mit dem nun der SMT-Solver aufgerufen werden kann. Ein bedeutender Unterschied zum vorherigen Design besteht darin, dass ein Großteil der skizzierten Infrastruktur nicht spezifisch für Ethereum Smart Contracts ist, sondern eine generalisierte Funktionalität bereitstellt. Alle grünen Teile des Schaubildes sind nicht Ethereum-spezifisch: HoRSt-Spezifikationen können für beliebige Horn lause-basierte Semantiken geschrieben werden, und sobald der Vertrag gemäß der HoRSt-Spezifikation in die Zwischenrepräsentation überführt wurde, sind alle Optimierungen und der Übersetzungsschritt in das smt-lib-Format ebenfalls generisch und wiederverwendbar. Lediglich die Verarbeitungsschritte, die die Smart Contract einlesen und eine Verbindung zur HoRSt-Spezifikation herstellen sind speziell auf Ethereum Smart Contracts zu geschnitten.

Dies hat den Vorteil, dass nun leicht Änderungen in der abstrakten Semantik vorgenommen werden können, ohne das die wesentliche Funktionalität des Tools (die Art und Weise, wie die Spezifikation für den SMT-Solver aufbereitet wird) angerührt werden muss. Dies vereinfacht es sehr viele unterschiedliche Versionen der abstrakten Semantik zu testen und ermöglicht es auch anderen Wissenschaftlern und Interessierten das Tool leicht zu modifizieren oder zu erweitern. Außerdem kann die Infrastruktur so leicht genutzt werden, um auch ganz andere Arten von Programmen zu analysieren ohne ein ganzes Tool von Grund auf neu zu schreiben. Lediglich die Sprach-spezifischen Teile (in blau) müssen neu programmiert werden - alle anderen Teile können wiederverwendet werden.

Hoffentlich seid ihr jetzt genauso begeistert von HoRSt wie wir!

Euer EtherTrust Team