Po dvoch rokoch som sa na blog vrátil pre príspevok, ktorý sa líši od bežných nudných prednášok o Haskellovi a matematike. V posledných rokoch som pracoval na fintech v EÚ a zdá sa, že nastal čas napísať o téme, ktorej technické médiá venovali len malú pozornosť.
Facebook nedávno vydal to, čo nazýva „novou platformou finančných služieb“ s názvom Libra. Je umiestnený ako digitálny zúčtovací systém založený na koši medzinárodných mien, ktoré sú spravované na „blockchaine“ a uložené v peňažnom fonde spravovanom zo Švajčiarska. Ciele projektu sú ambiciózne a prinášajú rozsiahle geopolitické dôsledky.
В и Veľa rozumných článkov o nesprávnych menových a ekonomických predpokladoch za navrhovaným finančným systémom. Nie je však dostatok odborníkov schopných analyzovať z technického hľadiska. Nie veľa ľudí pracuje na finančnej infraštruktúre a verejne hovorí o svojej práci, takže tento projekt nemá v technických médiách veľa pozornosti, hoci jeho vnútro je otvorené svetu. Myslím open source v repozitároch и .
To, čo je otvorené svetu, je architektonicky schizofrenický artefakt s tvrdeniami, že je bezpečnou platformou pre globálnu platobnú infraštruktúru.
Ak sa ponoríte do kódovej základne, skutočná implementácia systému sa úplne odkloní od stanoveného cieľa, a to tými najbizarnejšími spôsobmi. Som si istý, že tento projekt má zaujímavú firemnú históriu. Je teda logické predpokladať, že to bolo navrhnuté s určitou starostlivosťou, ale v skutočnosti vidím naozaj zvláštny súbor architektonických rozhodnutí, ktoré narúšajú celý systém a ohrozujú používateľov.
Nebudem predstierať, že mám o Facebooku ako spoločnosti objektívny názor. Len málokto z IT branže sa na ňu pozerá so sympatiami. Ale porovnanie jeho tvrdení a zverejneného kódexu jasne ukazuje, že uvedený účel je v zásade klamlivý. Tento projekt skrátka nikoho nezmocňuje. Zostane úplne pod kontrolou spoločnosti, ktorej reklamný biznis je tak zaplavený škandálmi a korupciou, že nemá inú možnosť, ako sa pokúsiť diverzifikovať svoje platby a úverové hodnotenie, aby prežila. Jasným dlhodobým cieľom je pôsobiť ako sprostredkovateľ údajov a sprostredkovateľ v prístupe spotrebiteľov k úveru na základe ich osobných údajov na sociálnych sieťach. Toto je absolútne hrozný a temný príbeh, ktorému sa nedostáva takej pozornosti, akú by si zaslúžil.
Jedinou záchranou tohto príbehu je, že artefakt, ktorý vytvorili, je tak veselo nevhodný na danú úlohu, že ho možno vnímať iba ako akt arogancie. V tomto projekte je niekoľko hlavných architektonických chýb:
Riešenie problému byzantských generálov v sieti kontroly prístupu je nekonzistentný návrh
Problém byzantských generálov je pomerne úzka oblasť výskumu distribuovaných systémov. Popisuje schopnosť sieťového systému odolávať náhodným zlyhaniam komponentov a zároveň vykonávať nápravné opatrenia, ktoré sú dôležité pre fungovanie systému. Odolná sieť musí odolať niekoľkým typom útokov, vrátane reštartov, výpadkov, škodlivého zaťaženia a zlomyseľného hlasovania vo voľbách vedenia. Toto je hlavné rozhodnutie pre architektúru Libra a tu je úplne zbytočné.
Časová zložitosť tejto dodatočnej štruktúry závisí od algoritmu. Existuje veľa literatúry o variantoch protokolov Paxos a Raft, ktoré riešia problém byzantských generálov, ale všetky tieto štruktúry predstavujú dodatočné náklady na komunikáciu. 
zachovať kvórum. Pre Váhy zvolili algoritmus s najvyššími možnými nákladmi na komunikáciu v prípade zlyhania vedenia. A existuje ďalšia réžia z potenciálneho opätovného zvolenia lídrov v rámci viacerých typov udalostí zlyhania siete.
Pre systém fungujúci v rámci konzorcia vysoko regulovaných nadnárodných korporácií, kde všetci používatelia majú kód podpísaný Facebookom a prístup do siete kontroluje Facebook, jednoducho nemá zmysel uvažovať o zlomyseľných účastníkoch na úrovni konsenzu. Nie je jasné, prečo by tento systém dokonca vyriešil problém byzantských generálov namiesto toho, aby jednoducho udržiaval konzistentný audit trail na kontrolu súladu. Možnosť, že uzol Váh prevádzkovaný spoločnosťou Mastercard alebo Andressen Horrowitz náhle spustí škodlivý kód, je zvláštny scenár, ktorý treba plánovať, a je lepšie ho riešiť jednoduchým zabezpečením integrity protokolu a netechnickými (t. j. legálnymi) prostriedkami.
Svedectvo Kongresu označilo produkt za konkurenta novým medzinárodným platobným protokolom, ako sú WeChat, Alipay a M-Pesa. Žiadny z týchto systémov však nie je navrhnutý tak, aby bežal na validátorových fondoch, aby sa vyriešil problém byzantských generálov. Sú jednoducho navrhnuté na tradičnej širokopásmovej zbernici, ktorá robí zapojenie podľa pevného súboru pravidiel. Ide o prirodzený prístup k návrhu platobného systému. Dobre navrhnuté platobný systém jednoducho nenarazí na problém dvojitého míňania a forkov.
Réžia konsenzuálneho algoritmu nerieši žiadny problém a iba obmedzuje priepustnosť systému z iného dôvodu, ako je kult nákladu verejného blockchainu, ktorý nie je určený pre tento prípad použitia.
Váhy nemajú žiadne transakčné súkromie
Podľa dokumentácie je systém navrhnutý s prihliadnutím pseudonymita, to znamená, že adresy použité v protokole sú získané z verejných kľúčov na eliptických krivkách a neobsahujú metadáta o účtoch. Nikde v popise štruktúry riadenia pre organizáciu ani v samotnom protokole sa však neuvádza, ako budú ekonomické údaje zahrnuté v transakciách skryté pred validátormi. Systém je navrhnutý tak, aby replikoval transakcie vo veľkom rozsahu pre celý rad externých strán, ktoré by podľa existujúcich európskych a amerických zákonov o bankovom tajomstve nemali byť zasvätené do ekonomických podrobností.
Dátové politiky v jednotlivých krajinách je ťažké koordinovať, najmä vzhľadom na rozdielne zákony a nariadenia v rôznych jurisdikciách s rôznymi kultúrnymi názormi na ochranu údajov a súkromia. Samotný protokol je štandardne úplne otvorený pre členov konzorcia, čo je jasný technický nedostatok, ktorý nespĺňa požiadavky, pre ktoré je navrhnutý.
Libra HotStuff BFT nedokáže dosiahnuť priepustnosť potrebnú pre platobný systém
Vo Veľkej Británii sú zúčtovacie systémy ako BAC schopné spracovať približne 580 000 000 transakcií za mesiac. Zároveň vysoko optimalizované systémy ako Visa dokážu spracovať 150 000 000 transakcií denne. Výkon sa líši v závislosti od veľkosti transakcie, smerovania siete, zaťaženia systému a (proti praniu špinavých peňazí, schémy proti praniu špinavých peňazí).
Váhy sa snažia riešiť problémy, ktoré v skutočnosti nie sú problémami domácich transferov, keďže národné štáty v poslednom desaťročí modernizovali svoju zúčtovaciu infraštruktúru. Pre maloobchodných spotrebiteľov v Európskej únii nie je presúvanie peňazí žiadnym problémom. Na tradičnej infraštruktúre sa to dá urobiť so štandardným smartfónom v priebehu niekoľkých sekúnd. Pre veľké korporátne prevody existujú rôzne mechanizmy a pravidlá spojené s presunom veľkého množstva peňazí.
Neexistuje žiadny technický dôvod, prečo nemožno okamžite spracovať aj cezhraničné platby, okrem rozdielov v pravidlách a požiadavkách medzi príslušnými jurisdikciami. Ak sa potrebné preventívne opatrenia (povinná starostlivosť o zákazníka, kontroly sankcií atď.) vykonajú viackrát v rôznych fázach reťazca transakcií, môže to viesť k oneskoreniu transakcie. Toto oneskorenie je však čisto funkciou regulačných právnych predpisov a súladu, nie technológie.
Pre spotrebiteľov neexistuje žiadny dôvod, prečo by transakcia v Spojenom kráľovstve nebola zúčtovaná v priebehu niekoľkých sekúnd. Maloobchodné transakcie v EÚ sa skutočne spomaľujú (Know Your Customer) a AML obmedzenia uložené vládami a regulačnými orgánmi, ktoré sa vzťahujú rovnako na platby Libra. Aj keby Facebook prekonal prekážky pri cezhraničných prenosoch a prenosoch súkromných údajov, navrhovaný model je vzdialený stovky osobo-rokov od globálnej priepustnosti transakcií a pravdepodobne by bolo potrebné ho prepracovať od nuly.
Jazyk Libra Move je nesprávny
Biela kniha uvádza odvážne tvrdenia o novom, netestovanom jazyku s názvom Move. Tieto tvrdenia sú z pohľadu teórie programovacích jazykov (PLT) dosť pochybné.
Move je nový programovací jazyk na implementáciu vlastnej transakčnej logiky a inteligentných zmlúv na blockchaine Libra. Keďže cieľom Libra je jedného dňa slúžiť miliardám ľudí, Move je navrhnutý s bezpečnosťou ako najvyššou prioritou.
Kľúčovou vlastnosťou Move je schopnosť definovať ľubovoľné typy zdrojov so sémantikou inšpirovanou lineárnou logikou.
Vo verejných blockchainoch čelia inteligentné zmluvy logike verejných sietí s úschovnými účtami, praním špinavých peňazí, vydávaním OTC tokenov a hazardnými hrami. To všetko sa deje v úžasne zle navrhnutom jazyku s názvom Solidity, vďaka čomu z akademického hľadiska vyzerá autor PHP ako génius. Napodiv sa zdá, že nový jazyk od Facebooku nemá s týmito technológiami nič spoločné, keďže ide v skutočnosti o skriptovací jazyk určený na nejasné podnikové účely.
V súkromných distribuovaných účtovných knihách sú inteligentné zmluvy jedným z pojmov, ktoré konzultanti používajú bez veľkého zreteľa na jasnú definíciu alebo účel. Konzultanti podnikového softvéru zvyčajne zarábajú na nejednoznačnosti a inteligentné zmluvy sú apoteózou podnikového tmárstva, pretože ich možno definovať doslova ako čokoľvek.
Po tvrdeniach o jeho bezpečnosti sa musíme pozrieť na sémantiku jazyka. Správnosť v teórii programovacieho jazyka zvyčajne pozostáva z dvoch rôznych dôkazov: „pokrok“ a „zachovanie“, ktoré určujú konzistenciu celého priestoru pravidiel hodnotenia jazyka. Presnejšie povedané, v teórii typov je funkcia „lineárna“, ak použije svoj argument presne raz, a „afinná“, ak ho použije najviac raz. Systém lineárneho typu poskytuje statickú záruku, že deklarovaná lineárna funkcia je skutočne lineárna priradením typov všetkým podvýrazom funkcií a sledovaním toho, kde sa volania uskutočňujú. Toto je jemná vlastnosť, ktorú treba dokázať a nie je ľahké ju implementovať pre celý program. Lineárne písanie je stále veľmi akademická oblasť štúdia, ovplyvnená implementáciou typovej jedinečnosti v Clean a vlastníctvom typu v Rust. Existuje niekoľko predbežných návrhov na pridanie lineárnych typov do kompilátora Glasgow Haskell.
Vyhlásenie Move o používaní lineárnych typov vyzerá ako neoprávnené ponorenie sa do kompilátora, pretože tam je . Pokiaľ možno povedať, biela kniha cituje kanonickú literatúru od Girarda a Peircea a v skutočnej implementácii nič podobné nie je.
Navyše, formálna sémantika údajne bezpečného jazyka sa nikde neobjavuje ani v implementácii, ani v dokumente. Jazyk je dostatočne malý na to, aby našiel úplný dôkaz správnej sémantiky v Coq alebo Isabelle. V skutočnosti je celkom možné implementovať úplný kompilátor konverzie s dôkazovým prenosom do bajtkódu pomocou moderných nástrojov vynájdených v poslednom desaťročí. Vieme, ako na to, počnúc ešte v roku 1996.
Z hľadiska teórie programovacieho jazyka nie je možné otestovať tvrdenie, že Move je spoľahlivý a bezpečný jazyk, pretože tieto tvrdenia predstavujú skôr čisté mávnutie rukou a marketing než skutočné dôkazy. Toto je alarmujúca situácia pre jazykový projekt, ktorý je požiadaný o spracovanie transakcií v hodnote miliárd dolárov.
Kryptografia Váhy je chybná
Budovanie bezpečných kryptosystémov je veľmi náročný inžiniersky problém a vždy je najlepšie pristupovať k práci s nebezpečným kódom s poriadnou dávkou zdravej paranoje. V tejto oblasti došlo k veľkým prelomom, ako napríklad projekt Microsoft Everest, ktorý vytvára overiteľné zabezpečenie . Nástroje na vytváranie overiteľných primitív už existujú. Hoci je to drahé, zjavne to nie je nad ekonomické možnosti Facebooku. Tím sa však rozhodol nezúčastniť sa projektu, ktorý bol vyhlásený za spoľahlivý základ pre globálny finančný systém.
projekt libra z niekoľkých celkom nových knižníc na vytváranie experimentálnych kryptosystémov, ktoré sa objavili len v posledných rokoch. Nie je možné povedať, či sú závislosti na nasledujúcich nástrojoch bezpečné alebo nie, pretože žiadna z týchto knižníc nebola kontrolovaná a nemá štandardné zásady zverejňovania. Najmä v prípade niektorých základných knižníc neexistuje žiadna istota týkajúca sa ochrany proti útokom z bočného kanála a útokom načasovania.
Knižnica libra sa stáva ešte experimentálnejšou a ide ďalej použitím veľmi nových techník, ako sú overiteľné náhodné funkcie (VRF), bilineárne páry a prahové podpisy. Tieto metódy a knižnice môžu byť rozumné, ale ich kombinovanie do jedného systému vyvoláva vážne obavy z oblasti povrchu útoku. Kombinácia všetkých týchto nových nástrojov a techník výrazne zvyšuje zložitosť preukazovania bezpečnosti.
Malo by sa predpokladať, že celý tento kryptografický zásobník je zraniteľný voči rôznym útokom, kým sa nepreukáže opak. Slávny model Facebooku „Pohybujte sa rýchlo a rozbite veci“ nemožno použiť na kryptografické nástroje, ktoré spracúvajú finančné údaje zákazníkov.
Váham sa nedarí implementovať mechanizmy na ochranu spotrebiteľa
Charakteristickým rysom platobného systému je schopnosť vrátiť transakciu späť, ak je platba zrušená súdnym sporom alebo vedie k náhodnému alebo systémovému zlyhaniu. Systém Libra je navrhnutý ako „kompletný“ a neobsahuje typ transakcie na zrušenie platby. V Spojenom kráľovstve všetky platby medzi 100 a 30,000 XNUMX £ podliehajú zákonu o spotrebiteľských úveroch. To znamená, že platobný systém zdieľa zodpovednosť s predajcom v prípade problému so zakúpeným produktom alebo ak príjemca platby neposkytne službu. Podobné pravidlá platia v EÚ, Ázii a Severnej Amerike.
Súčasný dizajn Váh nezahŕňa protokol na dodržiavanie týchto zákonov a nemá jasný plán na jeho vytvorenie. Ešte horšie je, že z architektonického hľadiska konečnosť overenej dátovej štruktúry jadra, založená na stave disku Merkle, neumožňuje žiadnemu mechanizmu vytvoriť takýto protokol bez prepracovania jadra.
Po vykonaní technickej kontroly tohto projektu môžeme konštatovať, že jednoducho neprejde v žiadnom uznávanom časopise o výskume distribuovaných systémov alebo v časopise finančného inžinierstva. Aby sme sa pokúsili zmeniť globálnu menovú politiku, je potrebné vykonať obrovské množstvo technickej práce na vytvorenie spoľahlivej siete a bezpečného spracovania používateľských údajov, ktorým môže verejnosť a regulačné orgány dôverovať.
Nevidím dôvod domnievať sa, že Facebook urobil potrebnú prácu vo svojom dizajne, aby prekonal tieto technické problémy, alebo že má nejaké technické výhody oproti súčasnej infraštruktúre. Povedať, že spoločnosť potrebuje regulačnú flexibilitu, aby preskúmala inovácie, nie je ospravedlnením, že ich neurobí ako prvé.
Zdroj: hab.com