Das ist eine Übersetzung der folgenden Zusammenfassung:
Philipp Kant is der Direktor für Formale Methoden bei IOHK. Du kannst weitere Informationen über Ihn und seinen Erfahrungen hier finden.
- Seine Gruppe fokussiert sich auf die Einführung Formaler Methoden in Software Entwicklung Methode.
- Die Aufgabe seiner Gruppe ist es sicherzustellen, dass die Ergebnisse von den Wissenschaftlern, die die White Paper geschrieben haben und die die die Aspekte des Protokolls wissenschaftlich bewiesen haben, in eine maschinen-lesbare Sprache zu übersetzen und damit die Software zum laufen zu bringen.
- IOHK ist durch das einsetzen Formaler Methoden in die Blockchain Technologie einzigartig in der Branche.
- Die Formale Methodik wird eigentlich in Branchen wie der Raumfahrt oder Medizin eingesetzt. Also in Systemen wo sehr viel Geld oder das Leben der Menschheit auf dem Spiel steht.
- Die Blockchain ist ein System mit viel Geld und hat einen hohen Wert, deswegen wird diese Methodik hierfür angewandt.
In diesem Video startet Dr. Kant mit einer Einführung in Cardano und dem Proof-of-Stake Protokoll und kommt dann zu einer Präsentation zu Formalen Methoden. Das hier ist nur eine Zusammenfassung, dadurch sind einige Teile schwer zu verstehen. Diese können durch das anschauen des Videos mit den dazugehörigen Folien (Code und Grafiken) besser verstanden werden
Worüber geht es in PoS?
- Was möchtest du mit einer Kryptowährung erreichen?
- Dezentralisierung: Eine Währung ohne einer Zentralen Autorität und in den Händen seiner Nutzer.
- Erlaubnislos: Jeder sollte beitreten können, keine Eintritts-Voraussetzungen
- Ein stabiler Ledger
- Permanent: Eine Transaktion die in den Ledger eingetragen wurde soll dort bleiben und nicht löschbar sein.
- Lebendig: Übertragene Transaktionen sollten auch im Ledger eingetragen werden nach einer Zeit.
- alle diese Voraussetzungen zu selber Zeit zu erfüllen ist schwierig. Man benötigt etwas das sehr stabil ist, sodass jeder dem vertrauen kann, aber man möchte keine zentrale Autorität die etwas entscheiden muss und dadurch die Quelle des Vertrauens wird.
Wie Vertrauen im Bitcoin Netzwerk entsteht
- die Nutzer von Bitcoin senden eine Transaktion an das Netzwerk
- diese Transaktionen sind mit dem privaten Schlüssel signiert, so kann keiner fremdes Geld benutzen.
- die Personen möchten dass diese Transaktion ausgeführt wird und später nicht wieder verschwinden kann.
- gesendete Überweisungen werden in Blöcke gebündelt - wie die Seite eines Buches
- diese werden dann in eine bestimme Reihenfolge gesetzt - jeder Block verweist auf den vorherigen Block indem er der Hashwert von diesem in sich speichert.
- das in eine Reihenfolge setzen ist wichtig, weil wenn jemand versucht sein Geld zweimal zu überweisen, muss eine Transaktion als gültig ausgesucht werden.
- Vertrauen wird erzeugt indem jeder sich beteiligt, anstatt nur einer Person zu vertrauen.
- sollten einige nicht nach den Regeln spielen, so gibt es trotzdem ein stabiles und gültiges Ledger durch alle anderen Teilnehmer wo die Transaktionen geschrieben werden.
- Um sich davor zu schützen, dass Transaktionen gelöscht werden, gibt es die Longest-Chain Rule, weil zum Löschen auf kürzere und ältere Ketten zurückgegriffen werden müsste.
- Dadurch das man keine Erlaubnis benötigt, könnte sich ein Nutzer mehrmals registrieren und das ist ein Problem für das System
- Das wird eine Sybil-Attack genannt (Zwillings-Attacke)
- die Lösung von Bitcoin ist dass eine Registrierungsgebühr verlangt wird.
- die Gebühr ist, dass man ein willkürliches mathematisches Puzzle lösen muss
- Bitcoin fügt also einen willkürlichen Wert an Daten an jeden Block und der Hashwert eines jeden Blocks muss eine bestimmte Nummer an führenden Nullen haben.
- da ein Hashwert unumkehrbar ist, kann man den Block daraus nicht berechnen. Man muss es immer wieder neu berechnen und neu versuchen.
- man muss also Hash/Computer Leistung zu Verfügung stellen um einige Dateien auszuprobieren und den Hashwert von dem Block zu errechnen. Wenn dieser nicht passt muss man es erneut ausprobieren.
- durch diese Gebühr wäre eine Attacke auf das System sehr teuer, man müsste also mehr Computer und Rechenleistung als jeder andere im System besitzen.
Wie PoW funktioniert
- Es gibt eine zufällige Führungsauswahl, wo für jeden CPU den man dem System beisteuert, man eine Stimme bekommt.
- die Chance gewählt zu werden ist proportional zu dem wieviel Rechenleistung man dem System zu Verfügung stellt.
- der Gewinner bekommt die Möglichkeit einen Block zu schreiben und das wird dann auch belohnt.
- wegen der “longest-chain wins” Regeln is es sehr schwierig alte Blöcke zu verändern (außer man hat es irgendwie geschafft mehr als 50% der Rechenleistung vom System zu besitzen)
- Probleme von Bitcoin:
- Hashing Power verbraucht sehr viel Strom
- Der Verbrauch des Bitcoin Netzwerks ist vergleichbar mit dem gesamten Verbrauch eines kleinen Staates.
- und das alles für eine doch kleine Transaktionsrate (ca. 10 tx/sekunde)
- es ist schwierig das System zu skalieren in etwas mit mehr Geschwindigkeit
- Format des Rennens → der Gewinner bekommt alles
- um die Chance zu maximieren eine Belohnung zu bekommen arbeiten mehrere Leute in Form eines Pools zusammen und das führt zu einer Zentralisierung
Proof of Stake
- Andere Führungsauswahl: gewichtet nach dem Stake
- für jeden Zeit Slot, wählt das Protokoll zufällig einen Coin aus und der Besitzer dieses Coins darf den nächsten Block produzieren.
- um eine höhere Chance zu bekommen ausgewählt zu werden, muss man mehr Coins kaufen und das wird sehr sehr teuer
- das hat auch den Vorteil, dass es so an das System selbst gekoppelt ist
- wenn man ein großter Stake-Besitzer ist, man sehr viel von der Währung besitzt hat man eine hohe Chance Blöcke zu schreiben und auch Transaktionen zu löschen, aber das würde man nicht machen da wenn das bemerkt wird von den Menschen die Währungen weniger wert wird. (Vermögensverlust!) So bist du angehalten ehrlich zu bleiben, wodurch Vertrauen erzeugt wird.
- der Grund warum es bisher noch nicht verwendet wurde, ist dann man Zufälligkeit braucht für den Wahlprozess
- man benötigt also einen expliziten Zufallsgenerator → Es müssen sich alle auf eine Quelle des Zufalls einigen, wenn man nun aber eine Zentrale Autorität für den Zufall hat, kontrolliert diese einen großen Teil des Systems
- ein anderer Grund ist, dass viele dachten, dass dieses System nicht sicher ist weil jemand versuchen könnte die zufälligen Nummern zu erraten.
- es funktioniert ja nach dem Sinn, dass alle Coins in dem System in eine Reihe gestellt werden und eine bestimmte Zahl abgezählt wird, wer dann den Coin hat der bei der Zahl ist wird für den Block ausgewählt.
- wenn man dieses System voraussagen kann könnte jemand sein Geld quer durch das System senden um seinen Coin an dieser Stelle zu haben.
- was wir also benötigen ist ein dezentralen Zufallsgenerator, welcher nicht vorhergesagt werden kann
Ouroboros
- ein Ergebnis der Forscher von IOHK ist das Ouroboros Protokoll, welches das erste sichere PoS Protokoll ist
- diese Forschung wurde für eine Begutachtung von anderen freigegeben und bestätigt
- wie es funktioniert: Zeit wird in Slots geteilt und jeder Slot hat einen Block → für jeden Slot wird ein Stakeholder zufällig ausgewählt der Leader zu sein.
- dafür benötigt man den Zufall
- dafür wird eine Anzahl an Slots zu einer Epoche zusammengefasst. Am Anfang jeder Epoche wird ein bestimmter Code für den Zufallsgenerator von allen Stakeholdern ausgewählt
- grundsätzlich würfelt jeder Stakeholder eine Zahl (das erzeugt den Zufall, da diese Zahl nie den anderen gezeigt wird) und am Ende wird an das Netzwerk ein Beweis geschickt, dass jeder weis was er gewürfelt hat und nicht mehr verändert werden kann.
- Wenn nun der Stake für die nächste Epoche geklärt ist, werden alle Nummern gezeigt und in einer bestimmten Weise kombiniert → nun hat man den Code für den Zufallsgenerator
- dieser Code ist etwas worauf jeder Einfluss nehmen kann aber von keine genau vorhergesagt werden kann, da dieser aus der Vielzahl an geteilten Zahlen besteht
- Dieses System ist sicher gegen jede Beeinflussung, solange nicht einer mehr als 50% des Gesamten Stakes auf sich vereint.
Ouroboros Praos
- bei Vergrößerung des Protokolls kam die Frage auf “Was passiert wenn Nachrichten zeitversetzt sind?”
- da für das PoS Protokoll Zeit wichtig ist (jeder timeslot hat einen Block) und das System nur funktioniert, wenn die Information des letzten Block durch das gesamte Netzwerk verteilt ist bevor der nächste Slotleader an der Reihe ist. Ansonsten würde sich die Blockchain aufteilen, ganz automatisch.
- Praos ergänzt das System, dass eine Zeitverzögerung eingerechnet ist.
Von dem Papier zur Implementierung
- die Übersetzung von den Forschungspapieren aus dem Englischen in eine Sprache die von Maschinen verarbeitet werden kann.
- Es gibt eine Lücke zwischen den beiden Sprachen, da die Englische Sprache dafür da ist von Menschen verstanden zu werden, aber dort fehlen wichtige Details damit eine Maschine das verarbeiten kann
- Publizierung = Hohes Level an Abstraktionen, geschrieben in Englisch und mit mathematischen Formeln.
- vs. Code = kämpft mit den vielen Details und der Prezision für die Sprache Haskell, wenn du Code hast kann man dann einfach die Beweise für die Implementierung übernehmen?
kleine Schritte, keine großen Sprünge
- kleine Schritte machen es einfacher, sicherzustellen dass jeder Schritt auch richtig war
- der erste Schritt ist es den Algorithmus ins eine formale Sprache zu übersetzen (Ohne Details hinzuzufügen aber genauso abstrakt zu bleiben wir das whitepaper) aber etwas zu bekommen was von Maschinen gelesen und interpretiert werden kann.
- wenn man dann diese präzise aber abstraktes Stück hat, kann man beginnen es zu verfeinern und details hinzuzufügen.
- die Schritte sollten hier nun klein genug sein dass man jeden einzeln prüfen und testen kann um das Protokoll nicht in die falsche Richtung zu verändern
- Am Ende des Weges wird jeder Schritt simuliert und getestet worden sein
Prozesskalkulation
- der erste Schritt ist die Übersetzung in die Formale Sprache
- und welche Sprache sollte das sein?
- in einer Blockchain hat man sehr viel Computerkommunikation und es werden sehr viele Berechnungen des Ledger verteilt ausgeführt
- in der Informatik ist die Prozesskalkulation eine vielfältige Familie von verwandten Ansätzen zur formalen Modellierung gleichzeitiger Systemen
- unsere gewählte Prozesskalkulation heißt Psi-Berechnung (eine parametrische Familie von Prozessrechnungen)
Eingebettete domänenspezifische Sprache (EDSLs)
- wir wollen diesen Prozess in Haskell implementieren
- du kannst grundsätzlich in jeder Sprache schreiben, aber es ist einfacher zu verstehen wenn die Sprache in diese domäne passt
- Beispiele dafür: PostScript beschreibt Seiten an Text oder Grafiken, SQL beschreiben Datenbanken
- für eine eingebettete DSL → erschaffe diese Sprache in einer anderen Sprache, dadurch können Strukturen und der Syntax von der Sprache genutzt werden, aber die Hauptsprache verwendet es als Datensatz
- eine eingebettete DSL erlaubt verschiedene Interpretationen eines Wertes
Einbettung von Psi in Haskell
- Implementierung von Psi Kalkulation als ESDL in Haskell, danach wird Ourobos Praos in dieser Sprache geschrieben.
- danach kann durch verschiedene Interpretationen folgendes gemacht werden:
- Simulatoren erschaffen für das Programm
- oder Exporte zu einem Syntax eines Beweissystems (wie Isabelle oder Coq)
- oder das besitzen einer Interpretierer, welcher das gesamte Ding ausführen kann und zusätzliche Details hinzufügen kann und der ausführenden Code sein wird.
Modellierungsleistung (und Versagen)
- wir benötigen in dem PoS Protokoll eine gute Geschwindigkeit des Systems
- bevor etwas veröffentlicht wird, werden benchmarks ausgeführt
- das betrieben von Nodes auf verschiedenen Kontinenten und den Druck auf diese gezielt erhöhen, indem viele Transaktionen an diese gesendet werden um herauszufinden welche Parameter verbessert können damit der Durchsatz erhöht wird
- IOHK möchte nicht nur wissen wie gut der Code in der Theorie läuft sondern auch durch experimentieren
- mit experimentieren bekommst du Benchmark-Daten, aber man muss auch besser verstehen warum das so ist und was das Optimum ist
- danach kann man für Protokollfragen folgendes antworten:
- Wie lange dauert es bis eine Transaktion aufgenommen wurde?
- Wie lange dauert es dem Netzwerk beizutreten?
- Können Blocke durch das gesamte Netzwerk während eines einzelnen Slots verteilt werden?
- Was sind die technisches Voraussetzungen für eine Node?
Beeinträchtigung der Qualität: ΔQ
- Zeit gegen die Wahrscheinlichkeit, dass zu einer bestimmten zeit etwas passieren wird
- in einem perfekten System hat man eine Linie die irgendwann 1 erreichen wird
- in einem System der echten Welt können System versagen, wodurch Systeme niemals 1 erreichen können. Der Sättigungspunkt wird irgendwo darunter liegen und die Differenz zwischen diesem Punkt und 1 ist die Wahrscheinlichkeit eines Ausfalls wenn du für eine bestimmte Zeit wartest = unsachgemäße kumulative Verteilungsfunktion
- das ist etwas was in Haskell modelliert werden kann
- das geschieht, indem ΔQ eine Funktion ist, die den Zustand des Zufallsgenerators übernimmt
- ΔQ Formeln können für die Simulation genutzt werden aber auch für das algebraische verstehen
- this wird benutzt wenn man auf verschiedene Situationen schaut wie parallele oder sequenzielle Zusammensetzung
Hohe Sicherheit der Blockchainimplementierung
- Kryptowährungen halten einen sehr großen Wert
- IOHK denkt es ist besser Dinge umzusetzen mit einem sehr hohen Grad an Sicherheit
- die Forscher beweisen die Dinge des Protokolls aber müssen auch Sicherstellen das diese Beweise während der Übersetzung nicht verloren gehen
- es gibt sogar Vorschläge die Blockchain für kritische Infrastrukturen einzusetzen wie die Beurkundung von Grundstücksansprüchen
- wir müssen also ein System erschaffen, dass für diese Zwecke geeignet ist, auf Leistung ausgelegt ist und gleichzeitig nachweislich sicher ist.
Ich habe versucht soweit alles möglichts akkurat zu übersetzen, da hier aber sehr viele wissenschaftliche Themen der Informatik besprochen wurden wofür man schon fast ein Informatikstudium benötigt, könnten einige Teile nicht perfekt sein. Wenn ihr etwas ausbessern möchtet schreibt mir gerne eure Verbesserung. Lasst ein Herz
da - Danke!