Po dveh letih sem se vrnil na blog po objavo, ki se razlikuje od običajnih dolgočasnih predavanj o Haskellu in matematiki. Zadnjih nekaj let se ukvarjam s fintechom v EU in zdi se, da je prišel čas, da pišem o temi, ki ji tehnološki mediji posvečajo malo pozornosti.
Facebook je pred kratkim izdal tako imenovano "novo platformo za finančne storitve", imenovano Libra. Postavljen je kot digitalni poravnalni sistem, ki temelji na košarici mednarodnih valut, ki se upravljajo na "blockchainu" in so shranjene v denarnem skladu, ki se upravlja iz Švice. Cilji projekta so ambiciozni in prinašajo obsežne geopolitične posledice.
В и Veliko razumnih člankov o nezdravih monetarnih in ekonomskih predpostavkah, ki stojijo za predlaganim finančnim sistemom. Toda strokovnjakov, ki bi bili sposobni analize s tehničnega vidika, je premalo. Ni veliko ljudi, ki se ukvarjajo s finančno infrastrukturo in javno govorijo o svojem delu, zato ta projekt nima veliko pokritosti v tehnoloških medijih, čeprav je njegova notranjost odprta svetu. Mislim na odprto kodo v repozitorijih и .
Kar je odprto svetu, je arhitekturno shizofren artefakt, ki trdi, da je varna platforma za globalno plačilno infrastrukturo.
Če se poglobite v bazo kode, se dejanska izvedba sistema popolnoma oddaljuje od zastavljenega cilja in to na najbolj bizarne načine. Prepričan sem, da ima ta projekt zanimivo korporativno zgodovino. Zato je logično domnevati, da je bil zasnovan z nekaj skrbnosti, toda v resnici vidim res nenavaden nabor arhitekturnih odločitev, ki porušijo celoten sistem in ogrožajo uporabnike.
Ne bom se pretvarjal, da imam objektivno mnenje o Facebooku kot podjetju. Malokdo v IT industriji nanjo gleda s simpatijo. Toda primerjava njegovih izjav in objavljene kode jasno kaže, da je navedeni namen v osnovi zavajajoč. Skratka, ta projekt nikogar ne opolnomoči. Ostal bo v celoti pod nadzorom podjetja, katerega oglaševalski posel je tako zatopljen v škandale in korupcijo, da mu ne preostane drugega, kot da poskuša diverzificirati svoja plačila in kreditno točkovanje, da bi preživelo. Jasen dolgoročni cilj je delovati kot posrednik podatkov in posrednik pri dostopu potrošnikov do kreditov na podlagi njihovih osebnih podatkov v družbenih medijih. To je popolnoma grozljiva in temačna zgodba, ki ne dobi pozornosti, ki si jo zasluži.
Edina rešitev te zgodbe je, da je artefakt, ki so ga ustvarili, tako smešno neprimeren za zastavljeno nalogo, da ga lahko razumemo le kot dejanje prevzetnosti. V tem projektu je več večjih arhitekturnih napak:
Reševanje problema bizantinskih generalov v omrežju za nadzor dostopa je nedosledna zasnova
Problem bizantinskih generalov je precej ozko področje raziskovanja porazdeljenih sistemov. Opisuje zmožnost omrežnega sistema, da prenese naključne okvare komponent, medtem ko izvaja korektivne ukrepe, ki so ključni za delovanje sistema. Odporno omrežje mora prenesti več vrst napadov, vključno s ponovnimi zagoni, izpadi, zlonamernimi nalaganji in zlonamernim glasovanjem na volitvah vodstva. To je glavna odločitev za arhitekturo Libra in je popolnoma nesmiselna.
Stroški časovne kompleksnosti te dodatne strukture so odvisni od algoritma. Obstaja veliko literature o različicah protokolov Paxos in Raft, ki rešujejo problem bizantinskih generalov, vendar vse te strukture uvajajo dodatne stroške za komunikacijo prek 
ohraniti sklepčnost. Za Libro so izbrali algoritem z najvišjimi možnimi komunikacijskimi stroški v primeru neuspeha vodstva. Poleg tega obstajajo dodatni stroški zaradi morebitne ponovne izvolitve vodij v več vrstah dogodkov okvar omrežja.
Za sistem, ki deluje znotraj konzorcija visoko reguliranih multinacionalnih korporacij, kjer imajo vsi uporabniki kodo, podpisano s strani Facebooka, dostop do omrežja pa nadzira Facebook, preprosto ni smiselno obravnavati zlonamernih udeležencev na ravni konsenza. Ni jasno, zakaj bi ta sistem sploh rešil problem bizantinskih generalov, namesto da bi preprosto vzdrževal dosledno revizijsko sled za preverjanje skladnosti. Možnost, da vozlišče Libra, ki ga vodita Mastercard ali Andressen Horrowitz, nenadoma začne izvajati zlonamerno kodo, je nenavaden scenarij, ki ga je treba načrtovati in ga je bolje obravnavati s preprostim zagotavljanjem integritete protokola in netehničnimi (tj. pravnimi) sredstvi.
Pričevanje kongresu je izdelek označilo kot konkurenta novim mednarodnim plačilnim protokolom, kot so WeChat, Alipay in M-Pesa. Vendar nobeden od teh sistemov ni zasnovan tako, da bi deloval na bazenih validatorjev za rešitev problema bizantinskih generalov. Preprosto so zasnovani na tradicionalnem vodilu z visoko pasovno širino, ki omogoča ožičenje v skladu s fiksnim nizom pravil. To je naraven pristop k oblikovanju plačilnega sistema. Dobro oblikovana plačilni sistem preprosto ne bo naletel na problem dvojne porabe in vilic.
Stroški konsenznega algoritma ne rešijo nobene težave in samo omejuje prepustnost sistema brez drugega razloga kot tovornega kulta javne verige blokov, ki ni namenjen temu primeru uporabe.
Libra nima zasebnosti transakcij
Glede na dokumentacijo je sistem zasnovan ob upoštevanju psevdonimnost, to pomeni, da so naslovi, uporabljeni v protokolu, pridobljeni iz javnih ključev na eliptičnih krivuljah in ne vsebujejo metapodatkov o računih. Vendar nikjer v opisu strukture upravljanja za organizacijo ali v samem protokolu ni navedeno, kako bodo ekonomski podatki, vključeni v transakcije, skriti pred validatorji. Sistem je zasnovan za posnemanje transakcij v velikem obsegu za vrsto zunanjih strank, ki v skladu z veljavno zakonodajo o bančni tajnosti v Evropi in ZDA ne bi smele biti seznanjene z ekonomskimi podrobnostmi.
Podatkovne politike med državami je težko uskladiti, zlasti glede na različne zakone in predpise v različnih jurisdikcijah z različnimi kulturnimi pogledi na varstvo podatkov in zasebnost. Sam protokol je privzeto popolnoma odprt za člane konzorcija, kar je očitna tehnična pomanjkljivost, ki ne izpolnjuje zahtev, za katere je zasnovan.
Libra HotStuff BFT ne more doseči prepustnosti, potrebne za plačilni sistem
V Združenem kraljestvu klirinški sistemi, kot je BAC, zmorejo obdelati približno 580 transakcij na mesec. Hkrati lahko visoko optimizirani sistemi, kot je Visa, obdelajo 000 transakcij na dan. Zmogljivost se razlikuje glede na velikost transakcije, omrežno usmerjanje, obremenitev sistema in (preprečevanje pranja denarja, sheme pranja denarja).
Tehtnica poskuša rešiti težave, ki v resnici niso težave za domače prenose, saj so nacionalne države v zadnjem desetletju posodobile svojo klirinško infrastrukturo. Za maloprodajne potrošnike v Evropski uniji prenos denarja sploh ni problem. Na tradicionalni infrastrukturi je to mogoče storiti s standardnim pametnim telefonom v nekaj sekundah. Za prenose velikih podjetij obstajajo različni mehanizmi in pravila, povezana s premikanjem velikih količin denarja.
Ni tehničnega razloga, zakaj tudi čezmejnih plačil ni mogoče obdelati takoj, razen razlik v pravilih in zahtevah med ustreznimi jurisdikcijami. Če se potrebni preventivni ukrepi (pregled stranke, pregledi sankcij itd.) izvedejo večkrat na različnih stopnjah transakcijske verige, lahko to povzroči zamudo pri transakciji. Vendar je ta zamuda zgolj posledica regulativne zakonodaje in skladnosti, ne pa tehnologije.
Za potrošnike ni razloga, zakaj transakcija v Združenem kraljestvu ne bi bila opravljena v nekaj sekundah. Maloprodajne transakcije v EU se res upočasnjujejo (Know Your Customer) in omejitve proti pranju denarja, ki jih nalagajo vlade in regulatorji, ki veljajo enako za plačila Libra. Tudi če bi Facebook premagal ovire za čezmejne prenose in prenose zasebnih podatkov, je predlagani model na stotine osebnih let oddaljen od globalnega pretoka transakcij in bi ga bilo verjetno treba preoblikovati iz nič.
Jezik Libra Move ni pravilen
Bela knjiga vsebuje drzne trditve o novem, nepreizkušenem jeziku, imenovanem Move. Te trditve so precej dvomljive z vidika teorije programskega jezika (PLT).
Move je nov programski jezik za implementacijo transakcijske logike po meri in pametnih pogodb v blokovni verigi Libra. Ker želi Libra nekega dne služiti milijardam ljudi, je Move zasnovan tako, da je varnost glavna prioriteta.
Ključna značilnost Move je zmožnost definiranja poljubnih tipov virov s semantiko, ki se zgleduje po linearni logiki.
V javnih verigah blokov se pametne pogodbe soočajo z logiko javnih omrežij z depozitnimi računi, pranjem denarja, izdajo žetonov OTC in igrami na srečo. Vse to je narejeno v osupljivo slabo zasnovanem jeziku, imenovanem Solidity, zaradi katerega je z akademskega vidika avtor PHP videti kot genij. Nenavadno je, da se zdi, da nov jezik iz Facebooka nima nobene zveze s temi tehnologijami, saj je pravzaprav skriptni jezik, namenjen nejasnim poslovnim namenom.
V zasebnih porazdeljenih knjigah so pametne pogodbe eden tistih izrazov, ki jih svetovalci razmetavajo brez posebnega upoštevanja jasne definicije ali namena. Svetovalci za podjetniško programsko opremo običajno zaslužijo z dvoumnostjo, pametne pogodbe pa so apoteoza korporativnega obskurantizma, ker jih je mogoče definirati kot dobesedno karkoli.
Po trditvah o njegovi varnosti si moramo ogledati semantiko jezika. Pravilnost v teoriji programskega jezika je običajno sestavljena iz dveh različnih dokazov: »napredek« in »ohranjanje«, ki določata skladnost celotnega prostora pravil vrednotenja za jezik. Natančneje, v teoriji tipov je funkcija "linearna", če svoj argument uporabi točno enkrat, in "afina", če ga uporabi največ enkrat. Sistem linearnih tipov zagotavlja statično jamstvo, da je deklarirana linearna funkcija resnično linearna, tako da dodeljuje tipe vsem podizrazom funkcij in spremlja, kje so opravljeni klici. To je subtilna lastnost, ki jo je treba dokazati in je ni lahko implementirati za celoten program. Linearno tipkanje je še vedno zelo akademsko področje študija, na katerega vplivata implementacija edinstvenosti tipa v Clean in lastništvo tipa v Rust. Obstaja nekaj predhodnih predlogov za dodajanje linearnih tipov prevajalniku Glasgow Haskell.
Izjava Move o uporabi linearnih tipov se zdi kot neupravičen potop v prevajalnik, saj tam . Kolikor lahko razberemo, bela knjiga navaja kanonično literaturo Girarda in Peircea in v dejanski izvedbi ni nič podobnega.
Poleg tega se formalna semantika domnevno varnega jezika ne pojavi nikjer niti v izvedbi niti v dokumentu. Jezik je dovolj majhen, da bi našli popoln dokaz pravilne semantike v Coq ali Isabelle. V resnici je prevajalnik popolne pretvorbe od konca do konca s prenosom dokazov v bajtno kodo povsem mogoče implementirati s sodobnimi orodji, izumljenimi v zadnjem desetletju. Vemo, kako to storiti, začenši z že leta 1996.
Z vidika teorije programskega jezika je nemogoče preizkusiti trditev, da je Move zanesljiv in varen jezik, saj te trditve pomenijo čisto mahanje z roko in trženje in ne dejanski dokazi. To je alarmantna situacija za jezikovni projekt, od katerega se zahteva, da obdela milijarde dolarjev transakcij.
Kriptografija Libra je pomanjkljiva
Gradnja varnih kriptosistemov je zelo težak inženirski problem in vedno je najbolje, da se dela z nevarno kodo lotite z dobro dozo zdrave paranoje. Na tem področju so veliki preboji, kot je projekt Microsoft Everest, ki gradi preverljivo varno . Orodja za ustvarjanje preverljivih primitivov že obstajajo. Čeprav je to drago, očitno ne presega gospodarskih zmožnosti Facebooka. Vendar se je ekipa odločila, da ne bo sodelovala pri projektu, ki je bil napovedan kot zanesljiv temelj svetovnega finančnega sistema.
projekt libra iz več precej novih knjižnic za ustvarjanje eksperimentalnih kriptosistemov, ki so se pojavile šele v zadnjih nekaj letih. Nemogoče je reči, ali so odvisnosti od naslednjih orodij varne ali ne, saj nobena od teh knjižnic ni bila revidirana in nimajo standardnih politik razkritja. Zlasti za nekatere osnovne knjižnice ni gotovosti glede zaščite pred napadi stranskih kanalov in napadi na časovno razporeditev.
Knjižnica Libra postane še bolj eksperimentalna in presega , ki uporablja zelo nove tehnike, kot so preverljive naključne funkcije (VRF), bilinearni pari in podpisi pragov. Te metode in knjižnice so morda razumne, vendar združevanje vseh v en sistem povzroča resne pomisleke glede površine napada. Kombinacija vseh teh novih orodij in tehnik močno poveča kompleksnost dokazovanja varnosti.
Domnevati je treba, da je ta celoten kriptografski sklad ranljiv za različne napade, dokler se ne dokaže nasprotno. Znanega Facebookovega modela 'Hitro premikaj in zlomi stvari' ni mogoče uporabiti za kriptografska orodja, ki obdelujejo finančne podatke strank.
Libra ne izvaja mehanizmov za zaščito potrošnikov
Posebnost plačilnega sistema je zmožnost razveljavitve transakcije, če je plačilo preklicano s tožbo ali povzroči nenamerno ali sistemsko napako. Sistem Libra je zasnovan tako, da je "popoln" in ne vključuje vrste transakcije za preklic plačila. V Združenem kraljestvu za vsa plačila med £100 in £30,000 velja Zakon o potrošniških kreditih. To pomeni, da plačilni sistem deli odgovornost s prodajalcem v primeru težav s kupljenim izdelkom ali če prejemnik plačila ne opravi storitve. Podobna pravila veljajo v EU, Aziji in Severni Ameriki.
Trenutna zasnova Libre ne vključuje protokola za izpolnjevanje teh zakonov in nima jasnega načrta za njegovo ustvarjanje. Še huje, z arhitekturnega vidika, dokončnost overjene podatkovne strukture jedra, ki temelji na stanju pogona Merkle, ne dovoljuje nobenega mehanizma za ustvarjanje takšnega protokola brez preoblikovanja jedra.
Po opravljenem tehničnem pregledu tega projekta lahko sklepamo, da preprosto ne bo prestal ocene v nobeni ugledni reviji o raziskavah porazdeljenih sistemov ali finančnem inženiringu. Da bi poskusili spremeniti globalno denarno politiko, je treba opraviti ogromno tehničnega dela, da bi ustvarili zanesljivo omrežje in varno obdelavo uporabniških podatkov, ki jim lahko zaupajo javnost in regulatorji.
Ne vidim razloga, da bi verjel, da je Facebook opravil potrebno delo pri svoji zasnovi za premagovanje teh tehničnih težav ali da ima kakršne koli tehnične prednosti pred trenutno infrastrukturo. Reči, da podjetje potrebuje regulativno prožnost za raziskovanje inovacij, ni izgovor, da jih ne naredi prvo.
Vir: www.habr.com