Hallo zusammen,

Nach dem kleinen Exkurs beim letzten Mal über unsere Reise zu ETAPS, wollen wir jetzt damit weiter machen ein wenig zu erklären, wie man die Sicherheitsprobleme von Smart Contracts allgemein und formal beschreiben kann, so dass man die Contracts später später automatisch auf diese Probleme hin testen kann.

Wie bereits im vorletzten Beitrag angedeutet, ist es unser Ziel formal (also mithilfe der Semantik, die wir entwickelt haben), zu beschreiben, was einen sicheren Smart Contract ausmacht. Leider kann man kein ganz allgemeines Konzept von Sicherheit beschreiben, aber zumindest einzelne Sicherheitseigenschaften, die bestimmte Arten von Attacken (wie zum Beispiel den DAO hack) ausschließen.

Um das aber zu tun, muss man sich erst einmal überlegen, was den eigentlich die Sicherheitseigenschaft ist, die denn beim DAO contract verletzt wurde. Ein erster Ansatz könnte sein zu sagen: ,Dem Vertrag wurde Geld gestohlen, also ist die Eigenschaft, die verletzt wurde, dass sicheren Contracts kein Geld gestohlen werden kann’. Aber was heißt es denn formal (und vor allem allgemein), dass einem Contract Geld gestohlen wurde? Im Fall vom DAO Contract lag es daran, dass ein Nutzer mehr Geld abheben konnte, als er eingezahlt hat, aber das ist ja prinzipiell nicht bei jedem Contract problematisch. Ganz im Gegenteil, viele normale Contracts (zum Beispiel eine Lotterie) hätte die ganz normale Funktionalität, dass sie einigen Nutzern (nämlich den Gewinnern) mehr Geld auszahlen, als diese einbezahlt haben.

Was könnte also stattdessen das wirkliche Problem gewesen sein? So wie wir es sehen, war das Problem eigentlich, dass ein Angreifer (nämlich der smart contract, der das Geld geklaut hat) beeinflussen konnte, wie viel Geld der DAO contract tatsächlich ausgezahlt hat. Also in Abhängigkeit von dem Code des Angreifers, waren die ausgehenden Geldflüsse des DAO Contracts unterschiedlich. Dies ist eine Eigenschaft, die eine (korrekt implementierte) Lotterie nicht hätte: Auch wenn der Gewinner mehr Geld kriegt als die anderen, sollte dies nicht von dem Code des Gewinners abhängen: hat er einmal gewonnen kriegt er immer das gleiche Geld, egal welchen Code er hat.

Formal beschreiben wir eine solche Eigenschaft jetzt als sogenannte Hypereigenschaft - eine Eigenschaft die mehrere Ausführungen eine Programms (oder in unserem Fall Contracts) in unterschiedlichen Szenarien vergleicht. Um diese Hypereigenschaft zu beschreiben, stellen wir uns vor, dass wir zwei verschiedene Welten haben: Diese Welten sind komplett gleich außer, dass der Account, der mit dem DAO contract interagiert unterschiedlichen Code hat, zum Beispiel: einmal den Code eines Angreifers (wie wir ihn beim letzten Mal beschrieben haben) und einmal gar keinen Code (weil der Account ein externer Account ist). Jetzt wollen wir, dass der DAO contract in beiden Welten (sofern er auf die gleiche Art aufgerufen wird) immer die gleichen Auszahlungen macht. Und hier sehen wir schon das Problem: Wenn der DAO mit dem Angreifer agiert, zahlt er sein gesamtes Geld aus, wenn er mit einem externen Account interagiert immer das gleiche.

Wir haben das einmal in einem Bild zusammengefasst:

In Welt 1 interagiert der DAO contract mit einem Angreifer (wobei die ausgehenden Pfeile die Auszahlungen sind und die eingehenden Pfeile die Aufrufe durch den Angreifer). In Welt 2 interagiert der DAO hingegen mit einem externen Account (ohne Code), entsprechend gibt es nur eine Auszahlung.

Wir sagen also, dass der DAO contract sicher wäre, wenn er (egal mit wem er interagiert) immer das gleiche auszahlt. In unserem Papier, haben wir diese Eigenschaft Call integrity genannt. Diese Eigenschaft ist jetzt nicht nur spezifisch für den DAO, sondern schließt ähnliche Attacken in beliebigen Contracts aus.

Wie man solche Eigenschaften nun automatisch testen kann, beschreiben wir beim nächsten Mal.

Bis dann!

Euer EtherTrust Team