Das Modellieren von Protokollen

In vorangehenden Blog Beiträgen habe ich oft erwähnt, dass es schwierig ist ein tatsächliches Blockchain Protokoll spieltheoretisch zu modellieren. Ich habe auch immer wieder von unseren Bemühungen zur automatischen Synthese von spieltheoretischen Modellen berichtet. Während dieses Projekt vielversprechende Fortschritte macht, ist es dennoch auf Protokolle beschränkt, die vollständig in der Programmiersprache Solidity definiert sind. In diesem Blog berichte ich vom Modellieren einer sogenannten Blockchain Brücke. Das ist ein Protokoll, das verschiedene Blockchains beziehungsweise Kryptowährungen miteinander verbindet. Als solches, kann es nicht innerhalb einer einzigen Blockchain definiert werden. Deshalb kann man unsere Synthese Bemühungen nicht darauf anwenden.

Was ist eine Blockchain Brücke?

Eine Blockchain Brücke ist ein Protokoll, das die Interoperabilität zwischen verschiedenen Blockchains ermöglicht. Sie dient dazu, Token (= Werteinheiten) und Daten sicher von einer Blockchain auf eine andere zu übertragen. Nachdem jede Blockchain normalerweise ihre eigene Architektur, Protokolle und Token hat, sind direkte Übertragungen zwischen verschiedenen Blockchains nicht möglich. Da kommt die Blockchain Brücke ins Spiel. Sie ermöglicht es Vermögenswerte und Informationen zwischen unterschiedlichen Blockchains auszutauschen, ohne dass diese direkt miteinander kompatibel sein müssen.

Vereinfach gesagt funktioniert eine Blockchain Brücke, indem ein Token auf der ursprünglichen Blockchain "eingefroren" wird, während ein äquivalenter Token auf der Ziel-Blockchain "erzeugt" wird. Naheliegenderweise, gibt es dabei einige spieltheoretische Aspekte zu beachten, wie zum Beispiel die beidseitige Liquidität der Brücke, aber auch tiefergreifende Überlegungen, wie zum Beispiel das sichere "Erschaffen" neuer Tokens ohne dabei drastischen Einfluss auf die Inflation der Währung zu nehmen. Da Blockchain Brücken weiters entscheidend für die Schaffung eines interoperablen Blockchain Ökosystems sind, ist die Sicherstellung ihrer spieltheoretischen Sicherheit essentiell.

Stand der Dinge und Einsichten

Um genügend fachliches Know-How und Detailwissen aufzubauen, haben wir uns zu Beginn sehr häufig mit unserer Partnerfirma getroffen. Nachdem die spieltheoretische Analyse nur so gut ist wie ihr Modell, haben wir uns dafür ausreichend Zeit genommen. Aufgrund einer Geheimhaltungsklausel darf ich vor der Veröffentlichung der Blockchain Brücke noch nicht von konkreten Modellierungsschritten, der genauen Brückenarchitektur oder Ergebnissen der Sicherheitsanalyse berichten. Danach wird unsere Case Study selbstverständlich frei zugänglich publiziert.

Die Brücke besteht aus unterschiedlichsten Komponenten und wir haben lange beratschlagt welche Art der Modellierung für diese Struktur am besten geeignet ist. Voraussichtlich werden wir dafür die momentane Funktionalität von CheckMate erweitern müssen. Wir sind allerdings zuversichtlich, dass diese Änderung kompatibel mit unserem bisherigen Herangehensweise ist.

Mittlerweile stecken wir mitten in der Modellierung, die zugegebenermaßen sehr viel aufwändiger ist als erwartet. Wir schätzen, dass CheckMate die Größe des Modells zwar schafft, sind uns aber bewusst, dass die Laufzeit durchaus sehr lange sein könnte. Obwohl das Modell zu diesem Zeitpunkt noch nicht fertig ist, haben wir durch unsere Analyse und Detailfragen bereits jetzt Unstimmigkeiten im Protokoll erkannt und mit unserem Partner beheben können. Wir hoffen auf weitere spannende Erkenntnisse im weiteren Verlauf des Modellierens und vorallem duch unsere spieltheoretische Sicherheitsanalyse mit CheckMate.