Dois anos depois, voltei ao blog para um post que difere das palestras comuns e chatas sobre Haskell e matemática. Nos últimos anos, lidei com a tecnologia financeira na UE e parece que chegou a hora de escrever um tópico sobre o qual a mídia técnica prestou pouca atenção.
O Facebook lançou recentemente o que chama de "nova plataforma de serviços financeiros" chamada Libra. Ele está posicionado como um sistema de pagamento digital baseado em uma cesta de moedas internacionais que são gerenciadas em uma "blockchain" e armazenadas em um pool de caixa gerenciado da Suíça. Os objetivos do projeto são ambiciosos e acarretam consequências geopolíticas em larga escala.
O
Financial Times e o
New York Times têm muitos artigos razoáveis sobre premissas monetárias e econômicas irracionais no coração do sistema financeiro proposto. Mas não há especialistas suficientes capazes de analisar do ponto de vista técnico. Como muitas pessoas não trabalham na infraestrutura financeira e falam publicamente sobre seu trabalho, esse projeto não é muito abordado na mídia técnica, embora seu interior esteja aberto ao mundo inteiro. Quero dizer código-fonte aberto nos repositórios
Libra e
Calibra Organization .
O que está aberto ao mundo é um artefato esquizofrênico de arquitetura com uma reivindicação do papel de uma plataforma segura para a infraestrutura de pagamento global.
Se você mergulhar na base de código, a implementação real do sistema estará completamente em desacordo com o objetivo declarado e das maneiras mais bizarras. Estou certo de que este projeto tem uma história corporativa interessante. Portanto, é lógico supor que ele foi desenvolvido com algum zelo, mas, na realidade, vejo um conjunto realmente estranho de soluções arquiteturais que quebram todo o sistema e colocam em risco os usuários.
Não reivindicarei uma opinião objetiva sobre o Facebook como empresa. Poucas pessoas no setor de TI olham para ela com simpatia. Mas uma comparação de suas declarações e o código publicado mostra claramente que o objetivo declarado é uma farsa fundamental. Em suma, este projeto não capacita ninguém. Ele permanecerá completamente sob o controle de uma empresa cujo negócio de publicidade está tão envolvido em escândalos e corrupção que ele não tem escolha a não ser tentar diversificar os pagamentos e a pontuação de crédito para sobreviver. Um objetivo claro de longo prazo é atuar como intermediário de dados e intermediário no acesso do consumidor ao crédito com base em seus dados pessoais nas redes sociais. Esta é uma história completamente aterrorizante e sombria, que não presta a atenção que merece.
A única graça salvadora dessa história é que o artefato que eles criaram é tão engraçado que não se encaixa na tarefa que só pode ser vista como um ato de orgulho. Existem vários erros arquiteturais básicos neste projeto:
Resolver o problema dos generais bizantinos em uma rede com controle de acesso é um design inconsistente
A tarefa dos generais bizantinos é um campo bastante restrito de pesquisa de sistemas distribuídos. Ele descreve a capacidade de um sistema de rede suportar falhas arbitrárias de componentes ao executar ações corretivas críticas para o funcionamento do sistema. Uma rede resiliente deve suportar vários tipos de ataques, incluindo reinicializações, falhas, cargas maliciosas e votação maliciosa nas eleições de liderança. Esta é a principal solução para a arquitetura Libra, e é completamente inútil aqui.
A complexidade da sobrecarga de tempo dessa estrutura adicional depende do algoritmo. Há muita literatura sobre as variedades dos protocolos Paxos e Raft com a solução do problema dos generais bizantinos, mas todas essas estruturas introduzem custos adicionais adicionais para a comunicação através de
para manter um quorum. Para Libra, escolhemos o algoritmo com o maior custo possível de comunicação
em caso de falha na liderança. E há uma sobrecarga adicional da possível reeleição de líderes para vários tipos de eventos de falha de rede.
Para um sistema que opera em um consórcio de empresas multinacionais altamente regulamentadas, onde todos os usuários têm um código assinado no Facebook e o acesso à rede é controlado pelo Facebook, simplesmente não faz sentido considerar participantes mal-intencionados em nível de consenso. Não está claro por que, em geral, esse sistema resolve o problema dos generais bizantinos e não apenas mantém uma trilha de auditoria consistente para verificar a conformidade. A possibilidade de que o host Libra, gerenciado pela Mastercard ou Andressen Horrowitz, repentinamente comece a executar códigos maliciosos, é um cenário de planejamento estranho e é melhor resolvido simplesmente garantindo a integridade do protocolo e meios não técnicos (ou seja, legais).
Em depoimento ao Congresso, o produto é declarado concorrente de novos protocolos de pagamento internacionais, como WeChat, Alipay e M-Pesa. No entanto, nenhum desses sistemas foi projetado para funcionar em conjuntos de validadores para resolver o problema dos generais bizantinos. Eles são simplesmente projetados em um barramento tradicional de alto rendimento que faz a fiação de acordo com um conjunto fixo de regras. Essa é uma abordagem natural para o design de um sistema de pagamento.
Um sistema de pagamento
bem projetado simplesmente não atende ao problema de gastos duplos e garfos.
A sobrecarga do algoritmo de consenso não resolve nenhum problema e limita a taxa de transferência do sistema por nenhuma outra razão que não seja o culto à carga do blockchain público, que não se destina a esse caso de uso.
Libra não tem privacidade em transações
De acordo com a documentação, o sistema é projetado levando em consideração o
pseudônimo , ou seja, os endereços usados no protocolo são obtidos de chaves públicas nas curvas elípticas e não contêm metadados sobre as contas. No entanto, em nenhum lugar na descrição da estrutura de gerenciamento da organização ou no próprio protocolo indica como os dados econômicos que participam das transações serão ocultados dos validadores. O sistema foi projetado para replicação em larga escala de transações para várias partes externas, que, de acordo com as leis européias e americanas de sigilo bancário, não devem ser dedicadas a detalhes econômicos.
É difícil coordenar políticas de dados em diferentes países, especialmente considerando leis e regulamentos díspares em jurisdições diferentes que têm visões culturais diferentes sobre proteção e privacidade de dados. O protocolo em si é, por padrão, completamente aberto aos membros do consórcio, o que é uma falha técnica clara que não atende aos requisitos para os quais foi desenvolvido.
O Libra HotStuff BFT não consegue atingir a largura de banda necessária para o sistema de pagamento
No Reino Unido, sistemas de compensação como o BAC são capazes de realizar cerca de 580 milhões de transações por mês. Ao mesmo tempo, sistemas altamente otimizados como o Visa podem processar 150.000.000 de transações por dia. O desempenho depende do tamanho da transação, roteamento da rede, carga do sistema e
verificações AML (esquemas de combate à lavagem de dinheiro, lavagem de dinheiro).
Libra está tentando resolver problemas que, para transferências domésticas, não são realmente problemas, pois os estados-nação modernizaram sua infraestrutura de limpeza na última década. Para os consumidores de varejo na União Europeia, movimentar dinheiro não é um problema. Em uma infraestrutura tradicional, isso pode ser feito com um smartphone padrão em segundos. Para grandes transferências corporativas, existem vários mecanismos e regras relacionados ao movimento de grandes volumes de dinheiro.
Não há razões técnicas pelas quais os pagamentos transfronteiriços também não possam ser feitos instantaneamente, com exceção das diferenças nas regras e requisitos entre as respectivas jurisdições. Se as medidas preventivas necessárias (due diligence do cliente, verificação de sanções etc.) forem realizadas várias vezes em diferentes estágios da cadeia de transações, isso poderá levar a um atraso na transação. No entanto, esse atraso é puramente uma função da lei regulatória e de sua aplicação, não da tecnologia.
Para os consumidores, não há razão para que um acordo no Reino Unido não seja concluído em questão de segundos. As transações de varejo na UE estão realmente desacelerando os
cheques KYC (Conheça o seu cliente) e as restrições AML impostas pelos governos e reguladores que são igualmente aplicáveis aos pagamentos Libra. Mesmo que o Facebook supere os obstáculos às transferências internacionais e à transferência de dados privados, o modelo proposto está a centenas de anos-homem da taxa de transferência de transações globais e provavelmente será processado do zero.
O idioma do Libra Move está incorreto
O white paper faz afirmações ousadas sobre um novo idioma não verificado chamado Move. Essas afirmações são bastante duvidosas do ponto de vista da teoria das linguagens de programação (PLT).
Move é uma nova linguagem de programação para implementar lógica de transação personalizada e "contratos inteligentes" na blockchain Libra. Como Libra pretende um dia servir bilhões de pessoas, o Move é projetado com a máxima prioridade em segurança.
Um recurso importante do Move é a capacidade de definir tipos arbitrários de recursos com semântica inspirada na lógica linear.
Nas blockchains públicas, os contratos inteligentes se chocam com a lógica das redes públicas com contas de garantia, lavagem de dinheiro, a emissão de tokens de balcão e jogos de azar. Tudo isso é feito em uma linguagem incrivelmente mal projetada, chamada Solidity, que, do ponto de vista acadêmico, faz o autor do PHP parecer um gênio. Curiosamente, o novo idioma do Facebook parece não ter nada a ver com essas tecnologias, uma vez que na verdade é uma linguagem de script projetada para tarefas corporativas obscuras.
Nos livros de contabilidade privados, contratos inteligentes são um daqueles termos que os consultores dispersam sem muita atenção a definições ou objetivos claros. Os consultores de software corporativo geralmente ganham dinheiro com a ambiguidade, e os contratos inteligentes são a apoteose do obscurantismo corporativo, porque podem ser definidos literalmente como qualquer coisa.
Após declarações sobre sua segurança, devemos examinar a semântica da linguagem. A correção na teoria das linguagens de programação geralmente consiste em duas provas diferentes: "progresso" e "preservação", que determinam a consistência de todo o espaço das regras de avaliação de uma linguagem. Mais especificamente, na teoria dos tipos, uma função é “linear” se usar seu argumento exatamente uma vez e “afim” se não o usar mais de uma vez. O sistema de tipos lineares fornece uma garantia estática de que a função linear declarada é verdadeiramente linear, atribuindo tipos a todas as subexpressões de funções e rastreando localizações de chamadas. Essa é uma propriedade sutil para prova e não é fácil de implementar para todo o programa. A digitação linear ainda é uma área de pesquisa muito acadêmica, influenciada pela singularidade de tipos em Clean e propriedade de tipos em Rust. Existem algumas sugestões preliminares para adicionar tipos lineares ao compilador Haskell de Glasgow.
A instrução Move sobre o uso de tipos lineares parece imersão irracional no compilador, uma vez que não
existe uma lógica de verificação de tipo . Tanto quanto se pode julgar, o documento técnico cita a literatura canônica de Girard e Pierce, e na implementação real não há nada disso.
Além disso, a semântica formal de uma linguagem supostamente segura não é encontrada em nenhum lugar da implementação ou do documento. A linguagem é pequena o suficiente para encontrar uma prova completa da correção da semântica em Coq ou Isabelle. Na realidade, o compilador de ponta a ponta da conversão completa com a transferência de evidência para bytecode pode ser implementado usando ferramentas modernas inventadas na última década. Sabemos como fazer isso, começando com o
trabalho de George Nekula e Peter Lee em 1996.
Do ponto de vista da teoria das linguagens de programação, é impossível verificar a afirmação de que o Move é uma linguagem confiável e segura, uma vez que essas afirmações se resumem apenas a ondulação e marketing, e não a evidências reais. Essa é uma situação alarmante para um projeto de desenvolvimento de linguagem que está sendo proposto para confiar bilhões de dólares no processamento de transações.
A criptografia de Libra está incorreta
Construir sistemas de criptografia confiáveis é um problema de engenharia muito complexo, e é sempre melhor tratar códigos perigosos com uma boa dose de paranóia saudável. Existem grandes avanços nessa área, como o projeto Microsoft Everest, que cria uma
pilha TLS segura verificável. Já existem ferramentas para criar primitivas verificáveis. Embora seja caro, claramente não vai além das possibilidades econômicas do Facebook. No entanto, a equipe decidiu não participar do projeto, declarado como uma base confiável para o sistema financeiro global.
O projeto libra
conta com várias bibliotecas razoavelmente novas para a criação de sistemas criptográficos experimentais, que só apareceram nos últimos anos. É impossível dizer se as dependências das seguintes ferramentas são seguras ou não, pois nenhuma dessas bibliotecas foi auditada e não possui políticas de divulgação padrão. Em particular, para algumas bibliotecas importantes, não há certeza quanto à proteção contra ataques a canais de terceiros e ataques de tempo.
- ed25519-dalek
- curve25519-dalek
A biblioteca libra é ainda mais experimental e vai além do
modelo padrão, usando métodos muito novos, como funções aleatórias verificáveis (VRFs), pares bilineares e assinaturas de limites. Esses métodos e bibliotecas podem ser razoáveis, mas combiná-los todos em um sistema gera sérias preocupações sobre a área da superfície de ataque. A combinação de todas essas novas ferramentas e técnicas aumenta bastante a complexidade das evidências de segurança.
Deve-se supor que toda essa pilha criptográfica é vulnerável a vários ataques, até prova em contrário. O conhecido modelo do Facebook 'Move Fast and Break Things' não pode ser aplicado a ferramentas criptográficas que processam os dados financeiros dos clientes.
Libra não pode implementar mecanismos de proteção ao consumidor
Uma característica distintiva do sistema de pagamento é a capacidade de reverter a transação se o pagamento for cancelado por uma ação judicial ou levar a uma falha acidental ou do sistema. O Libra foi projetado para ser "totalmente concluído" e não inclui um tipo de transação para cancelar um pagamento. No Reino Unido, todos os pagamentos de £ 100 a £ 30.000 são regidos pelo Consumer Credit Act. Isso significa que o sistema de pagamento compartilha a responsabilidade com o vendedor em caso de problemas com os bens adquiridos ou se o beneficiário não prestou o serviço. Regras semelhantes se aplicam na UE, Ásia e América do Norte.
O desenho atual do Libra não inclui um protocolo para cumprir essas leis e não possui um plano claro para sua criação. Pior ainda, do ponto de vista arquitetural, a finalidade da estrutura dos dados autenticados do kernel, com base no estado da unidade Merkle, não permite nenhum mecanismo para criar esse protocolo sem redesenhar o kernel.
Após a realização de um exame técnico deste projeto, podemos concluir que ele simplesmente não passará no teste de qualquer revista respeitada em pesquisa de sistemas distribuídos ou engenharia financeira. Para tentar mudar a política monetária global, é necessário fazer uma enorme quantidade de trabalho técnico para criar uma rede confiável e um processamento seguro de dados do usuário, no qual as autoridades públicas e reguladoras possam confiar.
Não vejo razão para acreditar que o Facebook em seu projeto tenha feito o trabalho necessário para superar esses problemas técnicos ou que tenha algumas vantagens técnicas sobre a infraestrutura existente.
A afirmação de que uma empresa precisa de flexibilidade regulatória para aprender sobre inovações não é desculpa para não fazê-las primeiro.