Hallo zusammen

Nach dem wir uns das letzte Mal damit beschäftigt haben, wie man Sicherheitseigenschaften allgemein ausdrücken kann, stellt sich jetzt natürlich die Frage, wie man solche Eigenschaften automatisch überprüft.

Um nicht gleich mit der Tür ins Haus zufallen, wollen wir heute deshalb erst einmal einen allgemeinen Überblick über die unterschiedlichen Schritte in unserem Projekt geben und wie diese zusammenhängen.Dazu haben wir mal ein kleines Übersichtsbild vorbereitet:

Auf der linken Seite sind die Arbeitsschritte zu sehen, die wir euch bereits beschrieben haben und die in unserem wissenschaftlichen Papier zusammengefasst sind. Das sind zum Einen das Erstellen eine formalen Semantik und zum anderen das Formulieren von formalen Sicherheitseigenschaften basierend auf der Semantik.

Die nächsten Schritte bestehen jetzt daraus, die Semantik und die Sicherheitseigenschaften zu abstrahieren. Was genau bedeutet das?

Die Semantik beschreibt, wie genau ein Smart Contract ausgeführt wird. Dazu benötigt man aber alle Informationen über den aktuellen Zustand der Welt (also den Globalzustand und die Blockchain). In der Realität ist es aber nun so, dass man zu dem Zeitpunkt an dem man seine Vertrag schreibt oder einen anderen Vertrag aufruft gar nicht weiß, wie die Welt zu diesem Zeitpunkt genau aussieht. Im Falle von Kryptowährungen ist das besonders stark ausgeprägt: Man weiß zum Beispiel nicht wann und in welchem Block eine Transaktion zur Blockchain hinzugefügt wird, und was zu vor passiert ist und die Welt so zum Beispiel geändert hat. Im Fall von Smart Contracts will man beispielsweise auch, dass sie immer sicher sind, egal wer sie gerade aufruft (denn das kann man ja nicht kontrollieren). Und genau diese Unsicherheiten sind der Grund, weshalb wir abstrahieren müssen: Wir müssen nämlich sicherstellen, dass in allen möglichen Ausführungen (also egal, wie der Globalzustand oder die Blockchain aussieht), gewisse schlechte Dinge garantiert NIE passieren.

Unser Mittel um das zu modellieren nennt man Abstract Interpretation: Wie beschreiben eine abstrakte Semantik, die viele konkrete Ausführungen gleichzeitig beschreibt. Wir zeigen dann, dass wenn bestimmte Sachen während der abstrakten Ausführung nicht passieren können auch in all den konkreten Ausführungen, die von der abstrakten Ausführung repräsentiert werden, nicht passieren können. Diese Beziehung zwischen der konkreten und abstrakten Semantik nennen wir Soundness und diese Beziehung müssen wir beweisen um am Ende wirkliche Garantien zu bekommen, wir führen einen ,Soundness Beweis’.

Den Vorteil, den die abstrakte Semantik hat, ist dass wir sie Mithilfe von logischen Formeln (so genannten Horn Clauses) aufschreiben können, für die es schon existierende Lösungsprogramme gibt (so genannte SMT-Solver). Diese Solver können heraus dann herausfinden, ob bestimmte Zustände während der abstrakten Ausführung auftreten können oder nicht.

Um nun, auf Eigenschaften testen zu können, müssen wir zwei Dinge beachten

1. Wir müssen die Eigenschaften in Bezug auf die abstrakte Semantik formulieren und zeigen, dass sie der Formulierung für die konkreten Semantik entspricht (oder allgemeiner ist)
2. Wir müssen eine Sicherheitseigenschaft immer in der folgenden Form formulieren: ,Es soll niemals passieren, dass folgender Zustand während der Ausführung auftritt:’. Leider ist das nicht immer so einfach möglich. Denkt zum Beispiel an die Call integrity Eigenschaft vom letzen Beitrag! Die lässt sich nicht so formulieren, da sie viel komplizierter ist! Die Möglichkeit dieses Problem zu lösen ist eine andere, allgemeinere Eigenschaft zu finden, von der wir wissen, dass wenn diese gilt, dass dann auch sicher Call integrity gilt.

Zusammenfassen müssen wir also auch abstrakte Eigenschaften formulieren und beweisen, dass wenn diese für die abstrakte Ausführung gelten, sie dann auch für alle dazugehörigen konkreten Ausführungen gelten.

Wenn wir das getan haben und dann unseren SMT solver für einen konkreten Smart Contract (geschrieben in EVM Bytecode) fragen, ob eine dieser Eigenschaften gilt und er uns eine positive Antwort liefert, wissen wir sicher, dass der Vertrag diese positive Eigenschaft hat. Wenn der SMT-solver eine negative Antwort liefert, können wir hingegen nicht sicher sein, dass der Contract die Eigenschaft wirklich verletzt, vielleicht war unsere Abstraktion einfach zu verallgemeinernd. In diesem Fall wissen wir aber zumindest, dass wir uns den Contract noch einmal ganz genau angucken müssen um sicher zu gehen, dass er kein Sicherheitsproblem hat.

So, ich hoffe, dass ihr jetzt eine grobe Idee habt, was noch vor uns liegt.

Mehr gibt’s beim nächsten Mal!

Euer EtherTrust Team