Hallo zusammen,

Heute wollen wir euch erklären, wie wir die Sicherheitseigenschaft (Call Integrity), die wir euch hier vorgestellt haben, abstrahieren können, so dass wir sie Mithilfe von EtherTrust analysieren können.

Wenn wir mithilfe unseres Ansatzes zeigen wollen, dass ein Vertrag Call Integrity erfüllt, stoßen wir zunächst auf ein sehr substanzielles Problem: Aufgrund der Art und Weise wie wir die Ausführung mithilfe von Horn Clauses definieren, können wir nur Fragen der Form stellen: "Wenn wir in einer Konfiguration X gestartet sind, können wir dann eine Konfiguration Y erreichen?”. Insbesondere bedeutet dies, dass wir uns nur eine einzelne Ausführung unseres Vertrages anschauen können und nicht, wie es für Call Integrity nötig wäre (da dies eine Hypereigenschaft ist), mehrere Ausführungen des Vertrages miteinander vergleichen können.

Aus diesem Grund müssen wir uns überlegen, ob es eine Möglichkeit gibt, die Eigenschaft auf die gewünschte Weise zu formulieren. Exakt die gleiche Eigenschaft zu formulieren, ist nicht ohne weiteres möglich, aber da wir im Endeffekt an der Soundness-Eigenschaft interessiert sind, müssen wir das auch gar nicht. Es reicht, wenn wir eine Eigenschaft formulieren können, von der wir wissen, dass wenn sie wahr ist, uns auch garantiert, dass Call Integrity gilt!

Und dies ist exakt, was wir tun. Die Idee dabei ist wie folgt: Ein Vertrag kann nur dann ein unterschiedliches Verhalten in der Interaktion mit einem ehrlichen und einem Angreifer-Vertrag zeigen, wenn es möglich ist, dass der Vertrag zunächst einen externen Vertrag (den ehrlichen oder den Angreifer) aufruft und im Anschluss, falls der Vertrag “zurückgerufen” werden sollte es möglich ist, selbst noch weitere Verträge aufzurufen. Wenn der Vertrag hingegen sicherstellt, dass er nach einem “Rückruf” keine weiteren Aufrufe fremder Verträge mehr tätigt, ist er sicher. Bezogen auf den DAO-Hack, wäre es in diesem Fall einem Angreifer nicht möglich sicher immer weiter neues Geld vom DAO Vertrag überweisen, da der DAO Vertrag nach der ersten Überweisung beim Rückruf keine weiteren Überweisungen mehr tätigt. Eine Illustration dazu findet sich in folgendem Bild: 

Die Nummerierung zeigt die Reihenfolge der Aufrufe: Zunächst wird der DAO Vertrag aufgerufen (1), was später einen Aufruf des Angreifer Vertrags (2) zur Folge hat. In der folge dieses Aufrufst, ruft der Angreifer den DAO Vertrag zurück (3). An dieser Stell wird nun wieder der DAO Vertrag ausgeführt. Der DAO Vertrag ist ist sicher, falls er sicherstellt, dass zu diesem Zeitpunkt die CALL-Instruktion nicht mehr ausgeführt werden kann. 

Diese Formulierung der Sicherheitseigenschaft hat den Vorteil, dass sie nur eine einzige Ausführung eines Vertrages in Betracht zieht. Man könnte sie formulieren als:

“Wenn man in einer erlaubten Anfangskonfiguration startet den Vertrag auszuführen, ist es dann jemals möglich, dass der Vertrag zurück gerufen wird und dann einen weiteren Vertragsaufruf startet?”

Lautet die Antwort des SMT-Solvers NEIN, dann wissen wir, dass der Vertrag sicher ist und Call Integrity erfüllt.

Passende abstrakte Sicherheitseigenschaften zu finden, die komplizierte konkrete Eigenschaften garantieren, ist leider keine mechanische Aufgabe, sondern erfordert viel Forschungsaufwand. Deshalb wird es für uns in der Zukunft eine spannende Aufgabe bleiben, weitere interessante abstrakte Sicherheitseigenschaften für andere konkrete Eigenschaften zu formulieren.

Beim nächsten Mal werden wir euch über unsere ersten Versuche berichten, die theoretischen Ideen, die wir bisher erklärt haben, zum ersten Mal in die Praxis umzusetzen.

Bis zum nächsten Mal!

Euer EtherTrust-Team