Na twee jaar keerde ik terug naar de blog voor een bericht dat afwijkt van de gebruikelijke saaie lezingen over Haskell en wiskunde. Ik heb de afgelopen jaren in de EU aan fintech gewerkt en het lijkt erop dat de tijd is gekomen om over een onderwerp te schrijven dat weinig aandacht heeft gekregen van de techmedia.
Facebook heeft onlangs een zogenaamd ‘nieuw platform voor financiële diensten’ uitgebracht, genaamd Libra. Het is gepositioneerd als een digitaal verrekeningssysteem gebaseerd op een mandje met internationale valuta die worden beheerd op een ‘blockchain’ en opgeslagen in een geldpool die wordt beheerd vanuit Zwitserland. De doelstellingen van het project zijn ambitieus en brengen grootschalige geopolitieke gevolgen met zich mee.
В и Veel verstandige artikelen over de ondeugdelijke monetaire en economische aannames achter het voorgestelde financiële systeem. Maar er zijn niet genoeg specialisten die vanuit technisch oogpunt kunnen analyseren. Er zijn niet veel mensen die aan de financiële infrastructuur werken en in het openbaar over hun werk praten, dus dit project krijgt niet veel aandacht in de technische media, ook al staan de ingewanden open voor de wereld. Ik bedoel open source in repositories и .
Wat voor de wereld openstaat, is een architectonisch schizofreen artefact dat beweert een veilig platform te zijn voor de mondiale betalingsinfrastructuur.
Als je in de codebasis duikt, wijkt de daadwerkelijke implementatie van het systeem volledig af van het gestelde doel, en wel op de meest bizarre manieren. Ik ben er zeker van dat dit project een interessante bedrijfsgeschiedenis heeft. Het is dus logisch om aan te nemen dat het met enige zorgvuldigheid is ontworpen, maar in werkelijkheid zie ik een heel vreemde reeks architecturale beslissingen die het hele systeem kapot maken en gebruikers in gevaar brengen.
Ik zal niet pretenderen een objectieve mening te hebben over Facebook als bedrijf. Er zijn maar weinig mensen in de IT-industrie die met medeleven naar haar kijken. Maar een vergelijking van de verklaringen en de gepubliceerde code laat duidelijk zien dat het gestelde doel fundamenteel misleidend is. Kortom, dit project geeft niemand macht. Hij zal volledig onder de controle blijven van een bedrijf waarvan de reclameactiviteiten zo verwikkeld zijn in schandalen en corruptie dat het geen andere keus heeft dan te proberen zijn betalingen en kredietscores te diversifiëren om te overleven. Het duidelijke langetermijndoel is om op te treden als datamakelaar en tussenpersoon in de toegang van consumenten tot krediet op basis van hun persoonlijke socialemediagegevens. Dit is een absoluut gruwelijk en duister verhaal dat niet de aandacht krijgt die het verdient.
De enige goedmaker van dit verhaal is dat het artefact dat ze hebben gemaakt zo hilarisch ongeschikt is voor de taak die voorhanden is dat het alleen kan worden gezien als een daad van hoogmoed. Er zijn verschillende grote architectonische fouten in dit project:
Het oplossen van het Byzantijnse generaalsprobleem in een toegangscontrolenetwerk is een inconsistent ontwerp
Het probleem van de Byzantijnse generaals is een vrij beperkt onderzoeksgebied van gedistribueerde systemen. Het beschrijft het vermogen van een netwerksysteem om willekeurige componentstoringen te weerstaan en tegelijkertijd corrigerende maatregelen te nemen die cruciaal zijn voor de werking van het systeem. Een veerkrachtig netwerk moet bestand zijn tegen verschillende soorten aanvallen, waaronder herstarts, uitval, kwaadwillige belasting en kwaadwillig stemmen bij leiderschapsverkiezingen. Dit is de belangrijkste beslissing voor de Libra-architectuur, en het is hier volkomen zinloos.
De tijdcomplexiteitsoverhead van deze aanvullende structuur is afhankelijk van het algoritme. Er is veel literatuur over varianten van de Paxos- en Raft-protocollen die het probleem van de Byzantijnse generaals oplossen, maar al deze structuren introduceren extra overhead voor communicatie via 
quorum te behouden. Voor Libra kozen ze voor een algoritme met de hoogst mogelijke communicatiekosten bij falend leiderschap. En er is extra overhead als gevolg van potentiële herverkiezing van leiders bij meerdere soorten netwerkstoringen.
Voor een systeem dat opereert binnen een consortium van sterk gereguleerde multinationale ondernemingen, waarbij alle gebruikers code hebben die is ondertekend door Facebook en de toegang tot het netwerk wordt gecontroleerd door Facebook, heeft het eenvoudigweg geen zin om kwaadwillende deelnemers op consensusniveau te beschouwen. Het is niet duidelijk waarom dit systeem zelfs maar het probleem van de Byzantijnse generaals zou oplossen, in plaats van simpelweg een consistent audittraject in stand te houden om de naleving ervan te controleren. De mogelijkheid dat een Libra-knooppunt dat wordt beheerd door Mastercard of Andressen Horrowitz plotseling kwaadaardige code gaat draaien, is een vreemd scenario om op te plannen en kan beter worden aangepakt door simpelweg de protocolintegriteit en niet-technische (d.w.z. juridische) middelen te garanderen.
Getuigenis aan het Congres bestempelde het product als een concurrent van nieuwe internationale betalingsprotocollen zoals WeChat, Alipay en M-Pesa. Geen van deze systemen is echter ontworpen om op validatorpools te draaien om het probleem van de Byzantijnse generaals op te lossen. Ze zijn eenvoudigweg ontworpen op een traditionele bus met hoge bandbreedte die de bedrading volgens een vaste reeks regels maakt. Dit is een natuurlijke benadering bij het ontwerpen van een betalingssysteem. Goed ontworpen het betalingssysteem zal simpelweg niet te maken krijgen met het probleem van dubbele uitgaven en vorken.
De overhead van het consensusalgoritme lost geen enkel probleem op en beperkt alleen de doorvoer van het systeem om geen andere reden dan de ladingcultus van de publieke blockchain, die niet bedoeld is voor deze use case.
Weegschaal heeft geen transactieprivacy
Volgens de documentatie is het systeem ontworpen met inachtneming van pseudonimiteit, dat wil zeggen dat de adressen die in het protocol worden gebruikt, worden verkregen uit openbare sleutels op elliptische curven en geen metagegevens over accounts bevatten. Nergens in de beschrijving van de bestuursstructuur van de organisatie of in het protocol zelf wordt echter aangegeven hoe de economische gegevens die betrokken zijn bij transacties verborgen zullen blijven voor validators. Het systeem is ontworpen om transacties op grote schaal te repliceren naar een reeks externe partijen die, volgens de bestaande Europese en Amerikaanse bankgeheimwetten, niet op de hoogte mogen zijn van de economische details.
Het databeleid van verschillende landen is moeilijk te coördineren, vooral gezien de uiteenlopende wet- en regelgeving in verschillende rechtsgebieden met verschillende culturele opvattingen over gegevensbescherming en privacy. Het protocol zelf staat standaard volledig open voor consortiumleden, wat een duidelijke technische tekortkoming is die niet voldoet aan de eisen waarvoor het is ontworpen.
Libra HotStuff BFT kan de voor een betalingssysteem vereiste doorvoersnelheid niet realiseren
In Groot-Brittannië kunnen clearingsystemen zoals BAC ongeveer 580 transacties per maand verwerken. Tegelijkertijd kunnen sterk geoptimaliseerde systemen zoals Visa 000 transacties per dag verwerken. De prestaties variëren afhankelijk van de transactiegrootte, netwerkroutering, systeembelasting en (bestrijding van het witwassen van geld, witwasprogramma’s).
Libra probeert problemen op te lossen die niet echt problemen opleveren voor binnenlandse overdrachten, nu de nationale staten hun clearinginfrastructuur de afgelopen tien jaar hebben gemoderniseerd. Voor particuliere consumenten in de Europese Unie is het overmaken van geld helemaal geen probleem. Op traditionele infrastructuur kan dit met een standaard smartphone binnen enkele seconden worden gedaan. Voor grote bedrijfsoverdrachten zijn er verschillende mechanismen en regels verbonden aan het verplaatsen van grote geldbedragen.
Er is geen technische reden waarom grensoverschrijdende betalingen niet ook onmiddellijk kunnen worden verwerkt, anders dan verschillen in regels en vereisten tussen de relevante rechtsgebieden. Als de noodzakelijke preventieve maatregelen (klantenonderzoek, sanctiecontroles etc.) meerdere keren worden uitgevoerd in verschillende fasen van de transactieketen, kan dit vertraging in de transactie tot gevolg hebben. Deze vertraging is echter puur een gevolg van de regelgeving en de naleving ervan, en niet van de technologie.
Voor consumenten is er geen reden waarom een Britse transactie niet binnen enkele seconden zou worden afgehandeld. De detailhandelstransacties in de EU vertragen inderdaad (Know Your Customer) en AML-beperkingen opgelegd door overheden en toezichthouders, die eveneens van toepassing zijn op Libra-betalingen. Zelfs als Facebook de barrières voor grensoverschrijdende overdrachten en particuliere gegevensoverdrachten zou overwinnen, is het voorgestelde model honderden mensjaren verwijderd van de mondiale transactiedoorvoer en zou het waarschijnlijk helemaal opnieuw moeten worden ontworpen.
Libra Move-taal is onjuist
Het witboek doet gedurfde beweringen over een nieuwe, ongeteste taal genaamd Move. Deze uitspraken zijn nogal twijfelachtig vanuit het oogpunt van de programmeertaaltheorie (PLT).
Move is een nieuwe programmeertaal voor het implementeren van aangepaste transactielogica en slimme contracten op de Libra-blockchain. Omdat Libra ernaar streeft om op een dag miljarden mensen te bedienen, is Move ontworpen met veiligheid als topprioriteit.
Een belangrijk kenmerk van Move is de mogelijkheid om willekeurige resourcetypen te definiëren met semantiek geïnspireerd door lineaire logica.
In openbare blockchains worden slimme contracten geconfronteerd met de logica van openbare netwerken met geblokkeerde rekeningen, het witwassen van geld, de uitgifte van OTC-tokens en gokken. Dit alles wordt gedaan in een verbluffend slecht ontworpen taal genaamd Solidity, waardoor de auteur van PHP vanuit academisch oogpunt op een genie lijkt. Vreemd genoeg lijkt de nieuwe taal van Facebook niets met deze technologieën te maken te hebben, aangezien het eigenlijk een scripttaal is die bedoeld is voor obscure bedrijfsdoeleinden.
In particuliere gedistribueerde grootboeken zijn slimme contracten een van die termen die door consultants worden rondgegooid zonder veel aandacht voor een duidelijke definitie of doel. Enterprise-softwareconsultants verdienen doorgaans geld aan dubbelzinnigheid, en slimme contracten zijn de apotheose van het obscurantisme van bedrijven, omdat ze letterlijk als alles kunnen worden gedefinieerd.
Nadat we beweringen hebben gedaan over de veiligheid ervan, moeten we naar de semantiek van de taal kijken. Correctheid in de programmeertaaltheorie bestaat doorgaans uit twee verschillende bewijzen: ‘vooruitgang’ en ‘behoud’, die de consistentie bepalen van de hele ruimte van evaluatieregels voor de taal. Meer specifiek is een functie in de typetheorie "lineair" als hij zijn argument precies één keer gebruikt, en "affien" als hij het hoogstens één keer gebruikt. Het lineaire typesysteem biedt een statische garantie dat een gedeclareerde lineaire functie werkelijk lineair is, door typen toe te wijzen aan alle functie-subexpressies en bij te houden waar aanroepen worden gedaan. Dit is een subtiele eigenschap om te bewijzen en is niet eenvoudig te implementeren voor een heel programma. Lineair typen is nog steeds een zeer academisch studiegebied, beïnvloed door de implementatie van type-uniciteit in Clean en type-eigendom in Rust. Er zijn enkele voorlopige voorstellen voor het toevoegen van lineaire typen aan de Glasgow Haskell Compiler.
De verklaring van Move over het gebruik van lineaire typen lijkt sindsdien een ongegronde duik in de compiler . Voor zover men kan nagaan, citeert de whitepaper canonieke literatuur van Girard en Peirce, en er is niets vergelijkbaars in de feitelijke implementatie.
Bovendien verschijnt de formele semantiek van de zogenaamd veilige taal nergens in de implementatie of in het document. De taal is klein genoeg om een volledig bewijs van de correcte semantiek in Coq of Isabelle te vinden. In werkelijkheid is het heel goed mogelijk een end-to-end volledige conversiecompiler met bewijsoverdracht naar bytecode te implementeren met moderne tools die in het afgelopen decennium zijn uitgevonden. Wij weten hoe we het moeten doen, te beginnen met terug in 1996.
Vanuit het perspectief van de programmeertaaltheorie is het onmogelijk om de bewering dat Move een betrouwbare en veilige taal is te testen, aangezien deze beweringen neerkomen op puur handgebaar en marketing in plaats van daadwerkelijk bewijs. Dit is een alarmerende situatie voor een taalproject dat wordt gevraagd miljarden dollars aan transacties te verwerken.
Weegschaalcryptografie is gebrekkig
Het bouwen van veilige cryptosystemen is een zeer moeilijk technisch probleem, en het is altijd het beste om het werken met gevaarlijke code te benaderen met een flinke dosis gezonde paranoia. Er zijn grote doorbraken op dit gebied, zoals het Microsoft Everest-project, dat een verifieerbare beveiliging bouwt . Er bestaan al hulpmiddelen om verifieerbare primitieven te creëren. Hoewel dit duur is, valt het duidelijk niet buiten de economische mogelijkheden van Facebook. Het team besloot echter niet deel te nemen aan het project, dat werd aangekondigd als een betrouwbare basis voor het mondiale financiële systeem.
weegschaal project uit verschillende vrij nieuwe bibliotheken voor het creëren van experimentele cryptosystemen die pas de afgelopen jaren zijn verschenen. Het is onmogelijk om te zeggen of de afhankelijkheden van de volgende tools veilig zijn of niet, aangezien geen van deze bibliotheken is gecontroleerd en geen standaard openbaarmakingsbeleid heeft. Met name voor sommige kernbibliotheken bestaat er geen zekerheid over de bescherming tegen zijkanaalaanvallen en timingaanvallen.
De Libra-bibliotheek wordt nog experimenteler en gaat verder dan dat , waarbij zeer nieuwe technieken worden toegepast, zoals verifieerbare willekeurige functies (VRF's), bilineaire paren en drempelsignaturen. Deze methoden en bibliotheken kunnen redelijk zijn, maar het combineren ervan in één systeem roept ernstige zorgen op over het aanvalsoppervlak. De combinatie van al deze nieuwe tools en technieken vergroot de complexiteit van het bewijzen van beveiliging aanzienlijk.
Er moet worden aangenomen dat deze hele cryptografische stapel kwetsbaar is voor verschillende aanvallen totdat het tegendeel is bewezen. Het beroemde 'Move Fast and Break Things'-model van Facebook kan niet worden toegepast op cryptografische tools die financiële gegevens van klanten verwerken.
Libra slaagt er niet in mechanismen voor consumentenbescherming te implementeren
Een onderscheidend kenmerk van het betalingssysteem is de mogelijkheid om een transactie terug te draaien als de betaling wordt geannuleerd door een rechtszaak of leidt tot een accidentele of systeemfout. Het Libra-systeem is ontworpen om "compleet" te zijn en bevat geen transactietype voor het annuleren van betalingen. In Groot-Brittannië zijn alle betalingen tussen £100 en £30,000 onderworpen aan de Consumer Credit Act. Dit betekent dat het betalingssysteem de verantwoordelijkheid deelt met de verkoper in geval van een probleem met het gekochte product of als de ontvanger van de betaling de dienst niet levert. Soortgelijke regels gelden in de EU, Azië en Noord-Amerika.
Het huidige ontwerp van Libra bevat geen protocol om aan deze wetten te voldoen en er is geen duidelijk plan om er een te creëren. Erger nog, vanuit architectonisch perspectief staat de finaliteit van de geauthenticeerde datastructuur van de kernel, gebaseerd op de staat van de Merkle-drive, geen enkel mechanisme toe om een dergelijk protocol te creëren zonder de kernel opnieuw te ontwerpen.
Na een technische beoordeling van dit project te hebben uitgevoerd, kunnen we concluderen dat het eenvoudigweg niet door een gerespecteerd tijdschrift voor gedistribueerd systeemonderzoek of financiële engineering zal komen. Om te proberen het mondiale monetaire beleid te veranderen, moet er enorm veel technisch werk worden gedaan om een betrouwbaar netwerk en een veilige verwerking van gebruikersgegevens te creëren waarop het publiek en de toezichthouders kunnen vertrouwen.
Ik zie geen reden om aan te nemen dat Facebook het nodige werk heeft gedaan in zijn ontwerp om deze technische problemen te overwinnen of dat het enige technische voordelen heeft ten opzichte van de huidige infrastructuur. Zeggen dat een bedrijf flexibiliteit in de regelgeving nodig heeft om innovaties te onderzoeken, is geen excuus om ze niet eerst te doen.
Bron: www.habr.com