Efter två år återvände jag till bloggen för ett inlägg som skiljer sig från de vanliga tråkiga föreläsningarna om Haskell och matematik. Jag har arbetat med fintech i EU de senaste åren och det verkar som att det är dags att skriva om ett ämne som har fått lite uppmärksamhet från teknikmedia.
Facebook släppte nyligen vad de kallar en "ny plattform för finansiella tjänster" kallad Libra. Det är positionerat som ett digitalt avvecklingssystem baserat på en korg av internationella valutor som hanteras på en "blockchain" och lagras i en pengapool som hanteras från Schweiz. Målen för projektet är ambitiösa och medför storskaliga geopolitiska konsekvenser.
В и Massor av vettiga artiklar om de osunda monetära och ekonomiska antagandena bakom det föreslagna finansiella systemet. Men det finns inte tillräckligt med specialister som kan analysera ur teknisk synvinkel. Det är inte många som arbetar med finansiell infrastruktur och pratar offentligt om sitt arbete, så det här projektet får inte mycket bevakning i tekniska media, även om dess inre är öppna för världen. Jag menar öppen källkod i arkiv и .
Det som är öppet för världen är en arkitektoniskt schizofren artefakt med anspråk på att vara en säker plattform för den globala betalningsinfrastrukturen.
Om du dyker in i kodbasen avviker den faktiska implementeringen av systemet helt från det angivna målet, och på de mest bisarra sätt. Jag är säker på att detta projekt har en intressant företagshistoria. Så det är logiskt att anta att det designades med viss flit, men i verkligheten ser jag en riktigt märklig uppsättning arkitektoniska beslut som bryter hela systemet och utsätter användarna för risker.
Jag kommer inte att låtsas ha en objektiv åsikt om Facebook som företag. Få människor i IT-branschen ser på henne med sympati. Men en jämförelse av dess uttalanden och den publicerade koden visar tydligt att det uttalade syftet i grunden är vilseledande. Kort sagt, detta projekt ger ingen makt. Han kommer att förbli helt under kontroll av ett företag vars reklamverksamhet är så fast i skandal och korruption att det inte har något annat val än att försöka diversifiera sina betalningar och kreditvärdighet för att överleva. Det tydliga långsiktiga målet är att agera dataförmedlare och mellanhand i konsumenters tillgång till kredit baserat på deras personliga sociala mediedata. Det här är en helt fruktansvärd och mörk historia som inte får den uppmärksamhet den förtjänar.
Den enda räddande nåden med denna berättelse är att artefakten de skapade är så lustigt olämplig för uppgiften att den bara kan ses som en hybrishandling. Det finns flera stora arkitektoniska fel i detta projekt:
Att lösa det bysantinska generalsproblemet i ett åtkomstkontrollnätverk är en inkonsekvent design
Problemet med de bysantinska generalerna är ett ganska snävt område för forskning av distribuerade system. Den beskriver förmågan hos ett nätverkssystem att motstå slumpmässiga komponentfel samtidigt som de vidtar korrigerande åtgärder som är avgörande för systemets funktion. Ett motståndskraftigt nätverk måste stå emot flera typer av attacker, inklusive omstarter, avbrott, skadlig belastning och skadlig röstning i ledarskapsval. Detta är huvudbeslutet för Libra-arkitekturen, och det är helt meningslöst.
Tidskomplexiteten för denna extra struktur beror på algoritmen. Det finns mycket litteratur om varianter av Paxos- och Raft-protokollen som löser problemet med bysantinska generaler, men alla dessa strukturer introducerar ytterligare overhead för kommunikation över 
att upprätthålla beslutförhet. För Vågen valde de en algoritm med högsta möjliga kommunikationskostnad vid misslyckande av ledarskapet. Och det finns ytterligare omkostnader från potentiella omval av ledare över flera typer av nätverksfel.
För ett system som fungerar inom ett konsortium av högt reglerade multinationella företag, där alla användare har kod signerad av Facebook och åtkomst till nätverket kontrolleras av Facebook, är det helt enkelt inte meningsfullt att överväga skadliga deltagare på konsensusnivå. Det är inte klart varför detta system ens skulle lösa problemet med bysantinska generaler, snarare än att bara upprätthålla ett konsekvent revisionsspår för att kontrollera efterlevnaden. Möjligheten att en Libra-nod som drivs av Mastercard eller Andressen Horrowitz plötsligt börjar köra skadlig kod är ett udda scenario att planera för och åtgärdas bättre genom att helt enkelt säkerställa protokollintegritet och icke-tekniska (dvs lagliga) medel.
Vittnesmål till kongressen fakturerade produkten som en konkurrent till nya internationella betalningsprotokoll som WeChat, Alipay och M-Pesa. Inget av dessa system är dock utformat för att köras på valideringspooler för att lösa problemet med bysantinska generaler. De är helt enkelt designade på en traditionell buss med hög bandbredd som gör ledningar enligt en fast uppsättning regler. Detta är ett naturligt sätt att utforma ett betalningssystem. Väl-designad betalningssystemet kommer helt enkelt inte att stöta på problemet med dubbla utgifter och gafflar.
Konsensusalgoritmens overhead löser inga problem och begränsar bara systemets genomströmning utan någon annan anledning än lastkulten av den offentliga blockkedjan, som inte är avsedd för detta användningsfall.
Vågen har ingen transaktionssekretess
Enligt dokumentationen är systemet utformat med hänsyn tagen pseudonymitet, det vill säga adresserna som används i protokollet erhålls från publika nycklar på elliptiska kurvor och innehåller inte metadata om konton. Men ingenstans i beskrivningen av organisationens styrningsstruktur eller i själva protokollet anger det hur de ekonomiska data som är involverade i transaktioner kommer att döljas för validerare. Systemet är utformat för att replikera transaktioner i stor skala till en rad externa parter som, enligt befintliga europeiska och amerikanska lagar om banksekretess, inte bör vara insatta i de ekonomiska detaljerna.
Datapolicyer mellan länder är svåra att samordna, särskilt med tanke på olika lagar och förordningar i olika jurisdiktioner med olika kulturella syn på dataskydd och integritet. Själva protokollet är som standard helt öppet för konsortiummedlemmar, vilket är en tydlig teknisk brist som inte uppfyller de krav som det är utformat för.
Libra HotStuff BFT kan inte uppnå den genomströmning som krävs för ett betalningssystem
I Storbritannien kan clearingsystem som BAC hantera cirka 580 000 000 transaktioner per månad. Samtidigt kan högoptimerade system som Visa behandla 150 000 000 transaktioner per dag. Prestanda varierar beroende på transaktionsstorlek, nätverksrouting, systembelastning och (anti-penningtvätt, penningtvättssystem).
Vågen försöker lösa problem som egentligen inte är problem för inhemska överföringar, eftersom nationalstater har moderniserat sin clearinginfrastruktur under det senaste decenniet. För detaljhandelskonsumenter i EU är det inte alls ett problem att flytta pengar. På traditionell infrastruktur kan detta göras med en vanlig smartphone på några sekunder. För stora företagsöverföringar finns det olika mekanismer och regler för att flytta stora summor pengar.
Det finns inget tekniskt skäl till varför gränsöverskridande betalningar inte också kan behandlas omedelbart, annat än skillnader i regler och krav mellan de relevanta jurisdiktionerna. Om nödvändiga förebyggande åtgärder (kundkännedom, sanktionskontroller etc.) utförs flera gånger i olika skeden av transaktionskedjan kan detta resultera i en försening av transaktionen. Denna fördröjning är dock enbart en funktion av reglerande lagstiftning och efterlevnad, inte teknik.
För konsumenter finns det ingen anledning till varför en brittisk transaktion inte skulle klara av på några sekunder. Detaljhandelstransaktioner i EU saktar verkligen in (Känn din kund) och AML-restriktioner som införts av regeringar och tillsynsmyndigheter, som gäller lika för Vågen-betalningar. Även om Facebook skulle övervinna hindren för gränsöverskridande överföringar och privata dataöverföringar, är den föreslagna modellen hundratals personår borta från global transaktionsgenomströmning och skulle sannolikt behöva göras om från grunden.
Libra Move-språket är felaktigt
Vitboken gör djärva påståenden om ett nytt, oprövat språk som heter Move. Dessa påståenden är ganska tveksamma ur programmeringsspråksteorin (PLT).
Move är ett nytt programmeringsspråk för att implementera anpassad transaktionslogik och smarta kontrakt på Libra blockchain. Eftersom Libra siktar på att en dag tjäna miljarder människor, är Move designad med säkerhet som högsta prioritet.
En nyckelfunktion i Move är förmågan att definiera godtyckliga resurstyper med semantik inspirerad av linjär logik.
I offentliga blockkedjor möter smarta kontrakt logiken hos offentliga nätverk med spärrade konton, penningtvätt, utfärdande av OTC-token och hasardspel. Allt detta görs på ett förbluffande dåligt designat språk som heter Solidity, vilket ur akademisk synvinkel får författaren till PHP att se ut som ett geni. Konstigt nog verkar det nya språket från Facebook inte ha något att göra med dessa teknologier, eftersom det faktiskt är ett skriptspråk avsett för dunkla företagsändamål.
I privata distribuerade reskontra är smarta kontrakt en av de termer som slängs runt av konsulter utan större hänsyn till tydlig definition eller syfte. Konsulter för företagsmjukvaror tjänar vanligtvis pengar på oklarheter, och smarta kontrakt är apoteosen för företagens obskurantism eftersom de kan definieras som bokstavligen vad som helst.
Efter att ha gjort påståenden om dess säkerhet måste vi titta på språkets semantik. Korrekthet i programmeringsspråksteori består vanligtvis av två olika bevis: "framsteg" och "bevarande", som bestämmer överensstämmelsen i hela utrymmet av utvärderingsregler för språket. Mer specifikt, i typteorin är en funktion "linjär" om den använder sitt argument exakt en gång, och "affin" om den använder det högst en gång. Det linjära typsystemet ger statisk garanti för att en deklarerad linjär funktion verkligen är linjär genom att tilldela typer till alla funktionsunderuttryck och hålla reda på var anrop görs. Detta är en subtil egenskap att bevisa och är inte lätt att implementera för ett helt program. Linjär typning är fortfarande ett mycket akademiskt studieområde, påverkat av implementeringen av typunikitet i Clean och typägande i Rust. Det finns några preliminära förslag för att lägga till linjära typer till Glasgow Haskell Compiler.
Moves uttalande om att använda linjära typer verkar som ett obefogat dyk in i kompilatorn, eftersom det . Så vitt man kan säga citerar whitepaper kanonisk litteratur från Girard och Peirce, och det finns inget liknande i själva implementeringen.
Dessutom förekommer den formella semantiken för det förment säkra språket ingenstans i vare sig implementeringen eller dokumentet. Språket är tillräckligt litet för att hitta ett fullständigt bevis på korrekt semantik i Coq eller Isabelle. I verkligheten är en komplett konverteringskompilator med bevisöverföring till bytekod fullt möjlig att implementera med moderna verktyg som uppfanns under det senaste decenniet. Vi vet hur man gör det, till att börja med tillbaka 1996.
Ur ett programmeringsspråksteoretiskt perspektiv är det omöjligt att testa påståendet att Move är ett tillförlitligt och säkert språk, eftersom dessa påståenden uppgår till rent handviftande och marknadsföring snarare än faktiska bevis. Detta är en alarmerande situation för ett språkprojekt som uppmanas att behandla miljarder dollar i transaktioner.
Vågens kryptografi är felaktig
Att bygga säkra kryptosystem är ett mycket svårt tekniskt problem, och det är alltid bäst att närma sig att arbeta med farlig kod med en god dos hälsosam paranoia. Det finns stora genombrott inom detta område, som Microsoft Everest-projektet, som bygger en verifierbar säker . Det finns redan verktyg för att skapa verifierbara primitiver. Även om detta är dyrt är det helt klart inte utanför Facebooks ekonomiska kapacitet. Teamet beslutade dock att inte delta i projektet, som tillkännagavs som en pålitlig grund för det globala finansiella systemet.
Libra projekt från flera ganska nya bibliotek för att skapa experimentella kryptosystem som bara har dykt upp de senaste åren. Det är omöjligt att säga om beroenden av följande verktyg är säkra eller inte, eftersom inget av dessa bibliotek har granskats och inte har standardpolicyer för upplysningar. I synnerhet för vissa kärnbibliotek finns det ingen säkerhet angående skydd mot sidokanalattacker och timingattacker.
Biblioteket blir ännu mer experimentellt och går längre än så , med användning av mycket nya tekniker såsom verifierbara slumpmässiga funktioner (VRF), bilinjära par och tröskelsignaturer. Dessa metoder och bibliotek kan vara rimliga, men att kombinera dem alla i ett system väcker allvarliga farhågor om attackens yta. Kombinationen av alla dessa nya verktyg och tekniker ökar avsevärt komplexiteten i att bevisa säkerhet.
Det bör antas att hela denna kryptografiska stack är sårbar för olika attacker tills motsatsen bevisats. Facebooks berömda modell "Move Fast and Break Things" kan inte tillämpas på kryptografiska verktyg som behandlar kunddata.
Vågen misslyckas med att implementera konsumentskyddsmekanismer
En utmärkande egenskap hos betalningssystemet är möjligheten att återställa en transaktion om betalningen avbryts av en rättegång eller leder till ett oavsiktligt eller systemfel. Libra-systemet är designat för att vara "komplett" och inkluderar inte en transaktionstyp för annullering av betalning. I Storbritannien är alla betalningar mellan £100 och £30,000 XNUMX föremål för Consumer Credit Act. Det innebär att betalningssystemet delar ansvaret med säljaren vid problem med den köpta produkten eller om mottagaren av betalningen inte tillhandahåller tjänsten. Liknande regler gäller i EU, Asien och Nordamerika.
Den nuvarande designen av Vågen innehåller inte ett protokoll för att följa dessa lagar och har ingen tydlig plan för att skapa en. Ännu värre, ur ett arkitektoniskt perspektiv tillåter inte den slutgiltiga kärnans autentiserade datastruktur, baserat på tillståndet för Merkle-enheten, någon mekanism för att skapa ett sådant protokoll utan att göra om kärnan.
Efter att ha genomfört en teknisk granskning av detta projekt kan vi dra slutsatsen att det helt enkelt inte kommer att passera i någon respekterad tidskrift för distribuerad systemforskning eller finansteknisk tidskrift. För att försöka förändra den globala penningpolitiken krävs ett enormt tekniskt arbete för att skapa ett tillförlitligt nätverk och säker behandling av användardata som allmänheten och tillsynsmyndigheter kan lita på.
Jag ser ingen anledning att tro att Facebook har gjort det nödvändiga arbetet i sin design för att övervinna dessa tekniska problem eller att det har några tekniska fördelar jämfört med den nuvarande infrastrukturen. Att säga att ett företag behöver regulatorisk flexibilitet för att utforska innovationer är inte en ursäkt för att inte göra dem först.
Källa: will.com