Netidee Blog Bild
CheckMate: Die Fusion mehrerer Disziplinen
Blockchain Technologie, Spieltheorie und Automated Reasoning (23.06.2023)
Förderjahr 2022 / Stipendien Call #17 / ProjektID: 6321 / Projekt: Automated Verification of Game-Theoretic Security Properties for Decentralized Protocols

Die Kombination mehrerer Forschungsbereiche in einem Projekt ist oft ein schwieriges, jedoch immer ein spannendes Unterfangen. Mit der ersten Version unseres automatisierten Tools CheckMate ist uns so eine Fusion gelungen.

In den letzten Monaten habe ich die verschiedenen Forschungsbereiche, die in meinem PhD Projekt relevant sind, vorgestellt. Nun setze ich die Bausteine zusammen und stelle einen großen Meilenstein meiner Arbeit vor: CheckMate. Um den Nutzen und die Funktionsweise von CheckMate zu verstehen, fangen wir nochmal von vorne an.

Blockchain ist eine Technologie die uns Konzepte wie Kryptowährungen ermöglicht. Auf der Basis solcher unfälschbaren Währungsdaten, die festhalten wer wie viel dieser Währung besitzt, können wie bei konventionellen Währungen auch Geschäfte wie z.B. Überweisungen gemacht werden. Detaillierte Erklärungen dazu gibt es in meinem Blog "Was, Wie, Wofür Blockchain?". Blockchain Technologie kann aber viel mehr als einfache Transaktionen zu bewerkstelligen: Man kann diverse Finanzprodukte wie Crowd Funding, Auktionen oder Glücksspiel umsetzen. Diese komplexeren Anwendungen basieren auf sogenannten Smart Contracts oder auch Protokollen.

Solche Protokolle sollten sicher sein. Das heißt ein Hacker*innenangriff sollte unmöglich sein. Um das sicherzustellen müssen beide Aspekte eines solchen Protokolls berücksichtigt werden: die Kryptographischen und die Spieltheoretischen. Nehmen wir als Beispiel ein Passwort beim Online Banking: Dass das Passwort beim Eingeben geheim bleibt, ist Kryptographie; dass man es nicht freiwillig jemandem weitergibt, ist Spieltheorie.

Nachdem es zur Analyse der kryptographischen Aspekte schon solide Forschungsergebnisse gibt, beschäftige ich mich mit den spieltheoretischen. Insbesondere möchte ich garantieren, dass sich einerseits niemand zu Unrecht bereichern kann und andererseits, dass ehrlichen Nutzer*innen kein Schaden entstehen kann. Diese beiden Eigenschaften habe ich im Blog "Das Spiel des Lebens" genauer erklärt.

In unserem Prototypen CheckMate haben wir diese Sicherheitseigenschaften zuerst in spieltheoretische Konzepte und in einem zweiten Schritt in logische Formeln übersetzt. Wie im Blog "Steht der Bauer im Zimmer,.." erörtert, kann man logische Formeln einem Automated Reasoner geben. Dieser kann einem sagen, ob es möglich ist, diese Formeln alle gleichzeitig zu erfüllen. Wenn man die Formeln auf eine gewisse Art bereitstellt, kann man aus dem Output des Automated Reasoners ableiten, ob die Sicherheitseigenschaften erfüllt sind oder nicht.

Unser Tool ist folgendermaßen aufgebaut.

Graphische Darstellung von CheckMate
Graphische Darstellung von CheckMate

Um die Darstellung besser zu veranschaulichen, nehmen Sie an, Sie besitzen z.B. Bitcoin und möchten an einer Auktion teilnehmen. Sie vertrauen der Anbieterin der Auktion nicht und möchten sich daher vergewissern, dass die Durchführung mit rechten Dingen zugeht. Dafür können Sie CheckMate verwenden.

Sie nehmen die Beschreibung der Auktion zur Hand (Protokoll) und wissen wie sie laut Anbieterin ablaufen sollte (ehrliches Verhalten). Dann modellieren Sie das Protokoll als Spiel und das ehrliche Verhalten als ehrliche Historie, was zugegebenermaßen nicht ganz einfach ist und Fachwissen bedarf. Das ist Schritt 1 in der obigen Darstellung. Den Rest übernimmt CheckMate. CheckMate übersetzt das Spiel mit der zugehörigen ehrlichen Historie in logische Formeln (Schritt 2) und gibt diese an einen Automated Reasoner weiter (Schritt 3). Der Automated Reasoner wiederum teilt CheckMate mit, ob die Formeln unerfüllbar (Schritt 4a) oder erfüllbar (Schritt 4b) sind. CheckMate kann daraus schließlich folgern, ob das ursprüngliche Protokoll sicher war oder nicht. Somit wissen Sie, ob Sie ruhigen Gewissens an der Auktion teilnehmen können.   

Wir haben CheckMate erfolgreich an bestehenden Protokollen getestet und unsere Ergebnisse bei einer Fachkonferenz eingereicht. Ein Link zur Publikation wird so bald wie möglich ergänzt. Unser Prototyp ist Open Source und kann unter https://github.com/apre-group/checkmate downgeloadet werden.

In der Zukunft haben wir vor an der Modellierung der Protokolle als Spiele zu feilen um den Zugang und die User*innenfreundlichkeit von CheckMate zu verbessern.

Tags:

software verification Security Spieltheorie Automated Reasoning Automation

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: