Dopo due anni sono tornato sul blog per un post diverso dalle solite noiose lezioni su Haskell e la matematica. Negli ultimi anni ho lavorato sul fintech nell'UE e mi sembra un buon momento per scrivere su un argomento che ha ricevuto poca attenzione da parte dei media tecnologici.
Facebook ha recentemente rilasciato quella che definisce una “nuova piattaforma di servizi finanziari” chiamata Libra. È posizionato come un sistema di regolamento digitale basato su un paniere di valute internazionali gestite su una “blockchain” e archiviate in un pool di denaro gestito dalla Svizzera. Gli obiettivi del progetto sono ambiziosi e comportano conseguenze geopolitiche su larga scala.
В и Molti articoli sensati sulle infondate ipotesi monetarie ed economiche alla base del sistema finanziario proposto. Ma non ci sono abbastanza specialisti capaci di analizzare dal punto di vista tecnico. Non sono molte le persone che lavorano su infrastrutture finanziarie e parlano pubblicamente del proprio lavoro, quindi questo progetto non ottiene molta copertura nei media tecnologici, sebbene le sue viscere siano aperte al mondo. Intendo open source nei repository и .
Ciò che è aperto al mondo è un artefatto architettonicamente schizofrenico che pretende di essere una piattaforma sicura per l’infrastruttura di pagamento globale.
Se ti immergi nel codice base, l'effettiva implementazione del sistema diverge completamente dall'obiettivo dichiarato e nei modi più bizzarri. Sono sicuro che questo progetto abbia una storia aziendale interessante. Quindi è logico presumere che sia stato progettato con una certa diligenza, ma in realtà vedo una serie davvero strana di decisioni architetturali che rompono l'intero sistema e mettono a rischio gli utenti.
Non pretenderò di avere un'opinione obiettiva su Facebook come azienda. Poche persone nel settore IT la guardano con simpatia. Ma un confronto tra le sue dichiarazioni e il codice pubblicato mostra chiaramente che lo scopo dichiarato è fondamentalmente ingannevole. In breve, questo progetto non dà potere a nessuno. Rimarrà interamente sotto il controllo di una società la cui attività pubblicitaria è così impantanata nello scandalo e nella corruzione che non ha altra scelta che cercare di diversificare i pagamenti e il credit scoring per sopravvivere. L'obiettivo chiaro a lungo termine è quello di agire come broker di dati e intermediario nell'accesso dei consumatori al credito in base ai loro dati personali sui social media. Questa è una storia assolutamente orribile e oscura che non riceve l'attenzione che merita.
L'unica cosa che salva questa storia è che l'artefatto che hanno creato è così esilarantemente inadatto al compito da svolgere che può essere visto solo come un atto di arroganza. Ci sono diversi errori architettonici importanti in questo progetto:
Risolvere il problema dei generali bizantini in una rete di controllo degli accessi è un progetto incoerente
Il problema dei generali bizantini è un'area piuttosto ristretta di ricerca sui sistemi distribuiti. Descrive la capacità di un sistema di rete di resistere a guasti casuali dei componenti intraprendendo azioni correttive critiche per il funzionamento del sistema. Una rete resiliente deve resistere a diversi tipi di attacchi, tra cui riavvii, interruzioni, carichi dannosi e votazioni dannose nelle elezioni della leadership. Questa è la decisione principale per l'architettura Libra, e qui è completamente priva di significato.
Il sovraccarico di complessità temporale di questa struttura aggiuntiva dipende dall'algoritmo. Esiste molta letteratura sulle varianti dei protocolli Paxos e Raft che risolvono il problema dei generali bizantini, ma tutte queste strutture introducono un sovraccarico aggiuntivo per la comunicazione su 
per mantenere il quorum. Per Libra hanno scelto un algoritmo con il costo di comunicazione più alto possibile in caso di fallimento della leadership. Inoltre, vi è un sovraccarico aggiuntivo derivante dalla potenziale rielezione dei leader in diversi tipi di eventi di guasto della rete.
Per un sistema che opera all’interno di un consorzio di multinazionali altamente regolamentate, in cui tutti gli utenti hanno un codice firmato da Facebook e l’accesso alla rete è controllato da Facebook, semplicemente non ha senso considerare i partecipanti malintenzionati a livello di consenso. Non è chiaro il motivo per cui questo sistema risolverebbe anche il problema dei generali bizantini, invece di limitarsi a mantenere una traccia di controllo coerente per verificarne la conformità. La possibilità che un nodo Libra gestito da Mastercard o Andressen Horrowitz inizi improvvisamente a eseguire codice dannoso è uno scenario strano da pianificare ed è meglio affrontarlo semplicemente garantendo l'integrità del protocollo e mezzi non tecnici (cioè legali).
La testimonianza del Congresso ha presentato il prodotto come concorrente dei nuovi protocolli di pagamento internazionali come WeChat, Alipay e M-Pesa. Tuttavia, nessuno di questi sistemi è progettato per funzionare su pool di validatori per risolvere il problema dei generali bizantini. Sono semplicemente progettati su un bus tradizionale a larghezza di banda elevata che effettua il cablaggio secondo un insieme di regole fisse. Questo è un approccio naturale alla progettazione di un sistema di pagamento. Ben progettato il sistema di pagamento semplicemente non incontrerà il problema della doppia spesa e dei fork.
Il sovraccarico dell’algoritmo di consenso non risolve alcun problema e limita solo il rendimento del sistema per nessun altro motivo se non il culto del carico della blockchain pubblica, che non è destinata a questo caso d’uso.
Libra non ha privacy sulle transazioni
Secondo la documentazione, il sistema è progettato tenendo conto pseudonimo, ovvero gli indirizzi utilizzati nel protocollo sono ottenuti da chiavi pubbliche su curve ellittiche e non contengono metadati sugli account. Tuttavia, da nessuna parte nella descrizione della struttura di governance dell’organizzazione o nel protocollo stesso viene indicato come i dati economici coinvolti nelle transazioni saranno nascosti ai validatori. Il sistema è progettato per replicare le transazioni su larga scala per una serie di soggetti esterni che, secondo le attuali leggi sul segreto bancario europeo e statunitense, non dovrebbero essere a conoscenza dei dettagli economici.
Le politiche sui dati tra paesi sono difficili da coordinare, soprattutto date le leggi e i regolamenti disparati nelle diverse giurisdizioni con diverse visioni culturali sulla protezione dei dati e sulla privacy. Il protocollo stesso è per impostazione predefinita completamente aperto ai membri del consorzio, il che rappresenta un evidente difetto tecnico che non soddisfa i requisiti per i quali è stato progettato.
Libra HotStuff BFT non è in grado di raggiungere il throughput richiesto per un sistema di pagamento
Nel Regno Unito, i sistemi di compensazione come BAC sono in grado di gestire circa 580 milioni di transazioni al mese. Allo stesso tempo, sistemi altamente ottimizzati come Visa possono elaborare 000 di transazioni al giorno. Le prestazioni variano a seconda delle dimensioni della transazione, del routing della rete, del carico del sistema e (antiriciclaggio, schemi di riciclaggio di denaro).
Libra sta cercando di risolvere problemi che non sono realmente problemi per i trasferimenti nazionali, poiché gli stati nazionali hanno modernizzato le loro infrastrutture di compensazione negli ultimi dieci anni. Per i consumatori al dettaglio nell’Unione Europea, spostare denaro non è affatto un problema. Nelle infrastrutture tradizionali questo può essere fatto in pochi secondi con uno smartphone standard. Per i trasferimenti aziendali di grandi dimensioni, esistono vari meccanismi e regole associati allo spostamento di grandi quantità di denaro.
Non vi è alcuna ragione tecnica per cui i pagamenti transfrontalieri non possano essere elaborati anche istantaneamente, a parte le differenze nelle regole e nei requisiti tra le giurisdizioni interessate. Se le necessarie misure preventive (adeguata verifica della clientela, controlli delle sanzioni, ecc.) vengono eseguite più volte in diverse fasi della catena della transazione, ciò potrebbe comportare un ritardo nella transazione. Tuttavia, questo ritardo è puramente una funzione della legislazione normativa e della conformità, non della tecnologia.
Per i consumatori, non vi è alcun motivo per cui una transazione nel Regno Unito non venga completata in pochi secondi. Le transazioni al dettaglio nell’UE stanno effettivamente rallentando (Conosci il tuo cliente) e restrizioni antiriciclaggio imposte da governi e autorità di regolamentazione, che si applicano allo stesso modo ai pagamenti Libra. Anche se Facebook dovesse superare gli ostacoli ai trasferimenti transfrontalieri e ai trasferimenti di dati privati, il modello proposto è lontano centinaia di anni-persona dal throughput delle transazioni globali e probabilmente dovrebbe essere riprogettato da zero.
La lingua di Libra Move non è corretta
Il white paper fa affermazioni audaci su un nuovo linguaggio non testato chiamato Move. Queste affermazioni sono piuttosto dubbie dal punto di vista della teoria del linguaggio di programmazione (PLT).
Move è un nuovo linguaggio di programmazione per implementare la logica delle transazioni personalizzate e i contratti intelligenti sulla blockchain di Libra. Poiché Libra mira un giorno a servire miliardi di persone, Move è progettato pensando alla sicurezza come priorità assoluta.
Una caratteristica chiave di Move è la capacità di definire tipi di risorse arbitrari con semantica ispirata alla logica lineare.
Nelle blockchain pubbliche, i contratti intelligenti affrontano la logica delle reti pubbliche con conti di deposito a garanzia, riciclaggio di denaro, emissione di token OTC e gioco d’azzardo. Tutto questo viene fatto in un linguaggio sorprendentemente mal progettato chiamato Solidity, che da un punto di vista accademico fa sembrare l'autore di PHP un genio. Stranamente, il nuovo linguaggio di Facebook sembra non avere nulla a che fare con queste tecnologie, poiché in realtà è un linguaggio di scripting destinato a oscuri scopi aziendali.
Nei registri distribuiti privati, i contratti intelligenti sono uno di quei termini lanciati dai consulenti senza molto riguardo per una definizione o uno scopo chiaro. I consulenti di software aziendale in genere guadagnano dall’ambiguità e i contratti intelligenti sono l’apoteosi dell’oscurantismo aziendale perché possono essere definiti letteralmente come qualsiasi cosa.
Dopo aver fatto affermazioni sulla sua sicurezza, dobbiamo esaminare la semantica del linguaggio. La correttezza nella teoria dei linguaggi di programmazione consiste tipicamente in due diverse prove: “progresso” e “conservazione”, che determinano la coerenza dell'intero spazio delle regole di valutazione del linguaggio. Più specificamente, nella teoria dei tipi, una funzione è "lineare" se usa il suo argomento esattamente una volta, e "affine" se lo usa al massimo una volta. Il sistema di tipi lineari fornisce la garanzia statica che una funzione lineare dichiarata sia veramente lineare assegnando tipi a tutte le sottoespressioni di funzioni e tenendo traccia di dove vengono effettuate le chiamate. Questa è una proprietà sottile da dimostrare e non è facile da implementare per un intero programma. La tipizzazione lineare è ancora un campo di studio molto accademico, influenzato dall'implementazione dell'unicità del tipo in Clean e della proprietà del tipo in Rust. Esistono alcune proposte preliminari per l'aggiunta di tipi lineari al compilatore Haskell di Glasgow.
L'affermazione di Move sull'uso dei tipi lineari sembra un tuffo ingiustificato nel compilatore, da lì . Per quanto si può dire, il whitepaper cita la letteratura canonica di Girard e Peirce, e non c'è nulla di simile nell'effettiva implementazione.
Inoltre, la semantica formale del linguaggio apparentemente sicuro non appare da nessuna parte nell'implementazione o nel documento. Il linguaggio è sufficientemente piccolo per trovare una prova completa della semantica corretta in Coq o Isabelle. In realtà, un compilatore di conversione completa end-to-end con trasferimento di prova in bytecode è del tutto possibile da implementare con strumenti moderni inventati nell'ultimo decennio. Sappiamo come farlo, a cominciare da nel 1996.
Dal punto di vista della teoria del linguaggio di programmazione, è impossibile verificare l’affermazione secondo cui Move è un linguaggio affidabile e sicuro, poiché queste affermazioni equivalgono a semplici gesti di marketing e di marketing piuttosto che a prove reali. Si tratta di una situazione allarmante per un progetto linguistico a cui viene chiesto di elaborare transazioni per miliardi di dollari.
La crittografia di Libra è difettosa
Costruire sistemi crittografici sicuri è un problema ingegneristico molto difficile ed è sempre meglio affrontare il lavoro con codice pericoloso con una buona dose di sana paranoia. Ci sono importanti progressi in questo settore, come il progetto Microsoft Everest, che sta costruendo un sistema sicuro e verificabile . Esistono già strumenti per creare primitive verificabili. Anche se questo è costoso, chiaramente non va oltre le capacità economiche di Facebook. Tuttavia, il team ha deciso di non partecipare al progetto, annunciato come una base affidabile per il sistema finanziario globale.
progetto bilancia da diverse librerie abbastanza nuove per la creazione di crittosistemi sperimentali apparsi solo negli ultimi anni. È impossibile dire se le dipendenze dai seguenti strumenti siano sicure o meno, poiché nessuna di queste biblioteche è stata controllata e non dispone di politiche di divulgazione standard. In particolare, per alcune librerie core non esiste certezza riguardo alla protezione contro attacchi side-channel e timing attack.
La libreria libra diventa ancora più sperimentale e va oltre , applicando tecniche molto nuove come funzioni casuali verificabili (VRF), coppie bilineari e firme di soglia. Questi metodi e librerie possono essere ragionevoli, ma combinarli tutti in un unico sistema solleva serie preoccupazioni sulla superficie di attacco. La combinazione di tutti questi nuovi strumenti e tecniche aumenta notevolmente la complessità della dimostrazione della sicurezza.
Si dovrebbe presumere che l’intero stack crittografico sia vulnerabile a vari attacchi fino a prova contraria. Il famoso modello "Move Fast and Break Things" di Facebook non può essere applicato agli strumenti crittografici che elaborano i dati finanziari dei clienti.
La Bilancia non riesce ad attuare meccanismi di protezione dei consumatori
Una caratteristica distintiva del sistema di pagamento è la capacità di ripristinare una transazione se il pagamento viene annullato a causa di una causa legale o porta a un guasto accidentale o al sistema. Il sistema Libra è progettato per essere “completo” e non prevede un tipo di transazione per l’annullamento del pagamento. Nel Regno Unito, tutti i pagamenti compresi tra £ 100 e £ 30,000 sono soggetti al Consumer Credit Act. Ciò significa che il sistema di pagamento condivide la responsabilità con il venditore in caso di problemi con il prodotto acquistato o se il destinatario del pagamento non fornisce il servizio. Regole simili si applicano nell’UE, in Asia e nel Nord America.
L’attuale progettazione di Libra non include un protocollo per conformarsi a queste leggi e non ha un piano chiaro per crearne uno. Ancor peggio, da un punto di vista architetturale, la finalità della struttura dati autenticata del kernel, basata sullo stato dell'unità Merkle, non consente alcun meccanismo per creare un protocollo del genere senza riprogettare il kernel.
Dopo aver condotto una revisione tecnica di questo progetto, possiamo concludere che semplicemente non supererà l'esame di nessuna rispettata rivista di ricerca sui sistemi distribuiti o di ingegneria finanziaria. Per provare a cambiare la politica monetaria globale, è necessario svolgere un’enorme quantità di lavoro tecnico per creare una rete affidabile e un’elaborazione sicura dei dati degli utenti di cui il pubblico e i regolatori possano fidarsi.
Non vedo alcun motivo per credere che Facebook abbia svolto il lavoro necessario nella sua progettazione per superare questi problemi tecnici o che presenti vantaggi tecnici rispetto all’attuale infrastruttura. Dire che un’azienda ha bisogno di flessibilità normativa per esplorare le innovazioni non è una scusa per non realizzarle prima.
Fonte: habr.com