Dos a帽os despu茅s, volv铆 al blog por una publicaci贸n que difiere de las habituales conferencias aburridas sobre Haskell y las matem谩ticas. En los 煤ltimos a帽os, me he ocupado de la tecnolog铆a financiera en la UE, y parece que ha llegado el momento de escribir sobre un tema al que los medios t茅cnicos prestaron poca atenci贸n.
Facebook lanz贸 recientemente lo que llama la "nueva plataforma de servicios financieros" llamada Libra. Se posiciona como un sistema de pago digital basado en una canasta de monedas internacionales que se administran en una "cadena de bloques" y se almacenan en un grupo de efectivo administrado desde Suiza. Los objetivos del proyecto son ambiciosos y conllevan consecuencias geopol铆ticas a gran escala.
El
Financial Times y el
New York Times tienen muchos art铆culos razonables sobre supuestos monetarios y econ贸micos irrazonables en el coraz贸n del sistema financiero propuesto. Pero no hay suficientes especialistas capaces de an谩lisis desde un punto de vista t茅cnico. No muchas personas trabajan en la infraestructura financiera y hablan p煤blicamente sobre su trabajo, por lo que este proyecto no est谩 demasiado cubierto en los medios t茅cnicos, aunque sus interiores est谩n abiertos a todo el mundo. Me refiero al c贸digo abierto en los repositorios de
Libra y
Calibra Organization .
Lo que est谩 abierto al mundo es un artefacto esquizofr茅nico arquitect贸nico con el reclamo del papel de una plataforma segura para la infraestructura de pago global.
Si se sumerge en la base del c贸digo, entonces la implementaci贸n real del sistema est谩 completamente en desacuerdo con el objetivo establecido, y de las maneras m谩s extra帽as. Estoy seguro de que este proyecto tiene una interesante historia corporativa. Por lo tanto, es l贸gico suponer que se desarroll贸 con cierto entusiasmo, pero en realidad veo un conjunto realmente extra帽o de soluciones arquitect贸nicas que rompen todo el sistema y ponen en peligro a los usuarios.
No reclamar茅 una opini贸n objetiva sobre Facebook como empresa. Pocas personas en la industria de TI la miran con simpat铆a. Pero una comparaci贸n de sus declaraciones y el c贸digo publicado muestra claramente que el prop贸sito declarado es un enga帽o fundamental. En resumen, este proyecto no empodera a nadie. Permanecer谩 completamente bajo el control de una empresa cuyo negocio publicitario est谩 tan enredado en esc谩ndalos y corrupci贸n que no tiene m谩s remedio que intentar diversificar los pagos y la calificaci贸n crediticia para sobrevivir. Un objetivo claro a largo plazo es actuar como intermediario de datos e intermediario en el acceso de los consumidores al cr茅dito en funci贸n de sus datos personales en las redes sociales. Esta es una historia completamente aterradora y sombr铆a, que no presta la atenci贸n que merece.
La 煤nica gracia salvadora de esta historia es que el artefacto que crearon es tan divertido que no se ajusta a la tarea que solo puede verse como un acto de orgullo. Hay varios errores arquitect贸nicos b谩sicos en este proyecto:
Resolver el problema de los generales bizantinos en una red con control de acceso es un dise帽o inconsistente
La tarea de los generales bizantinos es un campo de investigaci贸n bastante limitado de sistemas distribuidos. Describe la capacidad de un sistema de red para soportar fallas arbitrarias de componentes cuando se toman acciones correctivas cr铆ticas para el funcionamiento del sistema. Una red resistente debe resistir varios tipos de ataques, incluidos reinicios, fallas, cargas maliciosas y votaciones maliciosas en las elecciones de liderazgo. Esta es la soluci贸n principal para la arquitectura de Libra, y aqu铆 no tiene ning煤n sentido.
La sobrecarga de la complejidad del tiempo de esta estructura adicional depende del algoritmo. Existe mucha literatura sobre las variedades de los protocolos Paxos y Raft con la soluci贸n del problema de los generales bizantinos, pero todas estas estructuras introducen costos generales adicionales para la comunicaci贸n a trav茅s de
para mantener un qu贸rum. Para Libra, elegimos el algoritmo con el costo de comunicaci贸n m谩s alto posible
en caso de falla de liderazgo. Y existe una sobrecarga adicional por la posible reelecci贸n de l铆deres para varios tipos de eventos de falla de red.
Para un sistema que opera en un consorcio de corporaciones transnacionales altamente reguladas, donde todos los usuarios tienen un c贸digo firmado por Facebook y el acceso a la red est谩 controlado por Facebook, simplemente no tiene sentido considerar participantes maliciosos a nivel de consenso. No est谩 claro por qu茅, en general, este sistema resuelve el problema de los generales bizantinos, y no solo mantiene una pista de auditor铆a consistente para verificar el cumplimiento. La posibilidad de que el host Libra, administrado por Mastercard o Andressen Horrowitz, de repente comience a ejecutar c贸digo malicioso, es un escenario de planificaci贸n extra帽o y se resuelve mejor simplemente asegurando la integridad del protocolo y los medios no t茅cnicos (es decir, legales).
En testimonio para el Congreso, el producto es declarado competidor de nuevos protocolos de pago internacionales como WeChat, Alipay y M-Pesa. Sin embargo, ninguno de estos sistemas est谩 dise帽ado para funcionar en grupos de validadores para resolver el problema de los generales bizantinos. Simplemente est谩n dise帽ados en un bus tradicional de alto rendimiento que realiza el cableado de acuerdo con un conjunto fijo de reglas. Este es un enfoque natural para el dise帽o de un sistema de pago.
Un sistema de pago
bien dise帽ado simplemente no resuelve el problema del doble gasto y los tenedores.
La sobrecarga del algoritmo de consenso no resuelve ning煤n problema y solo limita el rendimiento del sistema sin otra raz贸n que el culto a la carga de la cadena de bloques p煤blica, que no est谩 destinada para este caso de uso.
Libra no tiene privacidad de transacci贸n
De acuerdo con la documentaci贸n, el sistema est谩 dise帽ado teniendo en cuenta el
seud贸nimo , es decir, las direcciones utilizadas en el protocolo se obtienen de claves p煤blicas en curvas el铆pticas y no contienen metadatos sobre las cuentas. Sin embargo, en ninguna parte de la descripci贸n de la estructura de gesti贸n de la organizaci贸n o en el protocolo en s铆 indica c贸mo los datos econ贸micos que participan en las transacciones se ocultar谩n a los validadores. El sistema est谩 dise帽ado para la replicaci贸n a gran escala de transacciones para una serie de partes externas que, de acuerdo con las leyes de secreto bancario europeas y americanas existentes, no deber铆an dedicarse a los detalles econ贸micos.
Las pol铆ticas de datos en diferentes pa铆ses son dif铆ciles de coordinar, especialmente dadas las leyes y regulaciones dispares en diferentes jurisdicciones que tienen diferentes puntos de vista culturales sobre protecci贸n de datos y privacidad. El protocolo en s铆 est谩 completamente abierto por defecto a los miembros del consorcio, lo cual es una falla t茅cnica clara que no cumple con los requisitos para los que fue desarrollado.
Libra HotStuff BFT no puede lograr el ancho de banda requerido para el sistema de pago
En el Reino Unido, los sistemas de compensaci贸n como BAC son capaces de realizar alrededor de 580 millones de transacciones por mes. Al mismo tiempo, los sistemas altamente optimizados como Visa pueden procesar 150,000,000 de transacciones por d铆a. El rendimiento depende del tama帽o de la transacci贸n, el enrutamiento de la red, la carga del sistema y las
comprobaciones de AML (esquemas contra el lavado de dinero, lavado de dinero).
Libra est谩 tratando de resolver problemas que para las transferencias nacionales no son realmente problemas, ya que los estados nacionales han modernizado su infraestructura de compensaci贸n en la 煤ltima d茅cada. Para los consumidores minoristas en la Uni贸n Europea, mover dinero no es un problema en absoluto. En una infraestructura tradicional, esto se puede hacer con un tel茅fono inteligente est谩ndar en segundos. Para las grandes transferencias corporativas, existen varios mecanismos y reglas relacionadas con el movimiento de grandes vol煤menes de dinero.
No hay razones t茅cnicas por las que los pagos transfronterizos tampoco se puedan realizar de manera instant谩nea, con la excepci贸n de las diferencias en las normas y requisitos entre las jurisdicciones respectivas. Si las medidas preventivas necesarias (debida diligencia del cliente, verificaci贸n de sanciones, etc.) se llevan a cabo varias veces en diferentes etapas de la cadena de transacciones, esto puede conducir a un retraso en la transacci贸n. Sin embargo, este retraso es puramente una funci贸n de la ley reguladora y su aplicaci贸n, no de la tecnolog铆a.
Para los consumidores, no hay ninguna raz贸n por la cual un acuerdo en el Reino Unido no se resuelva en cuesti贸n de segundos. Las transacciones minoristas en la UE realmente se est谩n ralentizando en los
cheques KYC (Conozca a su cliente) y las restricciones ALD impuestas por los gobiernos y los reguladores, que son igualmente aplicables a los pagos de Libra. Incluso si Facebook supera los obst谩culos a las transferencias internacionales y la transferencia de datos privados, el modelo propuesto est谩 a cientos de a帽os-hombre del rendimiento de las transacciones globales y es probable que se procese desde cero.
El idioma de Libra Move es incorrecto
El documento t茅cnico hace declaraciones audaces sobre un nuevo lenguaje no verificado llamado Move. Estas declaraciones son bastante dudosas desde el punto de vista de la teor铆a de los lenguajes de programaci贸n (PLT).
Move es un nuevo lenguaje de programaci贸n para implementar l贸gica de transacci贸n personalizada y "contratos inteligentes" en la cadena de bloques Libra. Como Libra tiene como objetivo servir alg煤n d铆a a miles de millones de personas, Move est谩 dise帽ado con la m谩xima prioridad en seguridad.
Una caracter铆stica clave de Move es la capacidad de definir tipos arbitrarios de recursos con una sem谩ntica inspirada en la l贸gica lineal.
En blockchains p煤blicos, los contratos inteligentes se topan con la l贸gica de las redes p煤blicas con cuentas de dep贸sito en garant铆a, lavado de dinero, el tema de los tokens de venta libre y los juegos de azar. Todo esto se hace en un lenguaje incre铆blemente mal dise帽ado llamado Solidez, que desde un punto de vista acad茅mico hace que el autor de PHP parezca un genio. Curiosamente, el nuevo lenguaje de Facebook no parece tener nada que ver con estas tecnolog铆as, ya que en realidad es un lenguaje de secuencias de comandos dise帽ado para tareas corporativas oscuras.
En los libros contables privados distribuidos, los contratos inteligentes son uno de esos t茅rminos que los consultores dispersan sin prestar especial atenci贸n a definiciones u objetivos claros. Los consultores de software corporativo generalmente ganan dinero con la ambig眉edad, y los contratos inteligentes son la apoteosis del oscurantismo corporativo porque pueden definirse literalmente como cualquier cosa.
Despu茅s de las declaraciones sobre su seguridad, debemos mirar la sem谩ntica del lenguaje. La correcci贸n en la teor铆a de los lenguajes de programaci贸n generalmente consiste en dos pruebas diferentes: "progreso" y "preservaci贸n", que determinan la consistencia de todo el espacio de reglas de evaluaci贸n para un lenguaje. M谩s espec铆ficamente, en la teor铆a de tipos, una funci贸n es "lineal" si usa su argumento exactamente una vez, y "af铆n" si la usa no m谩s de una vez. El sistema de tipo lineal proporciona una garant铆a est谩tica de que la funci贸n lineal declarada es verdaderamente lineal, asignando tipos a todas las subexpresiones de funciones y rastreando ubicaciones de llamadas. Esta es una propiedad sutil para prueba, y no es f谩cil de implementar para todo el programa. La escritura lineal sigue siendo un 谩rea de investigaci贸n muy acad茅mica, influenciada por la singularidad de los tipos en Clean y la propiedad de tipos en Rust. Hay algunas sugerencias preliminares para agregar tipos lineales al compilador Haskell de Glasgow.
La declaraci贸n Move sobre el uso de tipos lineales parece una inmersi贸n irracional en el compilador, ya que no
existe tal l贸gica de verificaci贸n de tipos . Hasta donde se puede juzgar, el documento t茅cnico cita literatura can贸nica de Girard y Pierce, y en la implementaci贸n real no hay nada de eso.
Adem谩s, la sem谩ntica formal de un lenguaje supuestamente seguro no se encuentra en ninguna parte ni en la implementaci贸n ni en el documento. El lenguaje es lo suficientemente peque帽o como para encontrar una prueba completa de la correcci贸n de la sem谩ntica en Coq o Isabelle. En realidad, el compilador de extremo a extremo de la conversi贸n completa con la transferencia de evidencia a bytecode se puede implementar utilizando herramientas modernas inventadas en la 煤ltima d茅cada. Sabemos c贸mo hacerlo, comenzando con el
trabajo de George Nekula y Peter Lee en 1996.
Desde el punto de vista de la teor铆a de los lenguajes de programaci贸n, es imposible verificar la afirmaci贸n de que Move es un lenguaje confiable y seguro, ya que estas afirmaciones se reducen exclusivamente a agitar y comercializar, y no a evidencia real. Esta es una situaci贸n alarmante para un proyecto de desarrollo del lenguaje que se propone para confiar miles de millones de d贸lares en el procesamiento de transacciones.
La criptograf铆a de libra es incorrecta
La construcci贸n de sistemas criptogr谩ficos confiables es un problema de ingenier铆a muy complejo, y siempre es mejor tratar el c贸digo peligroso con una buena dosis de paranoia saludable. Hay avances importantes en esta 谩rea, como el proyecto Microsoft Everest, que construye una
pila TLS segura verificable. Ya existen herramientas para crear primitivas verificables. Aunque es costoso, claramente no va m谩s all谩 de las posibilidades econ贸micas de Facebook. Sin embargo, el equipo decidi贸 no participar en el proyecto, declarado como una base confiable para el sistema financiero global.
El proyecto libra se
basa en varias bibliotecas bastante nuevas para crear criptosistemas experimentales, que solo aparecieron en los 煤ltimos a帽os. Es imposible decir si las dependencias de las siguientes herramientas son seguras o no, ya que ninguna de estas bibliotecas ha sido auditada y no tiene pol铆ticas de divulgaci贸n est谩ndar. En particular, para algunas bibliotecas principales no hay certeza con respecto a la protecci贸n contra ataques en canales de terceros y ataques de tiempo.
- ed25519-dalek
- curva25519-dalek
La biblioteca de libra es a煤n m谩s experimental y va m谩s all谩 del
modelo est谩ndar utilizando m茅todos muy nuevos, como funciones aleatorias verificables (VRF), pares bilineales y firmas de umbral. Estos m茅todos y bibliotecas pueden ser razonables, pero combinarlos en un solo sistema plantea serias preocupaciones sobre el 谩rea de superficie de ataque. La combinaci贸n de todas estas nuevas herramientas y t茅cnicas aumenta enormemente la complejidad de la evidencia de seguridad.
Se debe suponer que toda esta pila criptogr谩fica es vulnerable a varios ataques, hasta que se demuestre lo contrario. El conocido modelo de Facebook 'Move Fast and Break Things' no se puede aplicar a las herramientas criptogr谩ficas que procesan los datos financieros de los clientes.
Libra no puede implementar mecanismos de protecci贸n al consumidor
Una caracter铆stica distintiva del sistema de pago es la capacidad de revertir la transacci贸n si el pago es cancelado por una demanda o conduce a una falla accidental o del sistema. Libra est谩 dise帽ado para ser "completamente completado" y no incluye un tipo de transacci贸n para cancelar un pago. En el Reino Unido, todos los pagos de 拢 100 a 拢 30,000 se rigen por la Ley de Cr茅dito al Consumidor. Esto significa que el sistema de pago comparte la responsabilidad con el vendedor en caso de un problema con los bienes comprados o si el beneficiario no prest贸 el servicio. Reglas similares se aplican en la UE, Asia y Am茅rica del Norte.
El dise帽o actual de Libra no incluye un protocolo para cumplir con estas leyes y no tiene un plan claro para su creaci贸n. Peor a煤n, desde un punto de vista arquitect贸nico, la estructura final de los datos del n煤cleo autenticados, basada en el estado de la unidad Merkle, no permite ning煤n mecanismo para crear dicho protocolo sin redise帽ar el n煤cleo.
Despu茅s de realizar un examen t茅cnico de este proyecto, podemos concluir que simplemente no pasar谩 la prueba en ninguna revista respetada sobre investigaci贸n de sistemas distribuidos o ingenier铆a financiera. Para tratar de cambiar la pol铆tica monetaria global, es necesario realizar una gran cantidad de trabajo t茅cnico para crear una red confiable y un procesamiento seguro de los datos de los usuarios, en los que el p煤blico y las autoridades reguladoras puedan confiar.
No veo ninguna raz贸n para creer que Facebook en su proyecto hizo el trabajo necesario para superar estos problemas t茅cnicos o que tiene algunas ventajas t茅cnicas sobre la infraestructura existente.
La afirmaci贸n de que una empresa necesita flexibilidad regulatoria para aprender sobre las innovaciones no es excusa para no hacerlas primero.