Després de dos anys, vaig tornar al bloc per a una publicació diferent de les habituals conferències avorrides sobre Haskell i les matemàtiques. He estat treballant en fintech a la UE durant els últims anys i sembla que ha arribat el moment d'escriure sobre un tema que ha rebut poca atenció dels mitjans tecnològics.
Facebook va llançar recentment el que anomena una "nova plataforma de serveis financers" anomenada Libra. Es posiciona com un sistema de liquidació digital basat en una cistella de monedes internacionals que es gestionen en una "cadena de blocs" i s'emmagatzemen en un pool de diners gestionat des de Suïssa. Els objectius del projecte són ambiciosos i comporten conseqüències geopolítiques a gran escala.
В и Molts articles assenyats sobre els supòsits monetaris i econòmics poc sòlids darrere del sistema financer proposat. Però no hi ha prou especialistes capaços d'analitzar des d'un punt de vista tècnic. Poca gent treballa en infraestructures financeres i parla públicament de la seva feina, de manera que aquest projecte no té molta cobertura als mitjans tecnològics, tot i que les seves entranyes estan obertes al món. Em refereixo a codi obert als repositoris и .
El que està obert al món és un artefacte arquitectònicament esquizofrènic amb afirmacions de ser una plataforma segura per a la infraestructura de pagament global.
Si us submergiu en la base de codi, la implementació real del sistema divergeix completament de l'objectiu declarat i de les maneres més estranyes. Estic segur que aquest projecte té una història corporativa interessant. Per tant, és lògic suposar que s'ha dissenyat amb certa diligència, però en realitat veig un conjunt estrany de decisions arquitectòniques que trenquen tot el sistema i posen en risc els usuaris.
No pretendré tenir una opinió objectiva sobre Facebook com a empresa. Poca gent del sector informàtic la mira amb simpatia. Però una comparació de les seves declaracions i el codi publicat mostra clarament que el propòsit declarat és fonamentalment enganyós. En definitiva, aquest projecte no apodera ningú. Continuarà completament sota el control d'una empresa el negoci de la publicitat està tan embolicat en l'escàndol i la corrupció que no li queda més remei que intentar diversificar els seus pagaments i la puntuació creditícia per sobreviure. L'objectiu clar a llarg termini és actuar com a intermediari de dades i intermediari en l'accés dels consumidors al crèdit a partir de les seves dades personals de les xarxes socials. Aquesta és una història absolutament horrible i fosca que no rep l'atenció que es mereix.
L'única gràcia salvadora d'aquesta història és que l'artefacte que van crear és tan hilarantment inadequat per a la tasca en qüestió que només es pot veure com un acte d'hubris. Hi ha diversos errors arquitectònics importants en aquest projecte:
Resoldre el problema dels generals bizantins en una xarxa de control d'accés és un disseny inconsistent
El problema dels generals bizantins és una àrea més aviat estreta d'investigació dels sistemes distribuïts. Descriu la capacitat d'un sistema de xarxa per suportar fallades de components aleatòries mentre prenen accions correctives crítiques per al funcionament del sistema. Una xarxa resistent ha de suportar diversos tipus d'atacs, com ara reinicis, interrupcions, càrregues malicioses i vots maliciosos a les eleccions de lideratge. Aquesta és la decisió principal de l'arquitectura Libra, i aquí no té sentit.
La sobrecàrrega de complexitat temporal d'aquesta estructura addicional depèn de l'algorisme. Hi ha molta literatura sobre variants dels protocols Paxos i Raft que resolen el problema dels generals bizantins, però totes aquestes estructures introdueixen una sobrecàrrega addicional per a la comunicació. 
per mantenir el quòrum. Per a Libra, van triar un algorisme amb el cost de comunicació més alt possible en cas de fracàs del lideratge. I hi ha una sobrecàrrega addicional per la possible reelecció de líders en diversos tipus d'esdeveniments de fallada de la xarxa.
Per a un sistema que opera dins d'un consorci de corporacions multinacionals altament regulades, on tots els usuaris tenen codi signat per Facebook i l'accés a la xarxa està controlat per Facebook, simplement no té sentit considerar els participants maliciosos a nivell de consens. No està clar per què aquest sistema resoldria fins i tot el problema dels generals bizantins, en lloc de simplement mantenir una pista d'auditoria coherent per comprovar el compliment. La possibilitat que un node Libra executat per Mastercard o Andressen Horrowitz comenci sobtadament a executar codi maliciós és un escenari estrany per planificar i s'aborda millor simplement assegurant la integritat del protocol i mitjans no tècnics (és a dir, legals).
Testimoni al Congrés va facturar el producte com a competidor dels nous protocols de pagament internacionals com WeChat, Alipay i M-Pesa. Tanmateix, cap d'aquests sistemes està dissenyat per executar-se en grups de validadors per resoldre el problema dels generals bizantins. Simplement estan dissenyats en un bus tradicional d'ample de banda elevat que fa el cablejat segons un conjunt de regles fixes. Aquest és un enfocament natural per dissenyar un sistema de pagament. Ben dissenyat el sistema de pagament simplement no es trobarà amb el problema de la doble despesa i forks.
La sobrecàrrega de l'algoritme de consens no resol cap problema i només limita el rendiment del sistema sense cap altre motiu que el culte de càrrega de la cadena de blocs pública, que no està pensada per a aquest cas d'ús.
Libra no té privadesa de transaccions
Segons la documentació, el sistema està dissenyat tenint en compte pseudònim, és a dir, les adreces utilitzades en el protocol s'obtenen a partir de claus públiques en corbes el·líptiques i no contenen metadades sobre els comptes. Tanmateix, enlloc de la descripció de l'estructura de govern de l'organització o del propi protocol s'indica com s'ocultaran als validadors les dades econòmiques implicades en les transaccions. El sistema està dissenyat per replicar transaccions a gran escala a una sèrie de parts externes que, d'acord amb les lleis de secret bancari europees i nord-americanes existents, no haurien de conèixer els detalls econòmics.
Les polítiques de dades entre països són difícils de coordinar, sobretot tenint en compte les lleis i regulacions dispars en diferents jurisdiccions amb diferents visions culturals sobre la protecció de dades i la privadesa. El protocol en si està per defecte totalment obert als membres del consorci, la qual cosa és una clara mancança tècnica que no compleix els requisits per als quals està dissenyat.
Libra HotStuff BFT no pot aconseguir el rendiment necessari per a un sistema de pagament
Al Regne Unit, els sistemes de compensació com BAC són capaços de gestionar uns 580 milions de transaccions al mes. Al mateix temps, sistemes altament optimitzats com Visa poden processar 000 de transaccions per dia. El rendiment varia segons la mida de la transacció, l'encaminament de la xarxa, la càrrega del sistema i (antiblanqueig de capitals, esquemes de blanqueig de capitals).
Libra està intentant resoldre problemes que no són realment problemes per a les transferències nacionals, ja que els estats nacionals han modernitzat la seva infraestructura de neteja durant l'última dècada. Per als consumidors minoristes de la Unió Europea, moure diners no és cap problema. A la infraestructura tradicional, això es pot fer amb un telèfon intel·ligent estàndard en qüestió de segons. Per a grans transferències corporatives, hi ha diversos mecanismes i regles associades a moure grans quantitats de diners.
No hi ha cap motiu tècnic perquè els pagaments transfronterers també no es puguin processar a l'instant, excepte les diferències de normes i requisits entre les jurisdiccions corresponents. Si les mesures preventives necessàries (diligència deguda al client, controls de sancions, etc.) es realitzen diverses vegades en diferents etapes de la cadena de transaccions, això pot provocar un retard en la transacció. Tanmateix, aquest retard és purament una funció de la legislació reguladora i el compliment, no de la tecnologia.
Per als consumidors, no hi ha cap raó per la qual una transacció al Regne Unit no s'aclareixi en qüestió de segons. Les transaccions minoristes a la UE s'estan alentint (Coneix el teu client) i restriccions AML imposades pels governs i els reguladors, que s'apliquen per igual als pagaments de Libra. Fins i tot si Facebook superés les barreres a les transferències transfrontereres i les transferències privades de dades, el model proposat està a centenars d'anys-persona del rendiment global de transaccions i probablement s'hauria de redissenyar des de zero.
L'idioma de Libra Move és incorrecte
El llibre blanc fa afirmacions atrevides sobre un llenguatge nou i no provat anomenat Move. Aquestes afirmacions són força dubtoses des del punt de vista de la teoria del llenguatge de programació (PLT).
Move és un nou llenguatge de programació per implementar lògica de transaccions personalitzada i contractes intel·ligents a la cadena de blocs Libra. Com que Libra té com a objectiu servir un dia a milers de milions de persones, Move està dissenyat amb la seguretat com a màxima prioritat.
Una característica clau de Move és la capacitat de definir tipus de recursos arbitraris amb una semàntica inspirada en la lògica lineal.
A les cadenes de blocs públiques, els contractes intel·ligents s'enfronten a la lògica de les xarxes públiques amb comptes de garantia, blanqueig de diners, emissió de fitxes OTC i jocs d'atzar. Tot això es fa en un llenguatge sorprenentment mal dissenyat anomenat Solidity, que des d'un punt de vista acadèmic fa que l'autor de PHP sembli un geni. Curiosament, sembla que el nou llenguatge de Facebook no té res a veure amb aquestes tecnologies, ja que en realitat és un llenguatge de script destinat a finalitats empresarials obscures.
En els llibres de registres privats distribuïts, els contractes intel·ligents són un d'aquells termes llançats pels consultors sense tenir gaire en compte la definició o el propòsit clars. Els consultors de programari empresarial solen guanyar diners amb l'ambigüitat, i els contractes intel·ligents són l'apoteosi de l'obscurantisme corporatiu perquè es poden definir literalment com qualsevol cosa.
Després de fer afirmacions sobre la seva seguretat, hem de mirar la semàntica de la llengua. La correcció en la teoria del llenguatge de programació consisteix normalment en dues proves diferents: "progrés" i "preservació", que determinen la coherència de tot l'espai de regles d'avaluació del llenguatge. Més concretament, en la teoria de tipus, una funció és "lineal" si fa servir el seu argument exactament una vegada, i "afí" si l'utilitza com a màxim una vegada. El sistema de tipus lineal proporciona una garantia estàtica que una funció lineal declarada és realment lineal assignant tipus a totes les subexpressions de funció i fent un seguiment d'on es fan les trucades. Aquesta és una propietat subtil de demostrar i no és fàcil d'implementar per a tot un programa. La mecanografia lineal encara és un camp d'estudi molt acadèmic, influenciat per la implementació de la singularitat de tipus a Clean i la propietat de tipus a Rust. Hi ha algunes propostes preliminars per afegir tipus lineals al compilador Glasgow Haskell.
La declaració de Move sobre l'ús de tipus lineals sembla una immersió injustificada al compilador, ja que allà . Pel que es pot dir, el llibre blanc cita literatura canònica de Girard i Peirce, i no hi ha res semblant en la implementació real.
A més, la semàntica formal del llenguatge suposadament segur no apareix enlloc de la implementació ni del document. El llenguatge és prou petit com per trobar una prova completa de la semàntica correcta en Coq o Isabelle. En realitat, un compilador de conversió completa d'extrem a extrem amb transferència de proves a bytecode és molt possible d'implementar amb eines modernes inventades en l'última dècada. Sabem com fer-ho, començant torna el 1996.
Des d'una perspectiva de la teoria del llenguatge de programació, és impossible provar l'afirmació que Move és un llenguatge fiable i segur, ja que aquestes afirmacions equivalen a simples moviments de mà i màrqueting en lloc d'evidència real. Aquesta és una situació alarmant per a un projecte lingüístic al qual se li demana processar milers de milions de dòlars en transaccions.
La criptografia de Balança és defectuosa
Construir criptosistemes segurs és un problema d'enginyeria molt difícil, i sempre és millor abordar el treball amb codi perillós amb una bona dosi de paranoia saludable. Hi ha grans avenços en aquesta àrea, com el projecte Microsoft Everest, que està construint un sistema segur verificable. . Ja existeixen eines per crear primitives verificables. Tot i que això és car, és evident que no supera les capacitats econòmiques de Facebook. No obstant això, l'equip va decidir no participar en el projecte, que es va anunciar com una base fiable per al sistema financer global.
projecte libra de diverses biblioteques força noves per a la creació de criptosistemes experimentals que només han aparegut en els últims anys. És impossible dir si les dependències de les eines següents són segures o no, ja que cap d'aquestes biblioteques ha estat auditada i no té polítiques de divulgació estàndard. En particular, per a algunes biblioteques bàsiques no hi ha certesa pel que fa a la protecció contra atacs de canal lateral i atacs de temporització.
La biblioteca de la biblioteca es torna encara més experimental i va més enllà , aplicant tècniques molt noves com ara funcions aleatòries verificables (VRF), parells bilineals i signatures de llindar. Aquests mètodes i biblioteques poden ser raonables, però combinar-los tots en un sol sistema genera serioses preocupacions sobre la superfície d'atac. La combinació de totes aquestes noves eines i tècniques augmenta enormement la complexitat de demostrar la seguretat.
Cal suposar que tota aquesta pila criptogràfica és vulnerable a diversos atacs fins que no es demostri el contrari. El famós model "Move Fast and Break Things" de Facebook no es pot aplicar a les eines criptogràfiques que processen les dades financeres dels clients.
Libra no implementa els mecanismes de protecció del consumidor
Una característica distintiva del sistema de pagament és la capacitat de revertir una transacció si el pagament es cancel·la per una demanda o provoca una fallada accidental o del sistema. El sistema Libra està dissenyat per ser "complet" i no inclou cap tipus de transacció per a la cancel·lació del pagament. Al Regne Unit, tots els pagaments entre 100 i 30,000 £ estan subjectes a la Llei de crèdit al consumidor. Això vol dir que el sistema de pagament comparteix la responsabilitat amb el venedor en cas d'un problema amb el producte comprat o si el destinatari del pagament no presta el servei. Regles similars s'apliquen a la UE, Àsia i Amèrica del Nord.
El disseny actual de Libra no inclou un protocol per complir amb aquestes lleis i no té un pla clar per crear-ne un. Encara pitjor, des d'una perspectiva arquitectònica, la finalitat de l'estructura de dades autenticades del nucli, basada en l'estat de la unitat Merkle, no permet cap mecanisme per crear aquest protocol sense redissenyar el nucli.
Després de realitzar una revisió tècnica d'aquest projecte, podem concloure que simplement no passarà cap a cap revista d'investigació de sistemes distribuïts o enginyeria financera respectada. Per intentar canviar la política monetària global, cal fer una gran quantitat de treball tècnic per crear una xarxa fiable i un processament segur de les dades dels usuaris en què el públic i els reguladors puguin confiar.
No veig cap motiu per creure que Facebook hagi fet el treball necessari en el seu disseny per superar aquests problemes tècnics o que tingui cap avantatge tècnic respecte a la infraestructura actual. Dir que una empresa necessita flexibilitat normativa per explorar innovacions no és una excusa per no fer-les primer.
Font: www.habr.com