Entwicklung CheckMate 1.0

Das Förderjahr habe ich begonnen, indem ich mit meinen Kollegen die erste Version von CheckMate, unserem Tool zur automatischen Analyse von spieltheoretischer Sicherheit, entwickelte. Wir hatten dabei einige Hürden zu überwinden. Besonders markant war als wir bemerkt haben, dass unsere initiale Umsetzung einen wesentlichen Aspekt ignorierte (die Notwendigkeit von Fallunterscheidungen in der formalen Analyse der Formeln) und dadurch inkorrekten Output produzierte. Nach der Korrektur, haben wir uns daran gemacht zu beweisen, dass unser adaptierter Algorithmus nun mathematisch fehlerfrei ist.

Anschließend haben wir unsere Ergebnisse schriftlich festgehalten und bei einer kompetetiven Fachkonferenz eingereicht, die auf computerunterstützte Verifizierung fokussiert ist. Leider war das nicht ganz die richtige Zielgruppe, denn unsere Arbeit wurde trotz guten und konstruktiven Reviews nicht angenommen. Daraufhin haben wir es bei einer anderen Top Konferenz versucht, dessen Schwerpunkt auf Computer- und Kommunikationssicherheit liegt. Bei dieser wurden wir schließlich mit sehr positiven Rückmeldungen angenommen. Später im Jahr (November) habe ich unsere Publikation dann auf dieser Konferenz in Kopenhagen vorstellen dürfen.

Skalierung und Laufzeitverbesserung

Parallel zu unseren Publizierungsarbeiten, haben wir im Frühling begonnen uns der Laufzeit von CheckMate anzunehmen. Obwohl CheckMate gut für kleinere Protokolle funktioniert, stoßen wir bei komplizierteren Eigenschaften der Protokolle schnell an die Kapazitätsgrenzen unseres Tools. Deshalb haben wir an der Compositionality ("Zerlegbarkeit") von Spielen geforscht. Wir hoffen mit solchen Methoden das Spielmodell der Protokolle in mehrere Teile zerlegen zu können, dann diese Teile zu analysieren und schließlich Erkenntnisse über das gesamte Spiel zu erhalten.

Mittlerweile haben wir erste theoretische Ergebnisse und arbeiten daran diese in CheckMate anzuwenden. Im nächsten Jahr hoffen wir bereits die neue Version von CheckMate publizieren zu können.

Spieltheoretische Modellierung

Nachdem ein Tool nur wertvoll ist, wenn es den passenden Input gibt - in unserem Fall spieltheoretische Modelle von Protokollen - habe ich zusammen mit einer Kollegin im Sommer ein weiteres Projekt gestartet: Die Modellierung einer Cross-Chain Bridge, also ein Protokoll das einen direkten "Währungswechsel" von einer Kryptowährung zur anderen ermöglicht. Das Projekt hat sich als äußerst herausfordernd herausgestellt. Wir haben lange gebraucht um die Details des Protokolls auf dem Level zu verstehen der notwendig ist um es spieltheoretisch zu modellieren.

Zur Zeit ist das Projekt pausiert, weil meine Kollegin im Mutterschutz ist. Wir sind allerdings sehr zufrieden mit unserem Fortschritt dieses Jahr und freuen uns darauf nächstes Jahr mit frischer Energie daran weiterzuarbeiten und bestenfalls ebenso zu publizieren.

Synthese von Spielmodellen

Last but not least war da natürlich noch die Zusammenarbeit mit der Ethereum Foundation, die uns hoffentlich ermöglicht in Zukunft Protokolle, die ausschließlich auf der Ethereum Blockchain laufen, automatisch als Spiel zu modellieren. Nachdem das vorher erwähnte Modellierungsprojekt unterschiedliche Blockchains verbindet, wird es dadurch glücklicherweise nicht obsolet.

Auch bei diesem Projekt hoffen wir auf eine Publikation gegen Ende 2024 oder Anfang 2025.

Ingesamt sieht man, dass dieses Jahr von dem Start einiger neuer Projekte geprägt war. Für mich ist der Beginn neuer Themen immer besonders herausfordernd und belastend, dadurch war 2023 wirklich ein schwieriges, anstrengendes und arbeitsreiches Jahr. Umso mehr freut es mich, dass sich alle (erwähnten) Projekte sehr gut entwickeln. Ich freue mich nun die begonnene Arbeit weiterzuverfolgen und im nächsten Jahr hoffentlich zu dem einen oder anderen erfolgreichen Abschluss (= Publikation) zu führen. Wenn alles gut läuft, kann ich nächstes Jahr um die Zeit vielleicht bereits über das Schreiben meiner Dissertation berichten.