Deux ans plus tard, je suis retourné sur le blog pour un article qui diffère des conférences ennuyeuses habituelles sur Haskell et les mathématiques. Au cours des dernières années, j'ai traité de la technologie financière dans l'UE et il semble que le moment soit venu d'écrire sur un sujet auquel les médias techniques n'ont pas prêté attention.
Facebook a récemment publié ce qu'elle appelle la «nouvelle plate-forme de services financiers» appelée Libra. Il se positionne comme un système de paiement numérique basé sur un panier de devises internationales géré sur une «blockchain» et stocké dans un cash pool géré depuis la Suisse. Les objectifs du projet sont ambitieux et entraînent des conséquences géopolitiques à grande échelle.
Le
Financial Times et le
New York Times contiennent de nombreux articles raisonnables sur des hypothèses monétaires et économiques déraisonnables au cœur du système financier proposé. Mais il n'y a pas assez de spécialistes capables d'analyser d'un point de vue technique. Peu de gens travaillent sur l'infrastructure financière et parlent publiquement de leur travail, donc ce projet n'est pas trop couvert par les médias techniques, bien que son intérieur soit ouvert au monde entier. Je veux dire open source dans les référentiels
Libra et
Calibra Organisation .
Ce qui est ouvert au monde est un artefact schizophrénique architectural qui revendique le rôle d'une plate-forme sécurisée pour l'infrastructure de paiement mondiale.
Si vous plongez dans la base de code, la mise en œuvre réelle du système est complètement en contradiction avec l'objectif déclaré et de la manière la plus bizarre. Je suis sûr que ce projet a une histoire d'entreprise intéressante. Par conséquent, il est logique de supposer qu'il a été développé avec un certain zèle, mais en réalité je vois un ensemble vraiment étrange de solutions architecturales qui brisent l'ensemble du système et mettent en danger les utilisateurs.
Je ne revendiquerai pas d'opinion objective sur Facebook en tant qu'entreprise. Peu de personnes dans l'industrie informatique la regardent avec sympathie. Mais une comparaison de ses déclarations et du code publié montre clairement que l'objectif déclaré est un canular fondamental. Bref, ce projet n'habilite personne. Il restera complètement sous le contrôle d'une entreprise dont les activités publicitaires sont tellement mêlées de scandales et de corruption qu'il n'a d'autre choix que d'essayer de diversifier les paiements et les notations de crédit pour survivre. Un objectif clair à long terme est d'agir en tant que courtier de données et intermédiaire dans l'accès des consommateurs au crédit sur la base de leurs données personnelles sur les réseaux sociaux. Il s'agit d'une histoire complètement terrifiante et sombre, qui ne prête pas l'attention qu'elle mérite.
La seule grâce salvatrice de cette histoire est que l'artefact qu'ils ont créé est si drôle qu'il ne correspond pas à la tâche qu'il ne peut être considéré que comme un acte de fierté. Il y a plusieurs erreurs architecturales de base dans ce projet:
La résolution du problème des généraux byzantins dans un réseau avec contrôle d'accès est une conception incohérente
La tâche des généraux byzantins est un domaine de recherche assez étroit des systèmes distribués. Il décrit la capacité d'un système de réseau à résister à des défaillances arbitraires de composants lorsqu'il prend des mesures correctives essentielles au fonctionnement du système. Un réseau résilient doit résister à plusieurs types d'attaques, notamment les redémarrages, les échecs, les charges malveillantes et les votes malveillants lors des élections à la direction. C'est la principale solution pour l'architecture Libra, et elle est complètement inutile ici.
Le surcoût de la complexité temporelle de cette structure supplémentaire dépend de l'algorithme. Il y a beaucoup de littérature sur les variétés des protocoles Paxos et Raft avec la solution du problème des généraux byzantins, mais toutes ces structures introduisent des frais généraux supplémentaires pour la communication sur
maintenir un quorum. Pour la Balance, nous avons choisi l'algorithme avec le coût de communication le plus élevé possible
en cas d'échec du leadership. Et il y a des frais supplémentaires de réélection potentielle des dirigeants pour plusieurs types d'événements de défaillance du réseau.
Pour un système fonctionnant dans un consortium de sociétés transnationales hautement réglementées, où tous les utilisateurs ont un code signé Facebook et où l'accès au réseau est contrôlé par Facebook, il est tout simplement inutile de considérer les participants malveillants à un niveau consensuel. On ne sait pas pourquoi, en général, ce système résout le problème des généraux byzantins, et pas seulement maintient une piste d'audit cohérente pour vérifier la conformité. La possibilité que l'hôte Libra, géré par Mastercard ou Andressen Horrowitz, commence soudainement à exécuter du code malveillant, est un scénario de planification étrange et est mieux résolu en garantissant simplement l'intégrité du protocole et des moyens non techniques (c'est-à-dire légaux).
En témoignage pour le Congrès, le produit est déclaré concurrent de nouveaux protocoles de paiement internationaux tels que WeChat, Alipay et M-Pesa. Cependant, aucun de ces systèmes n'est conçu pour fonctionner sur des pools de valideurs pour résoudre le problème des généraux byzantins. Ils sont simplement conçus sur un bus traditionnel à haut débit qui effectue le câblage selon un ensemble fixe de règles. Il s'agit d'une approche naturelle de la conception d'un système de paiement.
Un système de paiement
bien conçu ne résout tout simplement pas le problème des doubles dépenses et des fourchettes.
Les frais généraux de l'algorithme de consensus ne résolvent aucun problème et ne limitent que la capacité du système sans autre raison que le culte du fret de la blockchain publique, qui n'est pas destiné à ce cas d'utilisation.
Libra n'a aucune confidentialité de transaction
Selon la documentation, le système est conçu en tenant compte de la
pseudonymité , c'est-à-dire que les adresses utilisées dans le protocole sont obtenues à partir de clés publiques sur des courbes elliptiques et ne contiennent pas de métadonnées sur les comptes. Cependant, nulle part dans la description de la structure de gestion de l'organisation ou dans le protocole lui-même n'indique comment les données économiques participant aux transactions seront cachées aux validateurs. Le système est conçu pour la reproduction à grande échelle de transactions pour un certain nombre de parties externes, qui, conformément aux lois européennes et américaines sur le secret bancaire, ne devraient pas être consacrées aux détails économiques.
Les politiques de données dans différents pays sont difficiles à coordonner, en particulier compte tenu des lois et réglementations disparates dans les différentes juridictions qui ont des opinions culturelles différentes sur la protection des données et la vie privée. Le protocole lui-même est par défaut complètement ouvert aux membres du consortium, ce qui est une faille technique évidente qui ne répond pas aux exigences pour lesquelles il a été développé.
Libra HotStuff BFT n'est pas en mesure d'atteindre la bande passante requise pour le système de paiement
Au Royaume-Uni, des systèmes de compensation comme BAC sont capables d'effectuer environ 580 millions de transactions par mois. Dans le même temps, des systèmes hautement optimisés comme Visa peuvent traiter 150 000 000 de transactions par jour. Les performances dépendent de la taille des transactions, du routage du réseau, de la charge du système et des
contrôles AML (lutte contre le blanchiment d'argent, programmes de blanchiment d'argent).
La Balance essaie de résoudre des problèmes qui, pour les transferts intérieurs, ne sont pas vraiment des problèmes, car les États-nations ont modernisé leur infrastructure de compensation au cours de la dernière décennie. Pour les consommateurs de détail dans l'Union européenne, le transfert d'argent n'est pas du tout un problème. Sur une infrastructure traditionnelle, cela peut être fait avec un smartphone standard en quelques secondes. Pour les grands transferts d'entreprise, il existe différents mécanismes et règles liés au mouvement de gros volumes d'argent.
Il n'y a pas de raisons techniques pour lesquelles les paiements transfrontaliers ne peuvent pas non plus être effectués instantanément, à l'exception des différences de règles et d'exigences entre les juridictions respectives. Si les mesures préventives nécessaires (due diligence du client, vérification des sanctions, etc.) sont effectuées plusieurs fois à différents stades de la chaîne de transaction, cela peut entraîner un retard dans la transaction. Cependant, ce retard est purement fonction du droit réglementaire et de son application, et non de la technologie.
Pour les consommateurs, il n'y a aucune raison pour qu'un accord au Royaume-Uni ne soit pas réglé en quelques secondes. Les transactions de détail dans l'UE ralentissent vraiment les
contrôles KYC (Know Your Customer) et les restrictions AML imposées par les gouvernements et les régulateurs, qui s'appliquent également aux paiements Balance. Même si Facebook surmonte les obstacles aux transferts internationaux et au transfert de données privées, le modèle proposé est à des centaines d'années-homme du débit des transactions mondiales et est susceptible d'être traité à partir de zéro.
La langue de Libra Move est incorrecte
Le livre blanc fait des déclarations audacieuses sur un nouveau langage non vérifié appelé Move. Ces affirmations sont assez douteuses du point de vue de la théorie des langages de programmation (PLT).
Move est un nouveau langage de programmation pour implémenter une logique de transaction personnalisée et des «contrats intelligents» sur la blockchain Libra. Comme Libra vise à servir un jour des milliards de personnes, Move est conçu avec une priorité absolue sur la sécurité.
Une caractéristique clé de Move est la possibilité de définir des types arbitraires de ressources avec une sémantique inspirée de la logique linéaire.
Dans les chaînes de blocs publiques, les contrats intelligents s'inscrivent dans la logique des réseaux publics avec des comptes bloqués, le blanchiment d'argent, la question des jetons en vente libre et les jeux de hasard. Tout cela se fait dans un langage incroyablement mal conçu appelé Solidity, qui d'un point de vue académique fait que l'auteur de PHP ressemble à un génie. Curieusement, le nouveau langage de Facebook ne semble avoir rien à voir avec ces technologies, car il s'agit en fait d'un langage de script conçu pour des tâches d'entreprise obscures.
Dans les grands livres distribués privés, les contrats intelligents sont l'un de ces termes que les consultants dispersent sans trop d'attention à des définitions ou des objectifs clairs. Les consultants en logiciels d'entreprise gagnent généralement de l'argent sur l'ambiguïté, et les contrats intelligents sont l'apothéose de l'obscurantisme d'entreprise, car ils peuvent être définis littéralement comme n'importe quoi.
Après des déclarations sur sa sécurité, nous devrions examiner la sémantique du langage. La justesse de la théorie des langages de programmation consiste généralement en deux preuves différentes: «progrès» et «préservation», qui déterminent la cohérence de tout l'espace des règles d'évaluation d'un langage. Plus précisément, dans la théorie des types, une fonction est «linéaire» si elle utilise son argument exactement une fois, et «affine» si elle ne l'utilise pas plus d'une fois. Le système de type linéaire offre une garantie statique que la fonction linéaire déclarée est vraiment linéaire, en attribuant des types à toutes les sous-expressions de fonctions et en suivant les emplacements des appels. Il s'agit d'une propriété subtile pour la preuve, et elle n'est pas facile à implémenter pour l'ensemble du programme. Le typage linéaire est toujours un domaine de recherche très académique, influencé par l'unicité des types dans Clean et la propriété de type dans Rust. Il existe quelques suggestions préliminaires pour ajouter des types linéaires au compilateur Glasgow Haskell.
L'instruction Move sur l'utilisation des types linéaires semble une immersion déraisonnable dans le compilateur, car il n'y a
pas une telle logique de vérification de type . Autant que l'on puisse en juger, le document technique cite la littérature canonique de Girard et Pierce, et dans la mise en œuvre proprement dite il n'y a rien de tel.
De plus, la sémantique formelle d'un langage supposé sûr ne se trouve nulle part ni dans l'implémentation ni dans le document. Le langage est assez petit pour trouver une preuve complète de l'exactitude de la sémantique dans Coq ou Isabelle. En réalité, le compilateur de bout en bout de la conversion complète avec le transfert des preuves en bytecode peut être implémenté à l'aide d'outils modernes inventés au cours de la dernière décennie. Nous savons comment procéder, à commencer par les
travaux de George Nekula et Peter Lee en 1996.
Du point de vue de la théorie des langages de programmation, il est impossible de vérifier l'affirmation selon laquelle Move est un langage fiable et sûr, car ces déclarations se résument uniquement à l'agitation et au marketing, et non à des preuves réelles. Il s'agit d'une situation alarmante pour un projet de développement linguistique qui est proposé de confier des milliards de dollars au traitement des transactions.
La cryptographie Balance est incorrecte
La construction de cryptosystèmes fiables est un problème d'ingénierie très complexe, et il est toujours préférable de traiter un code dangereux avec une bonne dose de paranoïa saine. Il existe des percées majeures dans ce domaine, comme le projet Microsoft Everest, qui construit une
pile TLS sécurisée vérifiable. Des outils existent déjà pour créer des primitives vérifiables. Bien qu'il soit coûteux, il ne va clairement pas au-delà des possibilités économiques de Facebook. Cependant, l'équipe a décidé de ne pas participer au projet, déclaré comme une base fiable pour le système financier mondial.
Le projet libra
s'appuie sur plusieurs bibliothèques assez nouvelles pour créer des cryptosystèmes expérimentaux, qui ne sont apparus qu'au cours des dernières années. Il est impossible de dire si les dépendances des outils suivants sont sûres ou non, car aucune de ces bibliothèques n'a été vérifiée et n'a pas de politiques de divulgation standard. En particulier, pour certaines grandes bibliothèques, il n'y a aucune certitude concernant la protection contre les attaques sur les canaux tiers et les attaques temporelles.
- ed25519-dalek
- curve25519-dalek
La bibliothèque Libra est encore plus expérimentale et va au-delà du
modèle standard en utilisant de très nouvelles méthodes telles que les fonctions aléatoires vérifiables (VRF), les paires bilinéaires et les signatures de seuil. Ces méthodes et bibliothèques peuvent être raisonnables, mais leur combinaison dans un seul système soulève de sérieuses inquiétudes quant à la surface d'attaque. La combinaison de tous ces nouveaux outils et techniques augmente considérablement la complexité des preuves de sécurité.
Il faut supposer que toute cette pile cryptographique est vulnérable à diverses attaques, jusqu'à preuve du contraire. Le modèle bien connu de Facebook «Move Fast and Break Things» ne peut pas être appliqué aux outils cryptographiques qui traitent les données financières des clients.
La Balance ne peut pas mettre en œuvre des mécanismes de protection des consommateurs
Une caractéristique distinctive du système de paiement est la possibilité d'annuler la transaction si le paiement est annulé par une action en justice ou conduit à une défaillance accidentelle ou du système. Libra est conçu pour être «entièrement complété» et n'inclut pas de type de transaction pour annuler un paiement. Au Royaume-Uni, tous les paiements de 100 à 30 000 £ sont régis par le Consumer Credit Act. Cela signifie que le système de paiement partage la responsabilité avec le vendeur en cas de problème avec les biens achetés ou si le bénéficiaire n'a pas fourni le service. Des règles similaires s'appliquent dans l'UE, en Asie et en Amérique du Nord.
La conception actuelle de la Balance ne comprend pas de protocole pour se conformer à ces lois et n'a pas de plan clair pour sa création. Pire encore, d'un point de vue architectural, la finalité de la structure des données du noyau authentifiées, basée sur l'état du disque Merkle, ne permet aucun mécanisme pour créer un tel protocole sans repenser le noyau.
Après avoir effectué un examen technique de ce projet, nous pouvons conclure qu'il ne réussira tout simplement pas le test dans une revue respectée sur la recherche de systèmes distribués ou l'ingénierie financière. Pour essayer de changer la politique monétaire mondiale, un énorme travail technique doit être fait pour créer un réseau fiable et un traitement sécurisé des données des utilisateurs, auxquels le public et les autorités de réglementation pourraient faire confiance.
Je ne vois aucune raison de croire que Facebook dans son projet a fait le travail nécessaire pour surmonter ces problèmes techniques ou qu'il a des avantages techniques sur l'infrastructure existante.
L'affirmation selon laquelle une entreprise a besoin d'une flexibilité réglementaire pour se renseigner sur les innovations n'est pas une excuse pour ne pas les faire en premier.