Zwei Jahre später kehrte ich zu meinem Blog zurück, um einen Beitrag zu schreiben, der sich von den üblichen langweiligen Vorlesungen über Haskell und Mathematik unterscheidet. In den letzten Jahren habe ich mich mit Finanztechnologie in der EU befasst, und es scheint, dass es an der Zeit ist, über ein Thema zu schreiben, dem die technischen Medien wenig Aufmerksamkeit geschenkt haben.
Facebook hat kürzlich die so genannte „neue Finanzdienstleistungsplattform“ namens Libra veröffentlicht. Es ist als digitales Zahlungssystem positioniert, das auf einem Korb internationaler Währungen basiert, der in einer „Blockchain“ verwaltet und in einem von der Schweiz aus verwalteten Cashpool gespeichert wird. Die Ziele des Projekts sind ehrgeizig und haben weitreichende geopolitische Konsequenzen.
Die
Financial Times und die
New York Times haben viele sinnvolle Artikel über unvernünftige monetäre und wirtschaftliche Annahmen im Zentrum des vorgeschlagenen Finanzsystems. Es gibt jedoch nicht genügend Spezialisten, die eine Analyse aus technischer Sicht durchführen können. Da nicht viele Menschen an der Finanzinfrastruktur arbeiten und öffentlich über ihre Arbeit sprechen, wird dieses Projekt in den Fachmedien nicht zu stark thematisiert, obwohl es für die ganze Welt offen ist. Ich meine Open Source in den Repositories von
Libra und
Calibra Organization .
Für die Welt offen ist ein architektonisches schizophrenes Artefakt, das den Anspruch erhebt, eine sichere Plattform für die globale Zahlungsinfrastruktur zu sein.
Wenn Sie in die Codebasis eintauchen, weicht die tatsächliche Implementierung des Systems in höchst bizarrer Weise vollständig vom angegebenen Ziel ab. Ich bin sicher, dass dieses Projekt eine interessante Unternehmensgeschichte hat. Daher ist es logisch anzunehmen, dass es mit etwas Eifer entwickelt wurde, aber in Wirklichkeit sehe ich eine wirklich seltsame Reihe von Architekturlösungen, die das gesamte System zerstören und Benutzer gefährden.
Ich werde keine objektive Meinung über Facebook als Unternehmen behaupten. Nur wenige Leute in der IT-Branche sehen sie mit Sympathie an. Ein Vergleich ihrer Aussagen und des veröffentlichten Codes zeigt jedoch deutlich, dass der angegebene Zweck ein grundlegender Schwindel ist. Kurz gesagt, dieses Projekt befähigt niemanden. Er wird vollständig unter der Kontrolle eines Unternehmens bleiben, dessen Werbegeschäft so in Skandale und Korruption verwickelt ist, dass er keine andere Wahl hat, als zu versuchen, Zahlungen und Kreditwürdigkeit zu diversifizieren, um zu überleben. Ein klares langfristiges Ziel ist es, als Datenvermittler und Vermittler beim Zugang der Verbraucher zu Krediten auf der Grundlage ihrer persönlichen Daten in sozialen Netzwerken zu agieren. Dies ist eine völlig erschreckende und düstere Geschichte, die nicht die Aufmerksamkeit schenkt, die sie verdient.
Die einzige Rettung für diese Geschichte ist, dass das von ihnen erstellte Artefakt so lustig ist, dass es nicht zu der Aufgabe passt, die darin besteht, dass es nur als Akt des Stolzes angesehen werden kann. In diesem Projekt gibt es mehrere grundlegende Architekturfehler:
Die Lösung des Problems der byzantinischen Generäle in einem Netzwerk mit Zugriffskontrolle ist inkonsistent
Die Aufgabe der byzantinischen Generäle ist ein eher enges Forschungsfeld verteilter Systeme. Es beschreibt die Fähigkeit eines Netzwerksystems, willkürlichen Komponentenausfällen zu widerstehen, wenn Korrekturmaßnahmen ergriffen werden, die für das Funktionieren des Systems kritisch sind. Ein ausfallsicheres Netzwerk muss mehreren Arten von Angriffen standhalten, darunter Neustarts, Ausfälle, böswillige Angriffe und böswillige Abstimmungen bei Führungswahlen. Dies ist die Hauptlösung für die Libra-Architektur und ist hier völlig sinnlos.
Der Zeitaufwand für diese zusätzliche Struktur hängt vom Algorithmus ab. Es gibt eine Menge Literatur zu den Varianten der Paxos- und Raft-Protokolle mit der Lösung des byzantinischen Generäle-Problems, aber all diese Strukturen verursachen zusätzliche Overhead-Kosten für die Kommunikation
ein Quorum aufrechterhalten. Für die Waage haben wir den Algorithmus mit den höchstmöglichen Kommunikationskosten gewählt
im Falle eines Führungsversagens. Darüber hinaus entstehen durch die potenzielle Wiederwahl von Führungskräften für verschiedene Arten von Netzwerkausfallereignissen zusätzliche Kosten.
Für ein System, das in einem Konsortium stark regulierter transnationaler Unternehmen arbeitet, in dem alle Benutzer einen von Facebook signierten Code haben und der Zugriff auf das Netzwerk von Facebook kontrolliert wird, ist es einfach nicht sinnvoll, böswillige Teilnehmer auf Konsensebene zu betrachten. Es ist unklar, warum dieses System im Allgemeinen das Problem der byzantinischen Generäle löst und nicht nur einen konsistenten Prüfpfad zur Überprüfung der Einhaltung führt. Die Möglichkeit, dass der Libra-Host, der von Mastercard oder Andressen Horrowitz verwaltet wird, plötzlich schädlichen Code ausführt, ist ein seltsames Planungsszenario und wird besser gelöst, indem lediglich die Protokollintegrität und nichttechnische (d. H. Legale) Mittel sichergestellt werden.
Als Beweis für den Kongress wird das Produkt als Konkurrent zu neuen internationalen Zahlungsprotokollen wie WeChat, Alipay und M-Pesa deklariert. Keines dieser Systeme ist jedoch dafür ausgelegt, an Pools von Validatoren zu arbeiten, um das Problem der byzantinischen Generäle zu lösen. Sie werden einfach auf einem herkömmlichen Bus mit hohem Durchsatz konstruiert, der die Verkabelung nach einem festgelegten Regelwerk vornimmt. Dies ist ein natürlicher Ansatz für die Gestaltung eines Zahlungssystems.
Ein gut durchdachtes Zahlungssystem kann das Problem der doppelten Ausgaben und Gabeln einfach nicht lösen.
Der Overhead des Konsensalgorithmus löst kein Problem und begrenzt die Systemkapazität nur aus keinem anderen Grund als dem Frachtkult der öffentlichen Blockchain, der nicht für diesen Anwendungsfall vorgesehen ist.
Die Waage hat keinen Transaktionsschutz
Gemäß der Dokumentation ist das System unter Berücksichtigung der
Pseudonymität ausgelegt , dh die im Protokoll verwendeten Adressen stammen aus öffentlichen Schlüsseln auf elliptischen Kurven und enthalten keine Metadaten zu Konten. Nirgendwo in der Beschreibung der Verwaltungsstruktur für die Organisation oder im Protokoll selbst wird angegeben, wie die an Transaktionen beteiligten Wirtschaftsdaten vor den Prüfern verborgen werden. Das System ist für die groß angelegte Nachbildung von Transaktionen für eine Reihe von externen Parteien konzipiert, die im Einklang mit den geltenden europäischen und amerikanischen Gesetzen zum Bankgeheimnis nicht auf wirtschaftliche Details abzielen sollten.
Datenrichtlinien in verschiedenen Ländern sind schwierig zu koordinieren, insbesondere angesichts unterschiedlicher Gesetze und Vorschriften in verschiedenen Gerichtsbarkeiten, die unterschiedliche kulturelle Ansichten zum Datenschutz und zur Privatsphäre vertreten. Das Protokoll selbst steht standardmäßig allen Mitgliedern des Konsortiums offen. Dies ist ein klarer technischer Mangel, der nicht den Anforderungen entspricht, für die es entwickelt wurde.
Libra HotStuff BFT kann die für das Zahlungssystem erforderliche Bandbreite nicht erreichen
In Großbritannien können Clearingsysteme wie BAC etwa 580 Millionen Transaktionen pro Monat ausführen. Gleichzeitig können hochoptimierte Systeme wie Visa 150.000.000 Transaktionen pro Tag verarbeiten. Die Leistung hängt von der Transaktionsgröße, dem Netzwerk-Routing, der Systemlast und den
AML-Überprüfungen ab (Geldwäsche- und Geldwäschesysteme).
Die Waage versucht, Probleme zu lösen, die bei Inlandsüberweisungen keine wirklichen Probleme darstellen, da die Nationalstaaten in den letzten zehn Jahren ihre Clearing-Infrastruktur modernisiert haben. Für Privatkunden in der Europäischen Union ist der Geldumzug überhaupt kein Problem. Auf einer herkömmlichen Infrastruktur kann dies mit einem Standard-Smartphone in Sekunden erledigt werden. Für große Unternehmenstransfers gibt es verschiedene Mechanismen und Regeln, die sich auf den Transport großer Geldmengen beziehen.
Es gibt keine technischen Gründe, warum auch grenzüberschreitende Zahlungen nicht sofort ausgeführt werden können, mit Ausnahme von Unterschieden in den Regeln und Anforderungen zwischen den jeweiligen Gerichtsbarkeiten. Wenn die erforderlichen vorbeugenden Maßnahmen (Sorgfaltspflicht des Kunden, Überprüfung von Sanktionen usw.) mehrmals in verschiedenen Phasen der Transaktionskette durchgeführt werden, kann dies zu einer Verzögerung der Transaktion führen. Diese Verzögerung ist jedoch nur eine Funktion des Regulierungsrechts und seiner Durchsetzung, nicht der Technologie.
Für Verbraucher gibt es keinen Grund, warum ein Geschäft in Großbritannien nicht innerhalb von Sekunden abgeschlossen werden kann. Einzelhandelsgeschäfte in der EU verlangsamen sich in
Bezug auf
KYC-Schecks (Know Your Customer) und AML-Beschränkungen, die von Regierungen und Aufsichtsbehörden auferlegt wurden und gleichermaßen für Waagenzahlungen gelten. Auch wenn Facebook die Hindernisse für den internationalen Transfer und die Übertragung privater Daten überwindet, ist das vorgeschlagene Modell Hunderte von Mannjahren vom Durchsatz globaler Transaktionen entfernt und wird wahrscheinlich von Grund auf neu verarbeitet.
Die Sprache von Libra Move ist falsch
Das Whitepaper enthält kühne Aussagen zu einer neuen, nicht überprüften Sprache namens Move. Diese Aussagen sind aus Sicht der Theorie der Programmiersprachen (PLT) eher zweifelhaft.
Move ist eine neue Programmiersprache für die Implementierung benutzerdefinierter Transaktionslogik und "intelligenter Verträge" in der Libra-Blockchain. Da Libra eines Tages Milliarden von Menschen bedienen will, hat Move höchste Priorität bei der Sicherheit.
Ein wichtiges Merkmal von Move ist die Fähigkeit, beliebige Ressourcentypen mit einer von der linearen Logik inspirierten Semantik zu definieren.
In öffentlichen Blockchains stoßen intelligente Verträge auf die Logik öffentlicher Netzwerke mit Treuhandkonten, Geldwäsche, der Ausgabe von außerbörslichen Token und Glücksspielen. All dies geschieht in einer erstaunlich schlecht gestalteten Sprache namens Solidity, die aus akademischer Sicht den Autor von PHP wie ein Genie erscheinen lässt. Seltsamerweise scheint die neue Sprache von Facebook nichts mit diesen Technologien zu tun zu haben, da es sich tatsächlich um eine Skriptsprache handelt, die für obskure Unternehmensaufgaben entwickelt wurde.
In privaten verteilten Ledgern sind intelligente Verträge einer jener Begriffe, die Berater ohne besondere Beachtung klarer Definitionen oder Ziele streuen. Unternehmenssoftwareberater verdienen in der Regel Geld mit Mehrdeutigkeiten, und intelligente Verträge sind die Apotheose des Unternehmensobskurantismus, da sie wörtlich als alles definiert werden können.
Nach Aussagen über seine Sicherheit sollten wir uns die Semantik der Sprache ansehen. Die Richtigkeit in der Theorie der Programmiersprachen besteht normalerweise aus zwei verschiedenen Beweisen: "Fortschritt" und "Bewahrung", die die Konsistenz des gesamten Raums der Bewertungsregeln für eine Sprache bestimmen. Genauer gesagt ist eine Funktion in der Typentheorie "linear", wenn sie ihr Argument genau einmal verwendet, und "affin", wenn sie es nicht mehr als einmal verwendet. Das lineare Typensystem bietet eine statische Garantie dafür, dass die deklarierte lineare Funktion wirklich linear ist. Es weist allen Unterausdrücken von Funktionen Typen zu und verfolgt die Anrufpositionen. Dies ist eine subtile Eigenschaft für den Beweis, und es ist nicht einfach, sie für das gesamte Programm zu implementieren. Die lineare Typisierung ist immer noch ein sehr akademisches Forschungsgebiet, das von der Einzigartigkeit der Typen in Clean und dem Besitz von Typen in Rust beeinflusst wird. Es gibt einige vorläufige Vorschläge zum Hinzufügen linearer Typen zum Glasgow Haskell Compiler.
Die Move-Anweisung zur Verwendung von linearen Typen scheint unangemessen in den Compiler einzutauchen, da es
keine solche Typüberprüfungslogik gibt . Soweit man urteilen kann, zitiert das technische Dokument kanonische Literatur von Girard und Pierce, und in der tatsächlichen Umsetzung gibt es nichts dergleichen.
Darüber hinaus ist die formale Semantik einer vermeintlich sicheren Sprache weder in der Implementierung noch im Dokument zu finden. Die Sprache ist klein genug, um einen vollständigen Beweis für die Richtigkeit der Semantik in Coq oder Isabelle zu finden. In der Realität kann der End-to-End-Compiler der vollständigen Konvertierung mit der Übertragung von Beweisen in Bytecode mit modernen Werkzeugen implementiert werden, die im letzten Jahrzehnt erfunden wurden. Wir wissen, wie das geht, angefangen mit der
Arbeit von George Nekula und Peter Lee im Jahr 1996.
Aus der Sicht der Theorie der Programmiersprachen ist es unmöglich, die Aussage zu bestätigen, dass Move eine zuverlässige und sichere Sprache ist, da diese Aussagen nur auf das Winken und Vermarkten und nicht auf tatsächliche Beweise zurückzuführen sind. Dies ist eine alarmierende Situation für ein Sprachentwicklungsprojekt, bei dem vorgeschlagen wird, Milliarden von Dollar für die Transaktionsverarbeitung bereitzustellen.
Die Kryptographie der Waage ist falsch
Das Erstellen zuverlässiger Kryptosysteme ist ein sehr komplexes technisches Problem, und es ist immer besser, gefährlichen Code mit einer guten Dosis gesunder Paranoia zu behandeln. In diesem Bereich gibt es wichtige Durchbrüche, wie das Microsoft Everest-Projekt, das einen überprüfbaren sicheren
TLS-Stack erstellt . Es gibt bereits Werkzeuge zum Erstellen überprüfbarer Grundelemente. Obwohl es teuer ist, geht es eindeutig nicht über die wirtschaftlichen Möglichkeiten von Facebook hinaus. Das Team entschied sich jedoch, nicht an dem Projekt teilzunehmen, das als verlässliche Grundlage für das globale Finanzsystem erklärt wurde.
Das libra-Projekt
stützt sich auf mehrere relativ neue Bibliotheken zur Erstellung experimenteller Kryptosysteme, die erst in den letzten Jahren erschienen sind. Es ist unmöglich zu sagen, ob die Abhängigkeiten von den folgenden Tools sicher sind oder nicht, da keine dieser Bibliotheken geprüft wurde und keine Standard-Veröffentlichungsrichtlinien enthält. Insbesondere für einige große Bibliotheken gibt es keine Gewissheit hinsichtlich des Schutzes vor Angriffen auf Drittanbieter-Kanäle und Zeitangriffen.
- ed25519-dalek
- curve25519-dalek
Die Libra-Bibliothek ist noch experimenteller und geht über das
Standardmodell hinaus, indem sie sehr neue Methoden wie überprüfbare Zufallsfunktionen (VRFs), bilineare Paare und Schwellensignaturen verwendet. Diese Methoden und Bibliotheken mögen vernünftig sein, aber die Kombination aller Methoden in einem System wirft ernsthafte Bedenken hinsichtlich der Angriffsfläche auf. Die Kombination all dieser neuen Tools und Techniken erhöht die Komplexität der Sicherheitsnachweise erheblich.
Es ist anzunehmen, dass dieser gesamte kryptografische Stapel bis zum Beweis des Gegenteils für verschiedene Angriffe anfällig ist. Das bekannte Facebook-Modell "Move Fast and Break Things" kann nicht auf kryptografische Tools angewendet werden, die die Finanzdaten von Kunden verarbeiten.
Die Waage kann keine Verbraucherschutzmechanismen implementieren
Eine Besonderheit des Zahlungssystems ist die Möglichkeit, die Transaktion zurückzusetzen, wenn die Zahlung durch einen Rechtsstreit storniert wird oder zu einem Unfall oder Systemausfall führt. Die Waage ist so konzipiert, dass sie vollständig ausgefüllt ist und keinen Transaktionstyp zum Stornieren einer Zahlung enthält. In Großbritannien unterliegen alle Zahlungen von £ 100 bis £ 30.000 dem Verbraucherkreditgesetz. Dies bedeutet, dass das Zahlungssystem im Falle eines Problems mit der gekauften Ware oder wenn der Zahlungsempfänger die Dienstleistung nicht erbracht hat, die Verantwortung mit dem Verkäufer teilt. Ähnliche Regeln gelten in der EU, in Asien und in Nordamerika.
Das derzeitige Design der Waage enthält kein Protokoll zur Einhaltung dieser Gesetze und verfügt nicht über einen klaren Plan für dessen Erstellung. Noch schlimmer ist, dass aus architektonischer Sicht die Endgültigkeit der Struktur authentifizierter Kerneldaten, basierend auf dem Zustand des Merkle-Laufwerks, keinen Mechanismus zum Erstellen eines solchen Protokolls zulässt, ohne den Kernel neu zu entwerfen.
Nach einer technischen Prüfung dieses Projekts können wir feststellen, dass es den Test in keinem anerkannten Journal für verteilte Systemforschung oder Financial Engineering bestehen wird. Um zu versuchen, die globale Geldpolitik zu ändern, muss eine Menge technischer Arbeit geleistet werden, um ein zuverlässiges Netzwerk und eine sichere Verarbeitung von Benutzerdaten zu schaffen, denen die öffentliche Hand und die Aufsichtsbehörden vertrauen können.
Ich sehe keinen Grund zu der Annahme, dass Facebook in seinem Projekt die notwendige Arbeit geleistet hat, um diese technischen Probleme zu überwinden, oder dass es einige technische Vorteile gegenüber der vorhandenen Infrastruktur hat.
Die Behauptung, dass ein Unternehmen regulatorische Flexibilität benötigt, um sich über Innovationen zu informieren, ist keine Entschuldigung dafür, diese nicht zuerst zu erstellen.