(1) L’art De L’itération
Les crypto-monnaies sont des protocoles implémentés sous forme de logiciels. Les protocoles sont simplement des conversations intelligentes entre les participants. Le logiciel est en fin de compte la manipulation de données avec un objectif. Pourtant, la différence entre un logiciel solide et fiable ainsi que des protocoles utiles et sécurisés et leur inverse est tout à fait humaine.
Un bon logiciel a besoin de responsabilité, d’exigences commerciales claires, de processus reproductibles, de tests approfondis et d’itérations inlassables. Un bon logiciel a également besoin de développeurs raisonnablement talentueux possédant suffisamment de connaissances spécifiques au domaine pour concevoir correctement un système capable de résoudre complètement tout problème qu’ils essaient de résoudre.
Quant aux protocoles utiles et sécurisés, en particulier ceux impliquant la cryptographie et les systèmes distribués, ils commencent par un processus plus académique et axé sur les normes. Un examen par les pairs, des débats sans fin et un concept ferme de compromis sont nécessaires pour garantir l’utilité d’un protocole. Pourtant, ces seuls ne sont pas suffisants, les protocoles doivent être mis en œuvre et testés par une utilisation réelle.
Le défi unique dans l’industrie de la crypto-monnaie est que deux philosophies complètement différentes sont mutilées sans une synthèse hégélienne appropriée. Notre thèse est une mentalité de startup “avancer vite et casser les choses” animée par la jeunesse, la cupidité et la passion. L’antithèse est une approche lente, méthodique et académique motivée par le désir de solidifier les innovations de notre espace dans une belle niche bénéficiant d’un financement et d’un prestige suffisants.
Le résultat est que de nombreuses crypto-monnaies sont soit entièrement spécifiées sur un livre blanc uniquement pertinent pour un CV, soit simplement par un code écrit à la hâte. Aucun des dix premiers actuels. les crypto-monnaies par capitalisation boursière sont basées sur un protocole évalué par des pairs. Aucune des dix principales crypto-monnaies actuelles n’a été implémentée à partir d’une spécification formelle.
Pourtant, des milliards de dollars de valeur sont en jeu. Une fois déployée, une crypto-monnaie est extrêmement difficile à changer. Comment un utilisateur sait-il qu’il utilise un système sécurisé ? Comment un utilisateur sait-il que les allégations marketing sont légitimes ? Que se passe-t-il si le protocole proposé ne peut jamais réaliser les revendications ?
Ce manque de synthèse et de respect du processus est l’une des principales raisons pour lesquelles IOHK a voulu construire Cardano. Notre espoir était de développer un projet de référence qui servirait d’exemple sur la façon de faire les choses de manière plus efficace, saine et honnête.
Le but n’est pas de proposer une manière totalement nouvelle de développer des logiciels et des protocoles, mais plutôt de reconnaître que de grands logiciels et protocoles existent déjà et que nous pouvons imiter les conditions qui ont conduit à leur création. Deuxièmement, rendre ces conditions publiquement connues et open source si possible afin qu’elles puissent être imitées au profit de l’ensemble du domaine.
(2) Faits Et Opinions
L’autre préoccupation est de savoir où s’arrêtent les faits et où commence l’opinion. Il existe des centaines de langages de programmation, des dizaines de paradigmes de développement et plus d’une philosophie de gestion de projet. Le monde universitaire est criblé de ses propres défis découlant de son éloignement des préoccupations commerciales et de l’aspect pratique.
Pour Cardano, nous avons d’abord tenté de saisir les lacunes évidentes qui peuvent être universellement reconnues comme étant utiles d’un point de vue technique. Par exemple, la cryptographie et les systèmes distribués sont tous deux des sujets extraordinairement impliqués avec beaucoup trop d’exemples de la façon dont des mains naïves peuvent faire des erreurs horribles. Par conséquent, tout protocole nécessitant un aperçu de ces domaines doit être conçu par un expert reconnu et être soumis pour examen par d’autres experts.
Ouroboros est notre première étude de cas dans ce domaine. Il a été conçu par une équipe de cryptographes avec un historique de publication important, diversifié et publiquement vérifiable. Il a été construit selon le processus de cryptographie standard, avec des hypothèses de sécurité, un modèle contradictoire et des preuves. Ces preuves ont été vérifiées par soumission à des conférences et aussi indépendamment par des épreuves informatiques écrites en Isabelle par une équipe de l’Université de Cambridge.
Pourtant, ce travail à lui seul ne fournit aucune garantie d’utilité - juste une vérification rigoureuse d’un modèle de sécurité compte tenu de certaines hypothèses. Pour être utile, il faut implémenter et tester le protocole. Nos développeurs l’ont fait à la fois dans Haskell et aussi dans Rust. Ce travail a révélé que davantage d’efforts devaient être concentrés sur le modèle de synchronisation, ce qui a conduit à la création d’Ouroboros Praos.
Cet art de l’itération est ce qui produit d’excellents protocoles, chaque étape menant à de nouvelles leçons et à l’obligation de revérifier l’exactitude de l’étape précédente. C’est coûteux, long et parfois vraiment fastidieux, mais il est nécessaire de s’assurer qu’un protocole est correctement conçu.
Les protocoles - en particulier ceux qui doivent être utilisés par des milliards de personnes - ne sont pas de courte durée et évoluent rapidement. Ils sont plutôt destinés à être suivis pendant des années, voire des décennies. Il semble tout à fait raisonnable qu’avant d’accabler le monde d’un nouveau système financier avec lequel nous devrons tous vivre pendant les 100 prochaines années, nous voulions exiger un peu d’ennui et de rigueur de la part de ses concepteurs.
(3) Functional Sins
En pénétrant dans un territoire plus opiniâtre, les outils, les langages et les méthodologies utilisés dans le développement de logiciels sont davantage des artefacts de la providence religieuse que la réalité objective. Le code source est comme la prose écrite. Tout le monde a une opinion sur ce qui est bon – et ce qui est communiqué est parfois moins important que la manière dont il est communiqué.
Nous devons commettre le péché de choisir un camp en acceptant qu’il sera mauvais aux yeux d’au moins une personne. Cependant, il y a au moins un large corpus de justification derrière notre choix.
Les protocoles rendant Cardano possible sont mis en œuvre dans Haskell. L’interface utilisateur a été encapsulée dans un fork d’Electron que nous appelons Daedalus. Nous avons choisi d’utiliser le modèle d’architecture Web dans la mesure du possible, et pour notre base de données, nous avons opté pour un paradigme clé-valeur utilisant RocksDB.
Au niveau des composants, cette abstraction signifie que la maintenance est beaucoup plus simple, une meilleure technologie peut être remplacée plus tard avec peu d’effort, et que notre pile est en partie liée aux efforts de développement de Github et Facebook.
L’utilisation d’un WebGuI nous permet de tirer parti de React et de développer des fonctionnalités frontales à l’aide d’outils compris par des centaines de milliers de développeurs JavaScript. L’utilisation d’une architecture Web signifie que les composants peuvent être traités comme des services et que le modèle de sécurité est judicieux.
Choisir Haskell pour le développement de protocoles a été le choix le plus difficile. Même dans le monde fonctionnel, il existe de nombreux choix. Du côté plus flexible et impur, il y a des langages comme Clojure, Scala et F #, qui bénéficient des énormes bibliothèques de Java et des écosystèmes .Net tout en préservant certains des meilleurs aspects de la programmation fonctionnelle.
Il existe des langues plus académiques telles que Agda et Idris qui ont un lien étroit avec des techniques qui permettraient une vérification solide de l’exactitude. Pourtant, ils manquent de bibliothèques raisonnables et ont une expérience de développement médiocre.
Pour Cardano, le choix s’est porté sur Ocaml et Haskell. Ocaml est un langage merveilleux avec une grande communauté, un bon outillage, une expérience de développement raisonnable et un grand héritage dans l’espace de vérification formelle via Coq. Alors pourquoi avons-nous choisi Haskell ?
(4) Pourquoi Haskel ?
Les protocoles qui composent Cardano sont distribués, associés à la cryptographie et nécessitent un degré élevé de tolérance aux pannes. Les meilleurs jours, il y aura toujours des acteurs byzantins, des messages malformés et des clients défectueux causant involontairement une forme de ravage sur le réseau.
Tout d’abord, nous voulions un langage qui bénéficie d’un système de typage fort où nous pourrions facilement utiliser des outils tels que Quickcheck et des techniques plus élaborées telles que les types de raffinement tout en ayant une attente raisonnable de tolérance aux pannes. Un modèle OTP de style Erlang satisfait ce dernier alors que des langages comme Haskell et Ocaml satisfont le premier.
- Avec l’introduction de Cloud Haskell, Haskell a acquis de nombreux avantages d’Erlang sans renoncer aux siens. De plus, la modularité et la composabilité de Haskell nous ont permis d’utiliser une bibliothèque sur mesure plus légère appelée Time Warp pour Cardano.
- Deuxièmement, les bibliothèques de Haskell ont beaucoup évolué ces dernières années grâce au travail approfondi d’entités commerciales telles que Galois , FP Complete et Well-Typed . Par conséquent, Haskell peut être utilisé pour écrire des applications de production24.
- Troisièmement, l’évolution rapide de PureScript a fourni un pont indispensable vers le monde JavaScript, semblable à ce que Clojurescript a donné à Clojure. Nous nous attendons à ce que PureScript soit particulièrement important lorsqu’il s’agit de faire fonctionner Cardano dans un navigateur et de développer des portefeuilles mobiles.
- Quatrièmement, en ce qui concerne la résolution des dépendances, Haskell a bénéficié ces dernières années d’un effort social et technologique important mené par des technologues comme Michael Snoyman via une plate-forme appelée stackage qui est à la fois facile à utiliser et bien prise en charge par FP Complete.
- Cinquièmement, au-delà de la résolution adéquate des dépendances, nous visons à ce que nos versions logicielles soient reproductibles. En d’autres termes, avec les mêmes valeurs de configuration et versions de dépendance, il devrait produire exactement les mêmes artefacts de construction. Grâce à l’empilement, nous avons utilisé NixOps pour atteindre la reproductibilité avec un grand succès.
- Enfin, le vivier de talents de développeurs spécialisés dans Haskell est raisonnablement important - par rapport à ses pairs - et assez bien formé avec la bonne combinaison de diplômes universitaires et industriels. Il agit également comme un filtre de compétences car il est rare de trouver des développeurs Haskell expérimentés sans connaissances détaillées en informatique.
(5) Spécification Formelle Et Vérification
L’un des points forts du développement d’un protocole utilisant un modèle de sécurité dont l’exactitude est prouvée est qu’il fournit une limite garantie de pouvoir contradictoire. On reçoit un contrat selon lequel tant que le protocole est suivi et que les preuves sont correctes, l’adversaire ne peut pas violer les propriétés de sécurité revendiquées.
Une réflexion plus approfondie rend l’affirmation précédente encore plus significative. Les adversaires peuvent être arbitrairement intelligents et capables. Dire qu’ils sont vaincus uniquement par un modèle mathématique est extraordinaire. Et, bien sûr, ce n’est pas tout à fait vrai.
La réalité introduit des facteurs et des circonstances qui empêchent l’utopie de la sécurité pure et du comportement correct d’exister. Les implémentations peuvent être erronées. Le matériel peut introduire des vecteurs d’attaque précédemment ignorés. Le modèle de sécurité peut être insuffisant et non conforme à une utilisation réelle.
Un jugement est nécessaire sur le degré de spécification, de rigueur et de vérification requis pour un protocole. Par exemple, des efforts comme le projet SeL4 Microkernel sont un excellent exemple d’un assaut total contre l’ambiguïté nécessitant près de 200 000 lignes de code Isabelle pour vérifier moins de 10 000 lignes de code C. Pourtant, un noyau de système d’exploitation est une infrastructure critique qui pourrait constituer une grave vulnérabilité de sécurité s’il n’est pas correctement mis en œuvre.
Tous les logiciels cryptographiques devraient-ils nécessiter le même effort herculéen ? Ou peut-on choisir une voie moins vigoureuse qui produit des résultats équivalents ? Est-il également important que le protocole soit parfaitement implémenté si l’environnement dans lequel il s’exécute est notoirement vulnérable, comme sous Windows XP ?
Pour Cardano, nous avons choisi le compromis suivant.
- Premièrement, en raison de la nature complexe des domaines de la cryptographie et de l’informatique distribuée, les preuves ont tendance à être très subtiles, longues, compliquées et parfois assez techniques. Cela implique que la vérification par l’homme peut être fastidieuse et sujette aux erreurs. Par conséquent, nous pensons que chaque preuve significative présentée dans un livre blanc rédigé pour couvrir l’infrastructure de base doit être vérifiée par machine.
- Deuxièmement, pour vérifier le code Haskell afin qu’il corresponde correctement à nos livres blancs, nous pouvons choisir entre deux options populaires : l’interface avec les prouveurs SMT via LiquidHaskell et l’utilisation d’Isabelle/HOL.
Les solveurs SMT (satisfiability modulo theories) traitent le problème de trouver des paramètres fonctionnels qui satisfont une équation ou une inéquation, ou encore de montrer que de tels paramètres n’existent pas. Comme discuté par De Moura et Bjørner, les cas d’utilisation de SMT sont variés, mais le point clé est que ces techniques sont à la fois puissantes et peuvent réduire considérablement les bogues et les erreurs sémantiques.
Isabelle/HOL, en revanche, est un outil plus expressif et diversifié qui peut être utilisé à la fois pour spécifier et vérifier la mise en œuvre. Isabelle est un solveur de théorème générique travaillant avec des constructions logiques d’ordre supérieur, capable de représenter des ensembles et d’autres objets mathématiques à utiliser dans les preuves. Isabelle elle-même s’intègre au prouveur Z3 SMT pour travailler avec des problèmes impliquant de telles contraintes.
Les deux approches apportent de la valeur et nous avons donc décidé de les adopter toutes les deux par étapes. Les preuves écrites humaines seront encodées dans Isabelle pour vérifier leur exactitude, satisfaisant ainsi notre exigence de vérification par machine. Et nous avons l’intention d’ajouter progressivement Liquid Haskell à tout le code de production dans la mise en œuvre de Cardano tout au long de 2017 et 2018.
Enfin, la vérification formelle n’est aussi bonne que la spécification à partir de laquelle on vérifie et les outils disponibles. L’une des principales raisons de choisir Haskell est qu’il offre le bon équilibre entre pratique et théorie. La spécification dérivée des livres blancs ressemble beaucoup au code Haskell, et relier les deux est considérablement plus facile que de le faire avec un langage impératif.
Il est toujours très difficile de capturer une spécification appropriée et de mettre à jour la spécification lorsque des modifications telles que des mises à niveau, des corrections de bogues et d’autres préoccupations doivent être apportées ; cependant, cette réalité ne diminue en rien la valeur globale. Si l’on se donne la peine de construire une fondation sur une sécurité prouvable, alors la mise en œuvre devrait être ce qui a été réellement proposé sur papier.
(6) Transparence
Une dernière question lors de l’examen de la science et de l’ingénierie du développement d’une crypto-monnaie est de savoir comment aborder la transparence. Les décisions de conception ne sont pas booléennes et éthérées, venant aux développeurs dans les rêves et devenant soudainement canon. Ils sont issus de l’expérience, des débats et des enseignements tirés des erreurs antérieures.
Le défi est qu’un processus de développement totalement transparent pourrait influencer la discussion pour qu’elle devienne plus théâtrale que fondée sur des preuves. Les égos, les tentatives de gagner une communauté et la peur de paraître stupide pourraient forcer les conversations à devenir stériles et contre-productives.
De plus, des étrangers pourraient tenter de coopter la conversation dans le but de forcer leur tangente particulière à devenir le seul sujet pertinent. Tout le monde a une vache sacrée.
Alors, comment concilier le besoin d’un processus de développement transparent, qui est dû à la communauté qui a confié le progrès à un ensemble de développeurs principaux, avec le besoin d’une liberté d’expression sans crainte ?
Avec Cardano, nous avons décidé d’adopter un processus axé sur les normes avec une surveillance dirigée. La communauté doit savoir que la science et le code sont bien pensés, vérifiés et résolvent réellement les problèmes que les développeurs prétendent résoudre. À cette fin, l’examen par les pairs devrait satisfaire complètement la composante scientifique car il a été conçu spécifiquement à cette fin et nous a donné le monde moderne.
Pour le code, ce sujet est un peu plus opiniâtre. Pour Cardano, nous avons choisi de confier à la Fondation Cardano le rôle d’auditeur final du travail d’IOHK. Ils sont notamment chargés des missions suivantes :
- Examen régulier du code source contenu dans le Cardano Github pour vérifier la qualité, la couverture des tests, les commentaires appropriés et l’exhaustivité
- Examen de toute la documentation Cardano pour l’exactitude et l’utilité
- Vérifier les affirmations selon lesquelles les protocoles produits par les scientifiques sont pleinement mis en œuvre
Pour accomplir cette tâche, IOHK soumettra des rapports réguliers et opportuns à la Fondation - et à ses ayants droit - pour examen. La Fondation publiera à son tour un rapport de surveillance du développement à la communauté Cardano au moins une fois par trimestre.
Ce premier effort vise à lancer une conversation plus large sur la manière dont un projet décentralisé parvient à rendre des comptes. La supervision du développement par un tiers de confiance est un outil puissant pour s’assurer que les développeurs sont sur la bonne voie, mais cela ne suffit pas pour garantir complètement que le projet sera toujours livré.
Pour cette raison, après l’intégration de la trésorerie dans CSL, la Fondation encouragera des équipes de développement supplémentaires à construire des clients alternatifs basés sur les spécifications formelles développées conjointement avec IOHK. La diversité de développement a été une excellente technique utilisée par le projet Ethereum pour éviter la formation d’une monoculture autour d’un seul ensemble d’idées ou de développeurs.
En ce qui concerne les spécifications, il y a une mine de connaissances à tirer du processus de normalisation suivi par le WC3 et l’IETF . En fin de compte, chaque protocole intégré par Cardano nécessite une spécification indépendante du travail académique ou du code source. Il doit plutôt être dans un format approprié tel qu’un RFC.
L’un des principes fondamentaux de la Fondation Cardano est d’agir en tant qu’organisme de normalisation spécifiquement pour les protocoles Cardano et d’héberger des conversations pour mettre à jour, ajouter ou modifier les normes pertinentes pour Cardano. Si Internet (un produit de normes) via l’IETF peut parvenir à un consensus sur les protocoles de base à utiliser, il est tout à fait raisonnable de supposer qu’un organisme dédié pourrait faciliter le même résultat.
En guise de conclusion, il est intéressant d’explorer le déplacement de ces discussions vers une entité décentralisée hébergée sur une blockchain. Ce concept s’appelle une organisation autonome décentralisée (DAO) et des travaux préliminaires sont en cours dans ce domaine. IOHK développera un modèle DAO de référence pour les entités s’interfaçant avec Cardano à utiliser si nécessaire et c’est la prérogative de la Fondation Cardano de décider de l’adopter ou non dans le cadre de son mandat de normes.
Source : https://why.cardano.org/en/science-and-engineering/the-art-of-iteration/