Hallo allerseits,

Wie wir in unserem letzten Beitrag berichtet haben, sind beim Programmieren unseres Prototypen einige Probleme aufgetreten. Insbesondere war es ab einem bestimmten Punkt wirklich schwierig, eine gute Übersicht darüber zu haben, inwieweit unsere theoretisch definierte abstrakte Semantik wirklich sinngetreu durch das Tool implementiert wird. Dies widerspricht aber natürlich vollkommen unserem Ziel Sicherheitsgarantien zu gewährleisten: Denn was bringt uns auch der schönste Soundness-Beweis, wenn am Ende vllt etwas ganz anderes implementiert ist?

Aus diesem Grund haben wir uns dazu entschieden, EtherTrust neu zu implementieren - und diesmal auf eine allgemeinere Art und Weise. Weil es uns besonders wichtig ist, dass wir möglichst sicher sind, dass die implementierte abstrakte Semantik mit unserer Theorie übereinstimmt, ist das Kernstück unseres neuen Designs eine neue Spezifikationssprache: HoRSt! 

HoRSt steht für “Horn clause based Resolution for Static Analysis”, also für “auf Horn Clauses basierte Resolution (ein Widerlegungsverfahren) für statische Analyse”.

Die generelle Idee ist, dass HoRSt eine Sprache ist, in der man die abstrakte Semantik von Ethereum Smart contracts, genauso wie die abstrakten Sicherheitseigenschaften auf eine Art und Weise spezifizieren kann, die der mathematischen Darstellung sehr stark ähnelt. Auf diese Weise ist es einfach aus einer mathematischen Spezifikation eine HoRSt-Spezifikation und umgekehrt und es ist für den Menschen leicht zu überprüfen, ob zwei solche Spezifikationen übereinstimmen.

Die Idee unseres Tools ist es nun, dass wir die Übersetzung von HoRSt in ein Format, mit welchem der SMT-Solver arbeiten kann vollkommen automatisieren, so dass man für das Designen einer Statischen Analyse mithilfe von Horn Clauses und das Definieren von Sicherheitseigenschaften nur noch HoRSt-Code schreiben muss! Das hat auch den Vorteil, dass unser Tool sehr leicht modifizierter und von Dritten erweiterbar ist: Keiner muss dazu nun mehr tausende Zeilen von Java-Code anpassen, sondern nur noch eine HoRSt-Datei verändern.

Diese Idee ist natürlich schön und reizvoll, erfordert aber auch sehr viel Arbeit: Zunächst müssen wir uns schließlich überlegen, wie HoRSt sinnvoll aussehen kann und dann wie wir die allgemeinen Sprachkonstrukte von HoRSt verlässlich für den SMT-Solver übersetzen. Das ist natürlich sehr viel schwieriger, als es zuvor war, weil wir nicht nur eine spezielle Analyse implementieren müssen, sondern eine Infrastruktur für alle potentiellen Analysen, die man je mit HoRSt schreiben könnte! Und trotzdem müssen wir darauf achten, dass wir auf eine Art und Weise übersetzen, die effizient vom SMT-Solver verarbeitet werden kann - denn am Ende geht es uns ja auch um Performance! Im Idealfall, sollte dieser Übersetzungsschritt dem Entwickler sogar möglichst viel Arbeit abnehmen: Also auch wenn der Entwickler eine Formulierung wählt, die für den SMT-Solver nicht ideal ist, sollte der Übersetzer diese in eine bessere Formulierung übersetzen. Immer ist das natürlich nicht möglich, aber je mehr solcher Optimierungen wir unterstützen, desto bessre für den Theoretiker, der die Analyse entwickelt.

Euer EtherTrust Team