Die Ethereum Foundation (EF) ist eine Non-Profit Organisation, die sich für die Weiterentwicklung der Ethereum Blockchain einsetzt. Das beinhaltet die Entwicklung von Smart Contracts, die Kontrolle der Sicherheit, die Förderung von Forschung in relevanten Bereichen etc. Obwohl die Ethereum Foundation nicht die Betreiberin der Ethereum Blockchain ist, kann man ihre Rolle am ehesten mit der EZB (= Europäischen Zentral Bank) im traditionellen Finanzwesen vergleichen. Die Forscher*innen des Formal Verification Teams sind an der formalen Analyse und der formalen Verifikation von Protokollen der Ethereum Blockchain, auch Smart Contracts genannt, interessiert.

Wie im letzten Blog Post "Der Mehrwert von Konferenzen" erwähnt, ist die Idee der Kollaboration bereits bei einer Fachkonferenz im Sommer 2022 entstanden. Das Formal Verification Team hat damals begonnen sich für spieltheoretische Ansätze der Verifikation zu interessieren, während ich die ersten Ergebnisse zu CheckMate präsentiert habe. Wir haben dann die Kaffeepausen dazu genutzt uns auszutauschen. Nach ein paar Tagen der Reflexion haben wir beschlossen im Herbst 2023 ein gemeinsames Projekt zu starten.

Hier nochmal eine kurze Auffrischung zu CheckMate. CheckMate ist ein von meiner Gruppe und mir entwickeltes Tool, das sicherstellt ob ein Protokoll - modelliert als Spiel - gegen gewinnbringende Angriffe immun ist oder nicht. Diese Art von Analyse ist unter anderem relevant für die Finanzprodukte der Ethereum Blockchain. Diese heißen Smart Contracts. Zur Zeit hat die Anwendung von CheckMate noch einen Haken: Anwender*innen müssen zuerst das Protokoll als Spiel modellieren bevor sie CheckMate verwenden können. So eine Modellierung ist komplex, aufwändig und benötigt Detailwissen (siehe auch CheckMate).

Die EF hat bei der formalen Analyse ihrer Finanzprodukte (Smart Contracts) gewissermaßen am anderen Ende gestartet. Ein Smart Contract der z.B. eine Auktion ermöglicht, wird meist in der Programmiersprache Solidity geschrieben. Ein Smart Contract is also quasi ein Programm, das - wenn es aufgerufen wird - das beschriebene Finanzprodukt durchführt. So wie jedes Programm kann auch ein Smart Contract Fehler haben. Dazu kommt, dass in Solidity viele interne Abhängigkeiten nicht erkennbar sind. Um Fehler in (in Solidity geschriebenen) Smart Contracts zu verhindern, hat das Formal Verification Team ein "Übersetzungstool"  namens ACT entwickelt, das die logischen Verknüpfungen im zugrundeliegenden Smart Contract klar und nachvollziehbar darstellt. Das heißt als Entwickler*in eines solchen Smart Contracts kann man sich die "übersetzte" Beschreibung anschauen und kontrollieren ob sich der Smart Contract so verhält, wie man das möchte.

In dem gemeinsamen Forschungsprojekt versuchen wir nun, wie in der obenstehenden Grafik dargestellt, das Übersetzungstool ACT mit CheckMate zu verbinden. Genauer gesagt, möchten wir aus der Beschreibung von ACT den Input für CheckMate, also das Spiel, generieren. So ein Vorgehen nennt man auch Synthese, weil wir ja sozusagen ein Spiel "künstlich" herstellen. Um ein Spiel zu synthetisieren, muss unter anderem bestimmt werden welches Verhalten nach welchem vorhergehenden Verhalten möglich ist und ob die Anwender*in darauf Einfluss nehmen kann. Im Beispiel von einer Auktion, sollte man das angebotene Gut nur bekommen können, wenn man davor ein Gebot abgegeben hat und - je nach Auktionstyp - auch den höchsten Wert geboten hat. Das ist also etwas das eine Teilnehmer*in beeinflussen kann. Wie lang die Auktion Gebote entgegennimmt hingegen, sollte nicht von Bieter*innen beeinflusst werden können.

Bis jetzt haben wir bereits vielversprechende Fortschritte in dieser Frage gemacht. Weitere Forschungsfragen die wir uns zur Zeit stellen sind:

• Wodurch (durch welche Parameter) wird der Gewinn/Verlust der Teilnehmer*innen bestimmt?   
  • z.B. erhaltenes Gut minus bezahlter Preis
• Welche Kategorien von Spieler*innen gibt es?    
  • z.B. Verkäufer*in, Käufer*in
• Wie viele Spieler*innen sollten wir pro Kategorie betrachten?     
  • z.B. 3 Bieter*innen, 2 Auktionsleiter*innen etc
• Welche Spieler*in ist wann "dran"?     
  • z.B. welche Bieter*in darf in welcher Reihenfolge ein Abgebot abgeben
• Wann endet das Spiel?   
  • z.B. wenn alle Bieter*innen 2 mal die Chance hatten zu bieten

Zusätzlich müssen wir uns bei jedem dieser Punkte zusätzlich überlegen ob sich das automatisch Erkennen lässt oder ob das Tool Unterstützung der User*in benötigt.

Ich denke man kann gut erkennen, dass sich die Synthese von Spielen zur Zeit noch mitten in der Entstehung befindet. Allerdings ist bereits jetzt abzusehen, dass eine erfolgreiche Umsetzung einen starken positiven Einfluss auf die Anwendbarkeit meiner Forschung haben kann. Ich hoffe die Zusammenarbeit mit EF bleibt weiterhin so spannend, motivierend und ergebnisreich wie bisher!