Két év után visszatértem a blogra egy bejegyzésért, amely eltér a Haskellről és a matematikáról szóló szokásos unalmas előadásoktól. Az elmúlt néhány évben a fintech-en dolgozom az EU-ban, és úgy tűnik, eljött az idő, hogy egy olyan témáról írjak, amely kevés figyelmet kapott a technológiai médiától.
A Facebook a közelmúltban kiadta a Libra nevű „új pénzügyi szolgáltatási platformot”. Digitális elszámolási rendszerként helyezkedik el, amely nemzetközi valutakosáron alapul, amelyeket egy „blokkláncon” kezelnek, és egy Svájcból kezelt pénzkészletben tárolnak. A projekt céljai ambiciózusak és nagyszabású geopolitikai következményekkel járnak.
В и Sok értelmes cikk a javasolt pénzügyi rendszer mögött meghúzódó megalapozatlan monetáris és gazdasági feltételezésekről. De nincs elég szakember, aki képes lenne technikai szempontból elemezni. Kevesen dolgoznak a pénzügyi infrastruktúrán, és nem beszélnek nyilvánosan a munkájukról, így ez a projekt nem kap sok tudósítást a technológiai médiában, bár a bensősége nyitott a világ felé. A nyílt forráskódra gondolok a tárolókban и .
Ami nyitva áll a világ előtt, az egy építészetileg skizofrén műalkotás, amely azt állítja, hogy biztonságos platform a globális fizetési infrastruktúra számára.
Ha belemerülünk a kódbázisba, a rendszer tényleges megvalósítása teljesen eltér a kitűzött céltól, méghozzá a legfurcsább módon. Biztos vagyok benne, hogy ennek a projektnek érdekes vállalati története van. Logikus tehát azt feltételezni, hogy némi gondossággal tervezték, de a valóságban nagyon furcsa építészeti döntések halmazát látom, amelyek az egész rendszert megbontják és a felhasználókat veszélyeztetik.
Nem fogok úgy tenni, mintha objektív véleményem lenne a Facebookról mint cégről. Az IT-iparban kevesen néznek rá együttérzéssel. Ám az állítások és a közzétett kód összehasonlítása egyértelműen azt mutatja, hogy a kinyilvánított cél alapvetően megtévesztő. Röviden, ez a projekt senkit nem hatalmaz fel. Teljes mértékben egy olyan cég irányítása alatt marad, amelynek reklámtevékenysége annyira belemerült a botrányokba és a korrupcióba, hogy nincs más választása, mint diverzifikálni a fizetéseket és a hitelezést a túlélés érdekében. Az egyértelmű hosszú távú cél, hogy adatközvetítőként és közvetítőként működjenek a fogyasztók hitelhez jutásában személyes közösségi média adataik alapján. Ez egy teljesen szörnyű és sötét történet, amely nem kapja meg a megérdemelt figyelmet.
A történet egyetlen üdvözítő ereje az, hogy az általuk készített műtárgy olyan mulatságosan alkalmatlan az adott feladatra, hogy csak egy hübrisznek tekinthető. Számos jelentős építészeti hiba van ebben a projektben:
A bizánci tábornokok problémájának megoldása egy hozzáférés-vezérlő hálózatban következetlen terv
A bizánci tábornokok problémája az elosztott rendszerek kutatásának meglehetősen szűk területe. Leírja a hálózati rendszer azon képességét, hogy ellenálljon a véletlenszerű alkatrészek meghibásodásának, miközben a rendszer működése szempontjából kritikus korrekciós intézkedéseket hajt végre. A rugalmas hálózatnak többféle támadásnak is ellenállnia kell, beleértve az újraindításokat, kimaradásokat, rosszindulatú betöltéseket és rosszindulatú szavazást a vezetői választásokon. Ez a Libra architektúra fő döntése, és teljesen értelmetlen.
Ennek a kiegészítő struktúrának az időbonyolultsága az algoritmustól függ. Sok irodalom létezik a Paxos és a Raft protokollok bizánci tábornokok problémáját megoldó változatairól, de ezek a struktúrák többletköltséget jelentenek a kommunikációhoz. 
a határozatképesség fenntartása érdekében. A Libra számára a lehető legmagasabb kommunikációs költségű algoritmust választották a vezetés kudarca esetén. És további többletköltséget jelent a vezetők esetleges újraválasztása többféle hálózati hiba esetén.
Egy erősen szabályozott multinacionális vállalatok konzorciumán belül működő rendszer esetében, ahol minden felhasználó rendelkezik a Facebook által aláírt kóddal, és a hálózathoz való hozzáférést a Facebook ellenőrzi, egyszerűen nincs értelme konszenzus szinten figyelembe venni a rosszindulatú résztvevőket. Nem világos, hogy ez a rendszer miért oldaná meg a bizánci tábornokok problémáját, ahelyett, hogy egyszerűen konzisztens ellenőrzési nyomvonalat tartana fenn a megfelelés ellenőrzésére. Az a lehetőség, hogy a Mastercard vagy Andressen Horrowitz által üzemeltetett Libra csomópont hirtelen rosszindulatú kódot kezd futtatni, egy furcsa forgatókönyv, amelyet meg kell tervezni, és jobban kezelhető a protokoll integritásának és nem technikai (azaz jogi) eszközökkel.
A Kongresszusnak adott tanúvallomás szerint a termék az új nemzetközi fizetési protokollok, például a WeChat, az Alipay és az M-Pesa versenytársa. Azonban ezeknek a rendszereknek egyikét sem úgy tervezték, hogy ellenőrző készleteken fussanak a bizánci tábornokok problémájának megoldására. Egyszerűen egy hagyományos nagy sávszélességű buszra tervezték, amely rögzített szabályok szerint végzi a vezetékezést. Ez a fizetési rendszer tervezésének természetes megközelítése. Jól kidolgozott a fizetési rendszer egyszerűen nem fog szembesülni a dupla költés és a villák problémájával.
A konszenzusos algoritmus többletterhelése nem old meg semmilyen problémát, és csak korlátozza a rendszer áteresztőképességét, csak a nyilvános blokklánc rakománykultusza miatt, amely nem erre a felhasználási esetre készült.
A Mérleg nem rendelkezik tranzakciós adatvédelemmel
A dokumentáció szerint a rendszer kialakítása a figyelembe vétellel történik álnév, azaz a protokollban használt címek nyilvános kulcsokból származnak elliptikus görbéken, és nem tartalmaznak metaadatokat a fiókokról. Azonban a szervezet irányítási struktúrájának leírásában vagy magában a protokollban sehol nem utal arra, hogy a tranzakciókban érintett gazdasági adatok hogyan lesznek elrejtve az érvényesítők elől. A rendszert úgy tervezték, hogy nagy léptékben reprodukálja a tranzakciókat számos külső fél számára, akiknek a meglévő európai és amerikai banktitokra vonatkozó törvények értelmében nem szabad megismerniük a gazdasági részleteket.
Az egyes országok adatpolitikáit nehéz összehangolni, különösen, ha a különböző joghatóságok eltérő törvényei és szabályozásai eltérőek az adatvédelemről és a magánéletről szóló eltérő kulturális nézetekkel. Maga a protokoll alapértelmezés szerint teljesen nyitott a konzorciumi tagok előtt, ami egyértelmű technikai hiányosság, amely nem felel meg azoknak a követelményeknek, amelyekre tervezték.
A Libra HotStuff BFT nem tudja elérni a fizetési rendszerhez szükséges átviteli sebességet
Az Egyesült Királyságban az olyan elszámolási rendszerek, mint a BAC, körülbelül 580 000 000 tranzakció kezelésére képesek havonta. Ugyanakkor az olyan magasan optimalizált rendszerek, mint a Visa, napi 150 000 000 tranzakciót tudnak feldolgozni. A teljesítmény a tranzakció méretétől, a hálózati útválasztástól, a rendszerterheléstől és a rendszerterheléstől függően változik (pénzmosás elleni küzdelem, pénzmosási rendszerek).
A Mérleg olyan problémákat próbál megoldani, amelyek a belföldi átutalások esetében nem igazán jelentenek problémát, mivel a nemzetállamok az elmúlt évtizedben modernizálták elszámolási infrastruktúrájukat. Az Európai Unió lakossági fogyasztói számára a pénz mozgatása egyáltalán nem jelent problémát. A hagyományos infrastruktúrán ez egy szabványos okostelefonnal másodpercek alatt megtehető. A nagyvállalati átutalások esetében különféle mechanizmusok és szabályok vonatkoznak a nagy mennyiségű pénz mozgatására.
Nincs technikai oka annak, hogy a határokon átnyúló fizetéseket ne lehetne azonnal feldolgozni, kivéve az egyes joghatóságok közötti szabályok és követelmények eltéréseit. Ha a szükséges megelőző intézkedéseket (ügyfél-átvilágítás, szankcióellenőrzés stb.) a tranzakciós lánc különböző szakaszaiban többször elvégzik, az a tranzakció késését eredményezheti. Ez a késedelem azonban pusztán a szabályozási jogszabályok és a megfelelés függvénye, nem pedig a technológia.
A fogyasztók számára nincs ok arra, hogy az Egyesült Királyságban végrehajtott tranzakciók ne számolnának el pillanatok alatt. A kiskereskedelmi tranzakciók az EU-ban valóban lassulnak (Ismerje meg ügyfelét) és a kormányok és a szabályozó hatóságok által elrendelt AML korlátozások, amelyek a Libra-kifizetésekre is vonatkoznak. Még ha a Facebook le is küzdené a határokon átnyúló adatátvitel és a magánjellegű adattovábbítás akadályait, a javasolt modell több száz személyévnyire van a globális tranzakciós forgalomtól, és valószínűleg a semmiből kellene újratervezni.
A Libra Move nyelve helytelen
A fehér könyv merész állításokat fogalmaz meg egy új, még nem tesztelt Move nevű nyelvről. Ezek az állítások a programozási nyelvelmélet (PLT) szempontjából meglehetősen kétségesek.
A Move egy új programozási nyelv egyéni tranzakciós logika és intelligens szerződések megvalósításához a Libra blokkláncon. Mivel a Libra célja, hogy egy napon emberek milliárdjait szolgálja ki, a Move tervezésénél a biztonság az elsődleges szempont.
A Move egyik legfontosabb jellemzője, hogy tetszőleges erőforrástípusokat határozhat meg a lineáris logika által ihletett szemantikával.
A nyilvános blokkláncokban az intelligens szerződések szembesülnek a nyilvános hálózatok letéti számlákkal, pénzmosással, OTC token-kibocsátással és szerencsejátékokkal. Mindezt a Solidity elképesztően rosszul megtervezett nyelven teszik, ami akadémiai szempontból zseninek teszi a PHP szerzőjét. Furcsa módon úgy tűnik, hogy a Facebook új nyelvének semmi köze ezekhez a technológiákhoz, mivel valójában egy szkriptnyelvről van szó, amelyet homályos vállalati célokra szánnak.
Az elosztott magánkönyvekben az intelligens szerződések egyike azoknak a fogalmaknak, amelyeket a tanácsadók úgy dobnak fel, hogy nem veszik figyelembe a világos meghatározást vagy célt. A vállalati szoftver-tanácsadók általában a kétértelműségből keresnek pénzt, az intelligens szerződések pedig a vállalati obskurantizmus apoteózisa, mert szó szerint bármiként definiálhatók.
Miután állításokat tettünk a biztonságáról, meg kell vizsgálnunk a nyelv szemantikáját. A programnyelv-elmélet helyessége jellemzően két különböző bizonyítékból áll: a „haladásból” és a „megőrzésből”, amelyek meghatározzák a nyelv értékelési szabályainak teljes terének konzisztenciáját. Pontosabban, a típuselméletben egy függvény "lineáris", ha pontosan egyszer használja az argumentumát, és "affin", ha legfeljebb egyszer használja. A lineáris típusú rendszer statikus garanciát nyújt arra, hogy a deklarált lineáris függvény valóban lineáris, mivel minden függvény részkifejezéshez típusokat rendel, és nyomon követi a hívások helyét. Ez egy finom tulajdonság, amelyet bizonyítani kell, és nem könnyű megvalósítani egy egész programban. A lineáris gépelés még mindig nagyon akadémikus terület, amelyet a Clean-ban a típus-egyediség, a Rust-ban pedig a típustulajdonlás alkalmazása befolyásol. Van néhány előzetes javaslat a lineáris típusok hozzáadására a Glasgow Haskell fordítóhoz.
A Move lineáris típusok használatára vonatkozó kijelentése indokolatlan belemerülésnek tűnik a fordítóba, mivel . Amennyire meg lehet állapítani, a fehér könyv Girard és Peirce kanonikus irodalmát idézi, és a tényleges megvalósításban nincs semmi hasonló.
Ezenkívül a biztonságosnak vélt nyelv formális szemantikája sehol sem jelenik meg sem a megvalósításban, sem a dokumentumban. A nyelv elég kicsi ahhoz, hogy teljes bizonyítékot találjon a helyes szemantikára a Coqban vagy az Isabelle-ben. A valóságban egy bájtkódba való bizonyítási átvitellel rendelkező végpontok közötti teljes konverziós fordító teljesen megvalósítható az elmúlt évtizedben feltalált modern eszközökkel. Tudjuk, hogyan kell csinálni, kezdve még 1996-ban.
Programozási nyelvelméleti szempontból lehetetlen tesztelni azt az állítást, hogy a Move megbízható és biztonságos nyelv, mivel ezek az állítások inkább puszta kézlengetést és marketinget jelentenek, mintsem tényleges bizonyítékot. Ez egy riasztó helyzet egy nyelvi projekt számára, amelyet több milliárd dolláros tranzakció feldolgozására kérnek fel.
A Libra kriptográfia hibás
A biztonságos kriptorendszerek felépítése nagyon nehéz mérnöki probléma, és mindig a legjobb, ha egy jó adag egészséges paranoiával közelítjük meg a veszélyes kóddal való munkát. Jelentős áttörések vannak ezen a területen, mint például a Microsoft Everest projekt, amely egy ellenőrizhető biztonságos . Már léteznek eszközök ellenőrizhető primitívek létrehozására. Bár ez drága, nyilvánvalóan nem haladja meg a Facebook gazdasági lehetőségeit. A csapat azonban úgy döntött, hogy nem vesz részt a projektben, amelyet a globális pénzügyi rendszer megbízható alapjaként hirdettek meg.
libra projekt több, meglehetősen új könyvtárból kísérleti kriptorendszerek létrehozására, amelyek csak az elmúlt néhány évben jelentek meg. Lehetetlen megmondani, hogy a következő eszközöktől való függőségek biztonságosak-e vagy sem, mivel ezen könyvtárak egyikét sem auditálták, és nem rendelkeznek szabványos közzétételi szabályzattal. Különösen egyes alapvető könyvtárak esetében nincs bizonyosság az oldalcsatornás támadások és az időzítési támadások elleni védelem tekintetében.
A Libra könyvtár még kísérletezőbbé válik, és túlmutat , nagyon új technikákat alkalmaz, például ellenőrizhető véletlen függvényeket (VRF), bilineáris párokat és küszöb aláírásokat. Ezek a módszerek és könyvtárak ésszerűek lehetnek, de ezek egy rendszerben való egyesítése komoly aggályokat vet fel a támadási felülettel kapcsolatban. Mindezen új eszközök és technikák kombinációja nagymértékben megnöveli a biztonság bizonyításának összetettségét.
Feltételezhető, hogy ez az egész kriptográfiai verem sebezhető különféle támadásokkal szemben, amíg az ellenkezőjét be nem bizonyítják. A Facebook híres „Move Fast and Break Things” modellje nem alkalmazható az ügyfelek pénzügyi adatait feldolgozó kriptográfiai eszközökre.
A Libra nem alkalmazza a fogyasztóvédelmi mechanizmusokat
A fizetési rendszer megkülönböztető jellemzője a tranzakció visszaállításának lehetősége, ha a fizetést per törli, vagy az véletlen vagy a rendszer meghibásodásához vezet. A Libra rendszert "teljesre" tervezték, és nem tartalmaz tranzakciótípust a fizetés törlésére. Az Egyesült Királyságban minden 100 és 30,000 XNUMX GBP közötti fizetésre a fogyasztói hiteltörvény vonatkozik. Ez azt jelenti, hogy a fizetési rendszer megosztja a felelősséget az eladóval abban az esetben, ha a vásárolt termékkel probléma merül fel, vagy ha a fizetés címzettje nem nyújtja a szolgáltatást. Hasonló szabályok érvényesek az EU-ban, Ázsiában és Észak-Amerikában.
A Libra jelenlegi kialakítása nem tartalmaz protokollt, amely megfelel ezeknek a törvényeknek, és nincs egyértelmű terve egy ilyen létrehozására. Ami még rosszabb, építészeti szempontból a kernel hitelesített adatszerkezetének véglegessége a Merkle-meghajtó állapotán alapulva semmilyen mechanizmust nem tesz lehetővé egy ilyen protokoll létrehozására a kernel újratervezése nélkül.
Miután elvégeztük a projekt műszaki áttekintését, arra a következtetésre juthatunk, hogy egyszerűen nem megy át egyetlen elismert elosztott rendszerkutatási vagy pénzügyi tervezési folyóiratban sem. Ahhoz, hogy megpróbáljuk megváltoztatni a globális monetáris politikát, hatalmas technikai munkát kell végezni egy megbízható hálózat létrehozása és a felhasználói adatok biztonságos feldolgozása érdekében, amelyben a nyilvánosság és a szabályozók megbízhatnak.
Nem látok okot azt hinni, hogy a Facebook megtette a szükséges munkát a tervezés során, hogy megoldja ezeket a technikai problémákat, vagy hogy a jelenlegi infrastruktúrához képest bármilyen technikai előnye van. Ha azt mondjuk, hogy egy vállalatnak szabályozási rugalmasságra van szüksége ahhoz, hogy felfedezze az innovációkat, az nem mentség arra, hogy ne először csinálja meg azokat.
Forrás: will.com