Despois de dous anos, volvín ao blog por unha publicación que difire das aburridas charlas habituais sobre Haskell e as matemáticas. Estiven traballando en fintech na UE durante os últimos anos e parece que chegou o momento de escribir sobre un tema que recibiu pouca atención dos medios tecnolóxicos.
Facebook lanzou recentemente o que chama unha "nova plataforma de servizos financeiros" chamada Libra. Está situado como un sistema de liquidación dixital baseado nunha cesta de moedas internacionais que se xestionan nunha "cadea de bloques" e que se almacenan nun pool de diñeiro xestionado desde Suíza. Os obxectivos do proxecto son ambiciosos e implican consecuencias xeopolíticas a gran escala.
В и Moitos artigos sensatos sobre as suposicións monetarias e económicas non sólidas detrás do sistema financeiro proposto. Pero non hai suficientes especialistas capaces de analizar dende o punto de vista técnico. Non moita xente traballa en infraestruturas financeiras e fala publicamente do seu traballo, polo que este proxecto non ten moita cobertura nos medios tecnolóxicos, aínda que as súas entrañas están abertas ao mundo. Refírome a código aberto nos repositorios и .
O que está aberto ao mundo é un artefacto arquitectónicamente esquizofrénico que pretende ser unha plataforma segura para a infraestrutura de pago global.
Se mergullas na base do código, a implementación real do sistema diverxe completamente do obxectivo declarado e das formas máis estrañas. Estou seguro de que este proxecto ten unha historia corporativa interesante. Polo tanto, é lóxico asumir que foi deseñado con certa dilixencia, pero en realidade vexo un conxunto de decisións arquitectónicas realmente estrañas que rompen todo o sistema e poñen en risco aos usuarios.
Non pretenderei ter unha opinión obxectiva sobre Facebook como empresa. Poucas persoas na industria das TIC miran con simpatía. Pero unha comparación das súas declaracións e o código publicado mostra claramente que o propósito declarado é fundamentalmente enganoso. En definitiva, este proxecto non empodera a ninguén. Permanecerá totalmente baixo o control dunha empresa cuxo negocio publicitario está tan metido no escándalo e na corrupción que non lle queda outra que tentar diversificar os seus pagos e a súa puntuación crediticia para sobrevivir. O obxectivo claro a longo prazo é actuar como intermediario de datos e intermediario no acceso dos consumidores ao crédito en función dos seus datos persoais das redes sociais. Esta é unha historia absolutamente espantosa e escura que non recibe a atención que merece.
A única graza salvadora desta historia é que o artefacto que crearon non é tan hilarantemente inadecuado para a tarefa que só se pode ver como un acto de arrogancia. Neste proxecto hai varios erros arquitectónicos importantes:
Resolver o problema dos xenerais bizantinos nunha rede de control de acceso é un deseño inconsistente
O problema dos xenerais bizantinos é unha área bastante estreita de investigación de sistemas distribuídos. Describe a capacidade dun sistema de rede para soportar fallos aleatorios de compoñentes mentres toma accións correctoras críticas para o funcionamento do sistema. Unha rede resistente debe soportar varios tipos de ataques, incluíndo reinicios, interrupcións, cargas maliciosas e votacións maliciosas nas eleccións de liderado. Esta é a decisión principal para a arquitectura Libra, e aquí carece de sentido.
A complexidade temporal desta estrutura adicional depende do algoritmo. Hai moita literatura sobre variantes dos protocolos Paxos e Raft que resolven o problema dos xenerais bizantinos, pero todas estas estruturas introducen sobrecarga adicional para a comunicación. 
para manter o quórum. Para Libra, escolleron un algoritmo co custo de comunicación máis alto posible en caso de fracaso do liderado. E hai unha sobrecarga adicional derivada da potencial reelección de líderes en varios tipos de eventos de falla de rede.
Para un sistema que opera dentro dun consorcio de corporacións multinacionais moi reguladas, onde todos os usuarios teñen código asinado por Facebook e o acceso á rede está controlado por Facebook, simplemente non ten sentido considerar participantes maliciosos a nivel de consenso. Non está claro por que este sistema resolvería o problema dos xenerais bizantinos, en lugar de simplemente manter unha pista de auditoría consistente para comprobar o cumprimento. A posibilidade de que un nodo Libra executado por Mastercard ou Andressen Horrowitz comece de súpeto a executar código malicioso é un escenario estraño para planificar e é mellor abordado simplemente garantindo a integridade do protocolo e os medios non técnicos (é dicir, legais).
Testimony to Congress presentou o produto como un competidor de novos protocolos de pago internacionais como WeChat, Alipay e M-Pesa. Non obstante, ningún destes sistemas está deseñado para executarse en grupos de validadores para resolver o problema dos xenerais bizantinos. Simplemente están deseñados nun bus tradicional de gran ancho de banda que fai o cableado segundo un conxunto de regras fixas. Este é un enfoque natural para deseñar un sistema de pago. Ben deseñado o sistema de pago simplemente non se atopará co problema do dobre gasto e os garfos.
A sobrecarga do algoritmo de consenso non resolve ningún problema e só limita o rendemento do sistema sen outro motivo que o culto á carga da cadea de bloques pública, que non está destinada a este caso de uso.
Libra non ten privacidade de transaccións
Segundo a documentación, o sistema está deseñado tendo en conta pseudónimo, é dicir, os enderezos utilizados no protocolo obtéñense de claves públicas en curvas elípticas e non conteñen metadatos sobre as contas. Non obstante, en ningún lugar da descrición da estrutura de goberno da organización nin do propio protocolo indican como se ocultarán aos validadores os datos económicos implicados nas transaccións. O sistema está deseñado para replicar transaccións a gran escala a unha serie de partes externas que, segundo as leis de segredo bancario existentes en Europa e Estados Unidos, non deberían estar ao tanto dos detalles económicos.
As políticas de datos entre os países son difíciles de coordinar, especialmente tendo en conta leis e regulamentos dispares en diferentes xurisdicións con diferentes visións culturais sobre a protección de datos e a privacidade. O protocolo en si está por defecto totalmente aberto aos membros do consorcio, o que supón unha clara deficiencia técnica que non cumpre os requisitos para os que está deseñado.
Libra HotStuff BFT non pode acadar o rendemento necesario para un sistema de pago
No Reino Unido, os sistemas de compensación como BAC son capaces de xestionar unhas 580 de transaccións ao mes. Ao mesmo tempo, sistemas altamente optimizados como Visa poden procesar 000 de transaccións ao día. O rendemento varía dependendo do tamaño da transacción, o enrutamento da rede, a carga do sistema e (anti-branqueo de capitais, esquemas de branqueo de capitais).
Libra está tentando resolver problemas que non son realmente problemas para as transferencias nacionais, xa que os estados nacionais modernizaron a súa infraestrutura de compensación durante a última década. Para os consumidores polo miúdo da Unión Europea, mover diñeiro non é un problema en absoluto. Na infraestrutura tradicional, isto pódese facer cun teléfono intelixente estándar en segundos. Para grandes transferencias corporativas, hai varios mecanismos e regras asociados ao movemento de grandes cantidades de diñeiro.
Non hai ningunha razón técnica para que os pagos transfronteirizos non se poidan procesar ao instante, salvo as diferenzas de regras e requisitos entre as xurisdicións pertinentes. Se as medidas preventivas necesarias (dilixencia debida ao cliente, comprobacións de sancións, etc.) se realizan varias veces en diferentes etapas da cadea de transaccións, isto pode provocar un atraso na transacción. Non obstante, este atraso é puramente unha función da lexislación regulamentaria e do cumprimento, non da tecnoloxía.
Para os consumidores, non hai razón para que unha transacción do Reino Unido non se aclare en cuestión de segundos. As transaccións polo miúdo na UE están a diminuír (Coñece o teu cliente) e restricións AML impostas polos gobernos e os reguladores, que se aplican por igual aos pagos de Libra. Aínda que Facebook superase os obstáculos para as transferencias transfronteirizas e as transferencias de datos privados, o modelo proposto está a centos de anos persoa do rendemento global das transaccións e probablemente teña que ser redeseñado desde cero.
O idioma de Libra Move é incorrecto
O libro branco fai afirmacións audaces sobre un novo idioma sen probar chamado Move. Estas afirmacións son bastante dubidosas desde o punto de vista da teoría da linguaxe de programación (PLT).
Move é unha nova linguaxe de programación para implementar lóxica de transacción personalizada e contratos intelixentes na cadea de bloques Libra. Dado que Libra pretende servir algún día a miles de millóns de persoas, Move está deseñado coa seguridade como unha prioridade.
Unha característica clave de Move é a capacidade de definir tipos de recursos arbitrarios cunha semántica inspirada na lóxica lineal.
Nas cadeas de bloques públicas, os contratos intelixentes enfróntanse á lóxica das redes públicas con contas de garantía, branqueo de cartos, emisión de tokens OTC e xogos de azar. Todo isto faise nunha linguaxe sorprendentemente mal deseñada chamada Solidity, que dende o punto de vista académico fai que o autor de PHP pareza un xenio. Curiosamente, a nova linguaxe de Facebook parece non ter nada que ver con estas tecnoloxías, xa que en realidade é unha linguaxe de script destinada a fins empresariais escuros.
Nos libros de contas distribuídas privadas, os contratos intelixentes son un deses termos lanzados polos consultores sen ter moito en conta a definición ou propósito claro. Os consultores de software empresarial adoitan gañar cartos coa ambigüidade, e os contratos intelixentes son a apoteose do escurantismo corporativo porque se poden definir literalmente como calquera cousa.
Despois de facer afirmacións sobre a súa seguridade, hai que mirar a semántica da lingua. A corrección na teoría da linguaxe de programación consiste normalmente en dúas probas diferentes: "progreso" e "preservación", que determinan a coherencia de todo o espazo de regras de avaliación da linguaxe. Máis concretamente, na teoría de tipos, unha función é "lineal" se usa o seu argumento exactamente unha vez, e "afín" se a usa como máximo unha vez. O sistema de tipos lineais proporciona unha garantía estática de que unha función lineal declarada é verdadeiramente lineal, asignando tipos a todas as subexpresións de funcións e facendo un seguimento de onde se realizan as chamadas. Esta é unha propiedade sutil para demostrar e non é fácil de implementar para todo un programa. A dixitación lineal aínda é un campo de estudo moi académico, influenciado pola implementación da singularidade do tipo en Clean e da propiedade do tipo en Rust. Existen algunhas propostas preliminares para engadir tipos lineais ao compilador Glasgow Haskell.
A declaración de Move sobre o uso de tipos lineais parece unha inmersión inxustificada no compilador, xa que alí . Polo que se pode dicir, o libro branco cita literatura canónica de Girard e Peirce, e non hai nada semellante na implementación real.
Ademais, a semántica formal da linguaxe supostamente segura non aparece en ningunha parte nin na implementación nin no documento. A linguaxe é o suficientemente pequena como para atopar unha proba completa da semántica correcta en Coq ou Isabelle. En realidade, un compilador de conversión completa de extremo a extremo con transferencia de probas a bytecode é moi posible de implementar con ferramentas modernas inventadas na última década. Sabemos como facelo, comezando alá polo 1996.
Desde a perspectiva da teoría da linguaxe de programación, é imposible probar a afirmación de que Move é unha linguaxe fiable e segura, xa que estas afirmacións equivalen a simples axitacións e marketing en lugar de probas reais. Esta é unha situación alarmante para un proxecto lingüístico ao que se lle pide que procese miles de millóns de dólares en transaccións.
A criptografía de Libra é defectuosa
Construír criptosistemas seguros é un problema de enxeñería moi difícil, e sempre é mellor abordar o traballo con código perigoso cunha boa dose de paranoia saudable. Hai avances importantes nesta área, como o proxecto Microsoft Everest, que está a construír un sistema seguro verificable. . Xa existen ferramentas para crear primitivas verificables. Aínda que isto é caro, claramente non supera as capacidades económicas de Facebook. Non obstante, o equipo decidiu non participar no proxecto, que se anunciou como unha base fiable para o sistema financeiro global.
proxecto libra de varias bibliotecas bastante novas para a creación de criptosistemas experimentais que só apareceron nos últimos anos. É imposible dicir se as dependencias das seguintes ferramentas son seguras ou non, xa que ningunha destas bibliotecas foi auditada e non teñen políticas de divulgación estándar. En particular, para algunhas bibliotecas principais non hai ningunha certeza sobre a protección contra ataques de canle lateral e ataques de temporización.
A biblioteca da biblioteca faise aínda máis experimental e vai máis alá , aplicando técnicas moi novas como funcións aleatorias verificables (VRF), pares bilineais e sinaturas de limiar. Estes métodos e bibliotecas poden ser razoables, pero combinalos todos nun só sistema suscita serias preocupacións sobre a superficie de ataque. A combinación de todas estas novas ferramentas e técnicas aumenta moito a complexidade de probar a seguridade.
Débese asumir que toda esta pila criptográfica é vulnerable a varios ataques ata que se demostre o contrario. O famoso modelo "Move Fast and Break Things" de Facebook non se pode aplicar ás ferramentas criptográficas que procesan os datos financeiros dos clientes.
Libra non aplica os mecanismos de protección do consumidor
Unha característica distintiva do sistema de pago é a capacidade de retrotraer unha transacción se o pago é cancelado por unha demanda ou leva a un fallo accidental ou do sistema. O sistema Libra está deseñado para ser "completo" e non inclúe un tipo de transacción para a cancelación do pago. No Reino Unido, todos os pagos entre £ 100 e £ 30,000 están suxeitos á Lei de crédito ao consumidor. Isto significa que o sistema de pago comparte a responsabilidade co vendedor no caso de producirse un problema co produto adquirido ou se o destinatario do pago non presta o servizo. Regras similares aplícanse na UE, Asia e América do Norte.
O deseño actual de Libra non inclúe un protocolo para cumprir con estas leis e non ten un plan claro para a súa creación. Peor aínda, desde unha perspectiva arquitectónica, a finalidade da estrutura de datos autenticados do núcleo, baseada no estado da unidade Merkle, non permite ningún mecanismo para crear tal protocolo sen redeseñar o núcleo.
Despois de realizar unha revisión técnica deste proxecto, podemos concluír que simplemente non se reunirá en ningunha revista de investigación de sistemas distribuídos ou de enxeñería financeira respectada. Para tentar cambiar a política monetaria global, hai que facer unha gran cantidade de traballo técnico para crear unha rede fiable e un procesamento seguro dos datos dos usuarios no que o público e os reguladores poidan confiar.
Non vexo ningunha razón para crer que Facebook fixo o traballo necesario no seu deseño para superar estes problemas técnicos ou que teña algunha vantaxe técnica sobre a infraestrutura actual. Dicir que unha empresa necesita flexibilidade normativa para explorar innovacións non é unha escusa para non facelos primeiro.
Fonte: www.habr.com