Netidee Blog Bild
1 Jahr Netidee Förderung
Rückblick und Ausschau zum Jahresende (19.12.2023)
Förderjahr 2022 / Stipendien Call #17 / ProjektID: 6321 / Projekt: Automated Verification of Game-Theoretic Security Properties for Decentralized Protocols

Ich habe es mir zur Gewohnheit gemacht am Ende eines Jahres Bilanz zu ziehen und in Ruhe das vergangene Jahr noch einmal Revue passieren zu lassen um daraus meine Lehren für das Nächste zu ziehen. So möchte ich das auch für mein Förderjahr 2023 tun.

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.

Eröffnungszeremonie Computer- and Communication Security Konferenz
Eröffnungszeremonie der Computer and Communication Security Konferenz 2023.

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.

 

Tags:

CheckMate Rückblick Compositionality Spielsynthese Modellierung

Sophie Rain

Profile picture for user sophie.rain
I am a PhD student at TU Wien, who loves to solve riddles. The riddles I work on professionally concern the security verification of Blockchain applications. I do so by applying mathematical concepts such as game theory, logic and most importantly automated reasoning.

Skills:

Automated Reasoning
,
Game Theory
,
Blockchain Technology
,
Logic
CAPTCHA
Diese Frage dient der Überprüfung, ob Sie ein menschlicher Besucher sind und um automatisierten SPAM zu verhindern.

    Weitere Blogbeiträge

    Datenschutzinformation
    Der datenschutzrechtliche Verantwortliche (Internet Privatstiftung Austria - Internet Foundation Austria, Österreich) würde gerne mit folgenden Diensten Ihre personenbezogenen Daten verarbeiten. Zur Personalisierung können Technologien wie Cookies, LocalStorage usw. verwendet werden. Dies ist für die Nutzung der Website nicht notwendig, ermöglicht aber eine noch engere Interaktion mit Ihnen. Falls gewünscht, treffen Sie bitte eine Auswahl: