Etter to år kom jeg tilbake til bloggen for et innlegg som skiller seg fra de vanlige kjedelige forelesningene om Haskell og matematikk. Jeg har jobbet med fintech i EU de siste årene, og det virker som tiden er inne for å skrive om et tema som har fått lite oppmerksomhet fra teknologimediene.
Facebook lanserte nylig det de kaller en "ny plattform for finansielle tjenester" kalt Libra. Det er posisjonert som et digitalt oppgjørssystem basert på en kurv av internasjonale valutaer som administreres på en "blokkjede" og lagres i en pengepool administrert fra Sveits. Målene for prosjektet er ambisiøse og medfører store geopolitiske konsekvenser.
В и Mange fornuftige artikler om de usunde monetære og økonomiske forutsetningene bak det foreslåtte finanssystemet. Men det er ikke nok spesialister som er i stand til å analysere fra et teknisk synspunkt. Det er ikke mange som jobber med finansiell infrastruktur og snakker offentlig om arbeidet sitt, så dette prosjektet får ikke mye omtale i teknologimediene, selv om dets innerste er åpent for verden. Jeg mener åpen kildekode i repositories и .
Det som er åpent for verden er en arkitektonisk schizofren artefakt som hevder å være en sikker plattform for den globale betalingsinfrastrukturen.
Hvis du dykker ned i kodebasen, avviker selve implementeringen av systemet fullstendig fra det uttalte målet, og på de mest bisarre måter. Jeg er sikker på at dette prosjektet har en interessant bedriftshistorie. Så det er logisk å anta at det ble designet med en viss flid, men i virkeligheten ser jeg et veldig merkelig sett med arkitektoniske beslutninger som bryter hele systemet og setter brukere i fare.
Jeg skal ikke late som jeg har en objektiv mening om Facebook som selskap. De færreste i IT-bransjen ser på henne med sympati. Men en sammenligning av uttalelsene og den publiserte koden viser tydelig at det uttalte formålet er grunnleggende villedende. Kort sagt, dette prosjektet styrker ingen. Han vil forbli fullstendig under kontroll av et selskap hvis reklamevirksomhet er så fast i skandale og korrupsjon at det ikke har noe annet valg enn å prøve å diversifisere sine betalinger og kredittscoring for å overleve. Det klare langsiktige målet er å fungere som datamegler og mellommann i forbrukernes tilgang til kreditt basert på deres personlige sosiale mediedata. Dette er en helt forferdelig og mørk historie som ikke får den oppmerksomheten den fortjener.
Den eneste frelsende nåden ved denne historien er at artefakten de skapte er så morsomt uegnet for oppgaven at den bare kan sees på som en hybrishandling. Det er flere store arkitektoniske feil i dette prosjektet:
Å løse det bysantinske generalproblemet i et tilgangskontrollnettverk er et inkonsekvent design
Problemet med de bysantinske generalene er et ganske smalt område for forskning av distribuerte systemer. Den beskriver evnen til et nettverkssystem til å motstå tilfeldige komponentfeil mens det iverksettes korrigerende tiltak som er kritiske for driften av systemet. Et motstandsdyktig nettverk må tåle flere typer angrep, inkludert omstart, driftsstans, ondsinnet belastning og ondsinnet stemmegivning i ledervalg. Dette er hovedavgjørelsen for Libra-arkitekturen, og det er helt meningsløst her.
Tidskompleksiteten til denne tilleggsstrukturen avhenger av algoritmen. Det finnes mye litteratur om varianter av Paxos- og Raft-protokollene som løser det bysantinske generalproblemet, men alle disse strukturene introduserer ekstra overhead for kommunikasjon over 
for å opprettholde beslutningsdyktighet. For Libra valgte de en algoritme med høyest mulig kommunikasjonskostnad ved svikt i ledelsen. Og det er ekstra overhead fra potensielle gjenvalg av ledere på tvers av flere typer nettverksfeilhendelser.
For et system som opererer innenfor et konsortium av høyt regulerte multinasjonale selskaper, der alle brukere har kode signert av Facebook og tilgang til nettverket kontrolleres av Facebook, gir det rett og slett ikke mening å vurdere ondsinnede deltakere på konsensusnivå. Det er ikke klart hvorfor dette systemet til og med ville løse problemet med bysantinske generaler, i stedet for bare å opprettholde et konsistent revisjonsspor for å kontrollere samsvar. Muligheten for at en Libra-node drevet av Mastercard eller Andressen Horrowitz plutselig begynner å kjøre ondsinnet kode er et merkelig scenario å planlegge for og løses bedre ved ganske enkelt å sikre protokollintegritet og ikke-tekniske (dvs. juridiske) midler.
Vitnesbyrd til kongressen fakturerte produktet som en konkurrent til nye internasjonale betalingsprotokoller som WeChat, Alipay og M-Pesa. Imidlertid er ingen av disse systemene designet for å kjøre på validatorpooler for å løse det bysantinske generalproblemet. De er ganske enkelt designet på en tradisjonell buss med høy båndbredde som lager ledninger i henhold til et fast sett med regler. Dette er en naturlig tilnærming til å designe et betalingssystem. Godt designet betalingssystemet vil rett og slett ikke støte på problemet med doble utgifter og gafler.
Overheaden til konsensusalgoritmen løser ikke noe problem og begrenser bare gjennomstrømningen til systemet uten andre grunner enn lastekulten til den offentlige blokkjeden, som ikke er ment for denne brukssaken.
Libra har ikke noe personvern for transaksjoner
I følge dokumentasjonen er systemet utformet med hensyn til pseudonymitet, det vil si at adressene som brukes i protokollen hentes fra offentlige nøkler på elliptiske kurver og inneholder ikke metadata om kontoer. Imidlertid, ingen steder i beskrivelsen av styringsstrukturen for organisasjonen eller i selve protokollen indikerer det hvordan de økonomiske dataene som er involvert i transaksjoner vil bli skjult for validatorer. Systemet er utformet for å replikere transaksjoner i stor skala til en rekke eksterne parter som i henhold til eksisterende europeiske og amerikanske lover om bankhemmeligheter ikke bør være kjent med de økonomiske detaljene.
Datapolitikk på tvers av land er vanskelig å koordinere, spesielt gitt ulike lover og forskrifter i ulike jurisdiksjoner med ulike kulturelle syn på databeskyttelse og personvern. Selve protokollen er som standard helt åpen for konsortiemedlemmer, noe som er en klar teknisk mangel som ikke oppfyller kravene den er designet for.
Libra HotStuff BFT klarer ikke å oppnå gjennomstrømmingen som kreves for et betalingssystem
I Storbritannia er clearingsystemer som BAC i stand til å håndtere rundt 580 000 000 transaksjoner per måned. Samtidig kan svært optimaliserte systemer som Visa behandle 150 000 000 transaksjoner per dag. Ytelsen varierer avhengig av transaksjonsstørrelse, nettverksruting, systembelastning og (anti-hvitvasking, hvitvaskingsordninger).
Libra prøver å løse problemer som egentlig ikke er problemer for innenlandske overføringer, ettersom nasjonalstater har modernisert sin clearing-infrastruktur det siste tiåret. For detaljbrukere i EU er det ikke noe problem å flytte penger i det hele tatt. På tradisjonell infrastruktur kan dette gjøres med en standard smarttelefon på sekunder. For store bedriftsoverføringer er det ulike mekanismer og regler knyttet til flytting av store pengebeløp.
Det er ingen teknisk grunn til at grenseoverskridende betalinger ikke også kan behandles umiddelbart, annet enn forskjeller i regler og krav mellom de relevante jurisdiksjonene. Dersom nødvendige forebyggende tiltak (kundevurdering, sanksjonskontroller etc.) utføres flere ganger på ulike stadier av transaksjonskjeden, kan dette føre til forsinkelse i transaksjonen. Imidlertid er denne forsinkelsen utelukkende en funksjon av regulatorisk lovgivning og samsvar, ikke teknologi.
For forbrukere er det ingen grunn til at en britisk transaksjon ikke ville bli klart i løpet av sekunder. Detaljhandelstransaksjoner i EU avtar faktisk (Kjen din kunde) og AML-restriksjoner pålagt av myndigheter og regulatorer, som gjelder like mye for Libra-betalinger. Selv om Facebook skulle overvinne hindringene for grenseoverskridende overføringer og private dataoverføringer, er den foreslåtte modellen hundrevis av personår unna global transaksjonsgjennomstrømning og vil sannsynligvis måtte redesignes fra bunnen av.
Libra Move-språket er feil
Hvitboken kommer med dristige påstander om et nytt, uprøvd språk kalt Move. Disse utsagnene er ganske tvilsomme fra et synspunkt av programmeringsspråkteori (PLT).
Move er et nytt programmeringsspråk for implementering av tilpasset transaksjonslogikk og smarte kontrakter på Libra blockchain. Fordi Libra har som mål å en dag betjene milliarder av mennesker, er Move designet med sikkerhet som en topp prioritet.
En nøkkelfunksjon ved Move er muligheten til å definere vilkårlige ressurstyper med semantikk inspirert av lineær logikk.
I offentlige blokkjeder møter smarte kontrakter logikken til offentlige nettverk med deponeringskontoer, hvitvasking av penger, utstedelse av OTC-tokener og gambling. Alt dette er gjort i et forbløffende dårlig designet språk kalt Solidity, som fra et akademisk synspunkt får forfatteren av PHP til å se ut som et geni. Merkelig nok ser det nye språket fra Facebook ut til å ikke ha noe med disse teknologiene å gjøre, siden det faktisk er et skriptspråk beregnet på obskure bedriftsformål.
I private distribuerte hovedbøker er smarte kontrakter et av disse begrepene som konsulenter kaster rundt uten mye hensyn til klar definisjon eller formål. Konsulenter for bedriftsprogramvare tjener vanligvis penger på tvetydighet, og smarte kontrakter er apoteosen til bedriftens obskurantisme fordi de kan defineres som bokstavelig talt hva som helst.
Etter å ha kommet med påstander om sikkerheten, må vi se på språkets semantikk. Korrekthet i programmeringsspråkteori består typisk av to forskjellige bevis: «fremgang» og «bevaring», som bestemmer konsistensen av hele rommet med evalueringsreglene for språket. Mer spesifikt, i typeteori, er en funksjon "lineær" hvis den bruker argumentet nøyaktig én gang, og "affin" hvis den bruker det maksimalt én gang. Det lineære typesystemet gir statisk garanti for at en erklært lineær funksjon virkelig er lineær ved å tilordne typer til alle funksjonsunderuttrykk og holde styr på hvor anrop gjøres. Dette er en subtil egenskap å bevise og er ikke lett å implementere for et helt program. Lineær typing er fortsatt et svært akademisk fagfelt, påvirket av implementeringen av typeunikk i Clean og typeeierskap i Rust. Det er noen foreløpige forslag for å legge til lineære typer til Glasgow Haskell Compiler.
Moves uttalelse om bruk av lineære typer virker som et uberettiget dykk inn i kompilatoren, siden det . Så vidt man kan se, siterer whitepaper kanonisk litteratur fra Girard og Peirce, og det er ikke noe lignende i selve implementeringen.
I tillegg vises den formelle semantikken til det antatt sikre språket ingen steder i verken implementeringen eller dokumentet. Språket er lite nok til å finne et fullstendig bevis på korrekt semantikk i Coq eller Isabelle. I virkeligheten er en ende-til-ende kompilator for full konvertering med bevisoverføring til bytekode fullt mulig å implementere med moderne verktøy oppfunnet i det siste tiåret. Vi vet hvordan vi gjør det, fra og med tilbake i 1996.
Fra et programmeringsspråkteoretisk perspektiv er det umulig å teste påstanden om at Move er et pålitelig og sikkert språk, siden disse påstandene utgjør ren håndvifting og markedsføring i stedet for faktiske bevis. Dette er en alarmerende situasjon for et språkprosjekt som blir bedt om å behandle milliarder av dollar med transaksjoner.
Vektens kryptografi er feil
Å bygge sikre kryptosystemer er et svært vanskelig ingeniørproblem, og det er alltid best å nærme seg arbeid med farlig kode med en god dose sunn paranoia. Det er store gjennombrudd på dette området, som Microsoft Everest-prosjektet, som bygger en verifiserbar sikker . Det finnes allerede verktøy for å lage verifiserbare primitiver. Selv om dette er dyrt, er det tydeligvis ikke utenfor Facebooks økonomiske muligheter. Imidlertid bestemte teamet seg for ikke å delta i prosjektet, som ble annonsert som et pålitelig grunnlag for det globale finansielle systemet.
Libra-prosjektet fra flere ganske nye biblioteker for å lage eksperimentelle kryptosystemer som først har dukket opp de siste årene. Det er umulig å si om avhengighetene til følgende verktøy er trygge eller ikke, siden ingen av disse bibliotekene har blitt revidert og ikke har standard retningslinjer for offentliggjøring. Spesielt for noen kjernebibliotek er det ingen sikkerhet angående beskyttelse mot sidekanalangrep og timingangrep.
Biblioteket blir enda mer eksperimentelt og går utover , ved å bruke helt nye teknikker som verifiserbare tilfeldige funksjoner (VRF), bilineære par og terskelsignaturer. Disse metodene og bibliotekene kan være rimelige, men å kombinere dem alle i ett system gir alvorlige bekymringer for angrepsoverflaten. Kombinasjonen av alle disse nye verktøyene og teknikkene øker kompleksiteten i å bevise sikkerhet.
Det bør antas at hele denne kryptografiske stabelen er sårbar for ulike angrep inntil det motsatte er bevist. Facebooks berømte "Move Fast and Break Things"-modell kan ikke brukes på kryptografiske verktøy som behandler kundedata.
Libra klarer ikke å implementere forbrukerbeskyttelsesmekanismer
Et særtrekk ved betalingssystemet er muligheten til å rulle tilbake en transaksjon hvis betalingen kanselleres av et søksmål eller fører til en utilsiktet feil eller systemfeil. Libra-systemet er designet for å være "fullstendig" og inkluderer ikke en transaksjonstype for kansellering av betaling. I Storbritannia er alle betalinger mellom £100 og £30,000 XNUMX underlagt Consumer Credit Act. Dette betyr at betalingssystemet deler ansvaret med selgeren ved problem med det kjøpte produktet eller dersom mottakeren av betalingen ikke yter tjenesten. Lignende regler gjelder i EU, Asia og Nord-Amerika.
Den nåværende utformingen av Libra inkluderer ikke en protokoll for å overholde disse lovene og har ikke en klar plan for å lage en. Enda verre, fra et arkitektonisk perspektiv, tillater ikke endeligheten av kjernens autentiserte datastruktur, basert på tilstanden til Merkle-stasjonen, noen mekanisme for å lage en slik protokoll uten å redesigne kjernen.
Etter å ha utført en teknisk gjennomgang av dette prosjektet, kan vi konkludere med at det rett og slett ikke vil bestå i noen respektert distribuert systemforskning eller finansteknisk tidsskrift. For å prøve å endre den globale pengepolitikken, må det gjøres en enorm mengde teknisk arbeid for å skape et pålitelig nettverk og sikker behandling av brukerdata som publikum og regulatorer kan stole på.
Jeg ser ingen grunn til å tro at Facebook har gjort det nødvendige arbeidet i designet for å overvinne disse tekniske problemene eller at det har noen tekniske fordeler i forhold til dagens infrastruktur. Å si at et selskap trenger regulatorisk fleksibilitet for å utforske innovasjoner er ikke en unnskyldning for ikke å gjøre dem først.
Kilde: www.habr.com