Hallo!

Heute wollen wir euch ein paar Ideen zeigen wie und warum die Semantik, die wir mithilfe von Horn clauses definieren, “abstrakter” ist als die konkret Ausführungssemantik für Smart Contracts.

Da die Details sehr technisch sind, wollen wir uns nicht mit ihnen befassen, sondern lieber die grundsätzliche Ideen diskutieren und ein Beispiel für eine konkrete Abstraktion geben, die wir umgehest haben.

Die generelle Idee hinter dem Erstellen einer abstrakten Semantik ist, dass die exakte Modellierung der Semantik den SMT-Solver, der diese Semantik schließlich als Eingabe bekommt, überfordern würde: Entweder würde der Lösungsvorgang sich sehr stark verlangsamen, oder das Problem so kompliziert werden, dass der SMT-Solver niemals eine Lösung finden kann. Manchmal kann es auch sein, dass man schon allein zum Modellieren der konkreten Semantik Funktionalitäten bräuchte, die der SMT-Solver überhaupt nicht unterstützt. Man muss also eine Darstellung der der Semantik finden, die weniger kompliziert (für den SMT-Solver) als die ursprüngliche Semantik ist, aber trotzdem noch alle möglichen Ausführungsschritte abdeckt (schließlich verfolgen wir das Ziel der Soundness, vgl. Roadmap). Gleichzeitig müssen wir aber auch darauf achten, dass die Semantik immer noch präzise genug ist: Eine einfache Abstraktion, die Soundness erfüllt, wäre beispielsweise zu sagen, dass man von jeder Programmkonfiguration jede andere Programmkonfiguration erreichen kann. Diese Abstraktion ist sound, da alle Möglichen Verhaltensweisen des echten Vertrages abgedeckt werden (schließlich ist potentiell jedes Verhalten möglich), aber trotzdem wäre eine solche Abstraktion nicht wirklich hilfreich, da wir niemals zeigen könnten, dass es Verhaltensweisen gibt, die ein Vertrag nicht zeigt. Wir könnten somit nie einen Vertrag sicher beweisen, da wir dies tun, indem wir zeigen, dass er NIE schädliches Verhalten zeigt. Eine grafische Illustration dieses Problems ist wie folgt gegeben: 

Unser Ziel ist, dass die Abstraktion, die wir wählen, sämtliches konkretes Verhalten enthält, aber dennoch sehr viel präziser ist als lediglich ein beliebiges Verhalten zu modellieren. 

Ein großes Problem bei der Analyse von Ethereum Bytecode ist, dass die Ausführung von Ethereum durch die Ressource ,Gas’ begrenzt ist. Das Problem dabei ist nicht die Begrenzung der Ausführungsschritte an sich, sondern das jede ausgeführte Operation einer unterschiedliche Menge an Gas beansprucht, die mitunter durch komplexe arithmetische Operationen berechnet werden muss. Wenn wir die Ausführung nun ganz genau modellieren, dann muss auch der SMT-Solver all diese komplizierten Berechnungen durchführen, was ihn in der Praxis überfordern würde. Gleichzeitig ist es aber so, dass wir im Allgemeinen ohnehin nicht genau wissen, wie viel Gas einem Smart Contract für seine Ausführung mitgegeben wird: Denn dies bestimmt die Person, die eine entsprechende Transaktion started, die den Smart Contract aufruft. Wenn wir nun allgemeine Eigenschaften eines Vertrages zeigen wollen, die unabhängig davon gelten, wer einen Vertrag wie genau aufruft, dann wissen wir in unserer Analyse ohnehin zu keinen Zeitpunkt, wie viel Gas noch zur Verfügung steht. Als Konsequenz, modellieren wir in unserer abstrakten Semantik Gas einfach überhaupt nicht. Damit wir trotzdem die Soundness Eigenschaft erfüllen, müssen wir sicherstellen, dass wir alle Verhaltensweisen des Vertrags modellieren, die bei jedem möglichen Gas-Wert auftreten können. Da der Haupteffekt von Gas ist, dass es dazu führen kann, dass wenn zu wenig Gas zur Ausführung zur Verfügung steht, die Ausführung des Vertrages vorzeitig fehlerhaft beendet wird. Wenn wir nun also Gas nicht spezifisch modellieren müssen wir es in unserer abstrakten Semantik erlauben, dass die Ausführung jederzeit (ohne, dass eine bestimmte Bedingung erfüllt sein muss) fehlerhaft beendet wird.

In unserer abstrakten Semantik finden sich noch viele weitere Abstraktionen. Wenn euch euch ihr euch genauer dafür interessiert, könnt ihr die Details in unseren Papieren (hier und hier) nachlesen!

Beim nächsten Mal werden wir uns damit befassen wie wir - passend zur abstrakten Semantik - auch abstrakte Sicherheitseigenschaften formulieren können.

Euer EtherTrust-Team