Hallo zusammen,

Heute geht es weiter mit Details zu unserem EtherTrust Projekt. Eine Frage, die wir heute diskutieren wollen, ist wie wir sicher stellen können, dass unsere ganzen Modelle überhaupt realistisch sind - denn nur dann können wir ja überhaupt wirklich belastbare Garantien bekommen.

Generell ist es natürlich schwierig komplette Ende-zu-Ende-Garantien zu geben. Immer wenn Dinge mathematisch modelliert werden oder Code geschrieben wird, können dabei Fehler auftreten. Es kann passieren, dass die Semantik nicht genau das widerspiegelt was die unterschiedlichen Nutzer im Ethereum Netzwerk tatsächlich ausführen, wenn wir das Analyse-Tool schreiben, können dabei Programmier-Fehler auftreten (selbst wenn die Theorie, die wir implementieren korrekt bewiesen ist) und es könnte sogar sein, dass der SMT-solver (das Lösungsprogramm für logische Formeln, das wir verwenden) fehlerhaft ist.

Trotzdem sollte man natürlich versuchen diese Probleme so gut es geht einzudämmen. Einen Schritt, den wir in diese Richtung unternehmen ist, dass wir unsere Semantik in einem Beweis-Assistenten formalisiert haben. Ein Beweisassistent ist ein Programm, dass es erlaubt mathematische Formalisierungen auf eine computer-lesbare Weise zu enkodieren. Wenn man dann Beweise über diese Formalisierungen führt, überprüft das Programm automatisch, ob die einzelnen Beweisschritte korrekt sind. Allein die Semantik zu Formalisieren gibt uns natürlich noch keinen Aufschluss darüber, ob die Semantik auch korrekt ist. Um das sicherzustellen, testen wir unsere Semantik. Der Beweisassistent, den wir benutzen, heißt F* und hat die praktische Funktion, dass man Formalisierungen, die man mit seiner Hilfe geschrieben hat, auch in eine ausführbare Programmiersprache exportieren kann. Das heißt, wir können Smart Contracts gemäß unserer Semantik ausführen! Entsprechend können wir unsere Semantik auch testen und zwar mit den gleichen Tests, die auch Ethereum verwendet um seine eigene Implementierung zu testen. Das gibt uns natürlich immer noch keine 100%ige Sicherheit, aber zumindest wissen wir, dass sich unsere Semantik auf allen Testfällen so verhält, wie es für die einzelnen Nutzer im Ethereum Netzwerk auch der Fall wäre. Wenn ihr euch anschauen wollt, wie diese Tests, die von Ethereum bereit gestellt werden aussehen, könnt ihr sie hier finden.

Außerdem erlaubt uns dies Tatsache, dass wir die Semantik in einem Beweisassistenten formalisiert haben in Zukunft auch noch einen Schritt weiter zu gehen: Wenn wir nämlich auch unsere abstrakte Semantik in F* formalisieren, können wir das Verhältnis zwischen den beiden Semantiken (die Soundness), die so wichtig für die formalen Garantien ist, in F* selbst beweisen! Das würde sicherstellen, dass die Soundness-Eigenschaft (siehe Roadmap) auf jeden Fall hält und wir beim Führen des Beweises auf Papier keinen Fehler gemacht habe. Aber das ist bisher leider noch Zukunftsmusik - wir planen aber fest, das nach dem Ablauf des EtherTrust Projektes in Angriff zu nehmen.

Falls jemand von euch jetzt neugierig ist, wie so ein Beweis-Assistent den aussieht, dann probiert es doch aus! Ein Online-Tutorial zu F* findet ihr hier.

Und wenn ihr euch dann auch mal unsere F*-Implementierung der Smart Contract Semantik ansehen wollt, findet ihr sie hier.

Bis zum nächsten Mal!

Euer EtherTrust Team