Après deux ans, je suis revenu sur le blog pour un article qui diffère des conférences ennuyeuses habituelles sur Haskell et les mathématiques. Je travaille sur la fintech dans l'UE depuis quelques années et cela semble être le bon moment pour écrire sur un sujet qui a reçu peu d'attention de la part des médias technologiques.
Facebook a récemment publié ce qu'il appelle une « nouvelle plateforme de services financiers » appelée Libra. Il se positionne comme un système de règlement numérique basé sur un panier de devises internationales gérées sur une « blockchain » et stockées dans un pool monétaire géré depuis la Suisse. Les objectifs du projet sont ambitieux et entraînent des conséquences géopolitiques à grande échelle.
В и De nombreux articles sensés sur les hypothèses monétaires et économiques erronées qui sous-tendent le 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 personnes travaillent sur les infrastructures financières et parlent publiquement de leur travail. Ce projet ne bénéficie donc pas d'une grande couverture médiatique dans les médias technologiques, même si ses entrailles sont ouvertes sur le monde. Je veux dire open source dans les référentiels и .
Ce qui est ouvert sur le monde est un artefact architectural schizophrène prétendant être 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 s'écarte complètement de 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. Il est donc logique de supposer qu'il a été conçu avec une certaine diligence, mais en réalité, je vois un ensemble vraiment étrange de décisions architecturales qui brisent l'ensemble du système et mettent les utilisateurs en danger.
Je ne prétendrai pas avoir une opinion objective sur Facebook en tant qu’entreprise. Peu de gens dans l’industrie informatique la regardent avec sympathie. Mais une comparaison de ses déclarations avec le code publié montre clairement que le but déclaré est fondamentalement trompeur. Bref, ce projet ne responsabilise personne. Il restera entièrement sous le contrôle d'une entreprise dont l'activité publicitaire est tellement embourbée dans le scandale et la corruption qu'elle n'a d'autre choix que d'essayer de diversifier ses paiements et son crédit pour survivre. L'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. C’est une histoire absolument horrible et sombre qui ne reçoit pas l’attention qu’elle mérite.
La seule grâce salvatrice de cette histoire est que l’artefact qu’ils ont créé est tellement inadapté à la tâche à accomplir qu’il ne peut être considéré que comme un acte d’orgueil. Il y a plusieurs erreurs architecturales majeures dans ce projet :
Résoudre le problème des généraux byzantins dans un réseau de contrôle d'accès est une conception incohérente
Le problème des généraux byzantins est un domaine de recherche plutôt restreint sur les systèmes distribués. Il décrit la capacité d'un système réseau à résister aux pannes aléatoires de composants tout en prenant 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 pannes, les charges malveillantes et les votes malveillants lors des élections à la direction. C’est la décision principale pour l’architecture Libra, et elle n’a absolument aucun sens ici.
La complexité temporelle de cette structure supplémentaire dépend de l’algorithme. Il existe de nombreuses publications sur les variantes des protocoles Paxos et Raft résolvant le problème des généraux byzantins, mais toutes ces structures introduisent une surcharge supplémentaire pour la communication via 
pour maintenir le quorum. Pour Libra, ils ont choisi un algorithme avec le coût de communication le plus élevé possible en cas d'échec du leadership. Et la réélection potentielle des dirigeants en cas de multiples types d’événements de défaillance du réseau entraîne une surcharge supplémentaire.
Pour un système fonctionnant au sein d’un consortium de sociétés multinationales hautement réglementées, où tous les utilisateurs ont un code signé par Facebook et où l’accès au réseau est contrôlé par Facebook, cela n’a tout simplement pas de sens de considérer les participants malveillants au niveau du consensus. On ne sait pas vraiment pourquoi ce système résoudrait le problème des généraux byzantins, plutôt que de simplement maintenir une piste d'audit cohérente pour vérifier la conformité. La possibilité qu'un nœud Libra géré par Mastercard ou Andressen Horrowitz commence soudainement à exécuter du code malveillant est un scénario étrange à planifier et il est préférable de le résoudre en garantissant simplement l'intégrité du protocole et des moyens non techniques (c'est-à-dire légaux).
Un témoignage devant le Congrès a présenté le produit comme un concurrent des 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 validateurs afin de résoudre le problème des généraux byzantins. Ils sont simplement conçus sur un bus traditionnel à large bande passante qui effectue le câblage selon un ensemble de règles fixes. Il s’agit d’une approche naturelle pour concevoir un système de paiement. Bien conçu le système de paiement ne rencontrera tout simplement pas le problème des doubles dépenses et des fourchettes.
La surcharge de l’algorithme de consensus ne résout aucun problème et ne fait que limiter le débit du système sans autre raison que le culte du cargo de la blockchain publique, qui n’est pas prévue pour ce cas d’usage.
La Balance n'a pas de confidentialité des transactions
Selon la documentation, le système est conçu en tenant compte pseudonymat, 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 gouvernance de l’organisation ou dans le protocole lui-même n’indique-t-il comment les données économiques impliquées dans les transactions seront cachées aux validateurs. Le système est conçu pour reproduire des transactions à grande échelle auprès d'un ensemble de parties externes qui, en vertu des lois européennes et américaines en vigueur sur le secret bancaire, ne devraient pas être au courant des détails économiques.
Les politiques en matière de données entre les pays sont difficiles à coordonner, en particulier en raison des lois et réglementations disparates dans différentes juridictions avec des visions culturelles différentes sur la protection des données et la confidentialité. Le protocole lui-même est par défaut entièrement ouvert aux membres du consortium, ce qui constitue une lacune technique évidente qui ne répond pas aux exigences pour lesquelles il a été conçu.
Libra HotStuff BFT n'est pas en mesure d'atteindre le débit requis pour un système de paiement
Au Royaume-Uni, les systèmes de compensation comme BAC sont capables de traiter environ 580 millions de transactions par mois. Dans le même temps, des systèmes hautement optimisés comme Visa peuvent traiter 000 000 150 de transactions par jour. Les performances varient en fonction de la taille de la transaction, du routage réseau, de la charge du système et (lutte contre le blanchiment d'argent, dispositifs de blanchiment d'argent).
La Libra tente de résoudre des problèmes qui ne concernent pas vraiment les transferts nationaux, car les États-nations ont modernisé leur infrastructure de compensation au cours de la dernière décennie. Pour les consommateurs de détail de l’Union européenne, transférer de l’argent ne pose aucun problème. Sur une infrastructure traditionnelle, cela peut être réalisé avec un smartphone standard en quelques secondes. Pour les transferts de grandes entreprises, il existe divers mécanismes et règles associés au transfert de grosses sommes d’argent.
Il n’existe aucune raison technique pour laquelle les paiements transfrontaliers ne peuvent pas également être traités instantanément, hormis les différences de règles et d’exigences entre les juridictions concernées. Si les mesures préventives nécessaires (due diligence client, contrôle des sanctions, etc.) sont appliquées à plusieurs reprises à différentes étapes de la chaîne de transaction, cela peut entraîner un retard dans la transaction. Cependant, ce retard est purement fonction de la législation réglementaire et de sa conformité, et non de la technologie.
Pour les consommateurs, il n’y a aucune raison pour qu’une transaction au Royaume-Uni ne soit pas réglée en quelques secondes. Les transactions de détail dans l’UE ralentissent en effet (Know Your Customer) et restrictions AML imposées par les gouvernements et les régulateurs, qui s'appliquent également aux paiements Libra. Même si Facebook parvenait à surmonter les obstacles aux transferts transfrontaliers et aux transferts de données privées, le modèle proposé est à des centaines d’années-personnes du débit mondial des transactions et devrait probablement être repensé à partir de zéro.
La langue de Libra Move est incorrecte
Le livre blanc fait des déclarations audacieuses sur un nouveau langage non testé 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 permettant d'implémenter une logique de transaction personnalisée et des contrats intelligents sur la blockchain Libra. Parce que Libra vise à servir un jour des milliards de personnes, Move est conçu avec la sécurité comme priorité absolue.
Une caractéristique clé de Move est la possibilité de définir des types de ressources arbitraires avec une sémantique inspirée de la logique linéaire.
Dans les blockchains publiques, les contrats intelligents sont confrontés à la logique des réseaux publics avec des comptes séquestres, du blanchiment d'argent, de l'émission de jetons OTC et des jeux de hasard. Tout cela est fait dans un langage étonnamment mal conçu appelé Solidity, qui, d'un point de vue académique, fait passer l'auteur de PHP pour un génie. Curieusement, le nouveau langage de Facebook semble n'avoir rien à voir avec ces technologies, puisqu'il s'agit en fait d'un langage de script destiné à des fins commerciales obscures.
Dans les registres distribués privés, les contrats intelligents sont l’un de ces termes utilisés par les consultants sans vraiment se soucier d’une définition ou d’un objectif clair. Les consultants en logiciels d’entreprise gagnent généralement de l’argent grâce à l’ambiguïté, et les contrats intelligents sont l’apothéose de l’obscurantisme des entreprises car ils peuvent être définis littéralement comme n’importe quoi.
Après avoir affirmé sa sécurité, nous devons examiner la sémantique du langage. L'exactitude dans la théorie des langages de programmation consiste généralement en deux preuves différentes : le « progrès » et la « préservation », qui déterminent la cohérence de l'ensemble de l'espace des règles d'évaluation du 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 l'utilise au plus une fois. Le système de types linéaires fournit une garantie statique qu'une fonction linéaire déclarée est véritablement linéaire en attribuant des types à toutes les sous-expressions de fonction et en gardant une trace de l'endroit où les appels sont effectués. Il s’agit d’une propriété subtile à prouver et qui n’est pas facile à mettre en œuvre pour l’ensemble d’un programme. Le typage linéaire est encore un domaine d'étude très académique, influencé par l'implémentation de l'unicité de type dans Clean et de la propriété de type dans Rust. Il existe quelques propositions préliminaires pour ajouter des types linéaires au compilateur Glasgow Haskell.
La déclaration de Move sur l'utilisation des types linéaires semble être une plongée injustifiée dans le compilateur, car il . Pour autant que l'on puisse en juger, le livre blanc cite la littérature canonique de Girard et Peirce, et il n'y a rien de similaire dans la mise en œuvre réelle.
De plus, la sémantique formelle du langage prétendument sécurisé n’apparaît nulle part dans l’implémentation ou dans le document. Le langage est suffisamment petit pour trouver une preuve complète de sémantique correcte en Coq ou Isabelle. En réalité, un compilateur de conversion complète de bout en bout avec transfert de preuve en bytecode est tout à fait possible à mettre en œuvre avec des outils modernes inventés au cours de la dernière décennie. Nous savons comment faire, à commencer par en 1996.
Du point de vue de la théorie des langages de programmation, il est impossible de tester l’affirmation selon laquelle Move est un langage fiable et sécurisé, car ces affirmations se résument à de simples gestes de la main et à du marketing plutôt qu’à des preuves réelles. Il s’agit d’une situation alarmante pour un projet linguistique chargé de traiter des milliards de dollars de transactions.
La cryptographie de la Balance est défectueuse
Construire des systèmes cryptographiques sécurisés est un problème d'ingénierie très difficile, et il est toujours préférable d'aborder le travail avec du code dangereux avec une bonne dose de paranoïa saine. Il existe des avancées majeures dans ce domaine, comme le projet Microsoft Everest, qui construit un système sécurisé vérifiable. . Des outils existent déjà pour créer des primitives vérifiables. Même si cela coûte cher, cela ne dépasse clairement pas les capacités économiques de Facebook. Cependant, l’équipe a décidé de ne pas participer au projet, annoncé comme une base fiable pour le système financier mondial.
projet Balance à partir de plusieurs bibliothèques relativement nouvelles pour créer des cryptosystèmes expérimentaux qui ne sont apparus que ces dernières années. Il est impossible de dire si les dépendances sur les outils suivants sont sûres ou non, puisqu'aucune de ces bibliothèques n'a été auditée et n'a pas de politiques de divulgation standard. En particulier, pour certaines bibliothèques principales, il n'existe aucune certitude quant à la protection contre les attaques par canal secondaire et les attaques temporelles.
La bibliothèque Libra devient encore plus expérimentale et va au-delà , appliquant des techniques très nouvelles 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 les combiner toutes en 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é de la preuve de sécurité.
Il faut supposer que l’ensemble de cette pile cryptographique est vulnérable à diverses attaques jusqu’à preuve du contraire. Le célèbre modèle « Move Fast and Break Things » de Facebook ne peut pas être appliqué aux outils cryptographiques qui traitent les données financières des clients.
La Libra ne parvient 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 une transaction si le paiement est annulé par un procès ou entraîne une panne accidentelle ou du système. Le système Libra est conçu pour être « complet » et n'inclut pas de type de transaction pour l'annulation du paiement. Au Royaume-Uni, tous les paiements compris entre 100 £ et 30,000 XNUMX £ sont soumis à la loi sur le crédit à la consommation. Cela signifie que le système de paiement partage la responsabilité avec le vendeur en cas de problème avec le produit acheté ou si le destinataire du paiement ne fournit pas le service. Des règles similaires s’appliquent dans l’UE, en Asie et en Amérique du Nord.
La conception actuelle de Libra n’inclut pas de protocole pour se conformer à ces lois et ne prévoit pas de plan clair pour en créer un. Pire encore, d'un point de vue architectural, la finalité de la structure de données authentifiées du noyau, basée sur l'état du lecteur Merkle, ne permet à aucun mécanisme de 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 sera tout simplement pas retenu dans aucune revue respectée de recherche sur les systèmes distribués ou d’ingénierie financière. Pour tenter de changer la politique monétaire mondiale, un énorme travail technique doit être réalisé pour créer un réseau fiable et un traitement sécurisé des données des utilisateurs auxquels le public et les régulateurs peuvent avoir confiance.
Je ne vois aucune raison de croire que Facebook a fait le travail nécessaire dans sa conception pour surmonter ces problèmes techniques ou qu'il présente des avantages techniques par rapport à l'infrastructure actuelle. Dire qu’une entreprise a besoin de flexibilité réglementaire pour explorer les innovations n’est pas une excuse pour ne pas les faire en premier.
Source: habr.com