Dans le cadre d'une vérification formelle, Ethereum cherche à garantir la sécurité des contrats intelligents

Un nouveau mot à la mode dans le domaine de la blockchain arrive à temps pour l’automne : la vérification formelle.

L'expression (utilisée pour décrire l'application des mathématiques à la vérification des programmes logiciels) a jusqu'à présent été évoquée avec parcimonie.dans la presse. Mais si les discussions lors du sommet des développeurs d'Ethereum la semaine dernière étaient une indication, cela pourrait jouer un rôle croissant étant donné les questions de sécurité qui entourent encore les contrats intelligents et les blockchains plus largement.

Comme en témoignent les nombreuses conférences consacrées à ce sujet lors de la Devcon2, l'idée de donner de nouvelles garanties aux développeurs Ethereum est largement adoptée par la communauté des développeurs. Ce concept est déjà proposé comme un moyen d'inspirer confiance dans tous les domaines, du protocole Ethereum lui-même à sa blockchain expérimentale de preuve d'enjeu.

Ce qui s’est passé n’est peut-être pas une surprise étant donné l’effondrement soudain de The DAO cet été, à ce jour le plus grand contrat intelligent jamais lancé sur la plateforme de développement d’applications décentralisée.

Mais pendant quevérification formelle Cela peut paraître complexe, mais le concept peut peut-être être résumé succinctement comme appliqué à Ethereum : les codeurs utilisent actuellement un langage largement nouveau (Solidity) pour écrire des contrats intelligents, en écrivant des commandes qui sont ensuite traduites en bytecode pour être utilisées par la machine virtuelle Ethereum (EVM) et diffusées aux nœuds du réseau pour exécution.

Dans un sens, la vérification formelle peut être considérée comme un moyen plus objectif de garantir que lorsque différents composants du réseau reçoivent ces instructions, ils les exécutent comme prévu pour le compte des utilisateurs.

Grant Passmore, cofondateur d'Aesthetic Integration, est un entrepreneur qui voit une opportunité de contribuer à cet effort, en utilisant Devcon2 pour lancer Imandra Contracts, une plate-forme de vérification formelle pour les contrats intelligents blockchain.

Lors de l'événement, il a évoqué l'idée Ethereum pourrait servir de « paradis » pour la vérification formelle (un point de contact largement cité dans les discussions) compte tenu des objectifs de sa communauté et des responsabilités importantes qu'elle souhaite confier au code.

Passmore a déclaré à CoinDesk:

La communauté Ethereum occupe une position unique : après la DAO, nous comprenons qu'une ingénierie rigoureuse est nécessaire. L'écriture d'un contrat intelligent ne peut T être abordée comme celle d'une application web.

Ailleurs, des intervenants comme Philip Daian de Cornell ont évoqué l'intérêt pour la méthodologie de manière plus générale, déclarant au public qu'il pensait que la vérification formelle pourrait aider Ethereum à résoudre des problèmes clés.

« Ce sera un élément essentiel du projet global. J'ai hâte d'utiliser Ethereum pour établir la norme et montrer aux gens comment procéder », a-t-il déclaré.

Roues d'entraînement

Compte tenu de l’importance accordée récemment par les sociétés financières à l’explorationlangages de contrats intelligents, c'était peut-être le concept d'application de la vérification formelle à Solidity qui était le sujet de discussion le plus fréquent.

Développé pour la plateforme Ethereum , Solidity a été critiqué pour son manque de tests et sa difficulté à écrire, notamment en raison de sa nouveauté. Ces problèmes ont sans doute été amplifiés par problèmesavec le compilateur du langage, le manque de bibliothèques publiques et l’effondrement de The DAO, qui a été examiné par des membres notables de sa communauté de développement.

Dans cette optique, Christian Reitweissner, le créateur de Solidity, a reconnu qu'il existe une volonté de mettre en œuvre une vérification formelle afin que les erreurs puissent être détectées plus efficacement par les codeurs Ethereum .

Reitweissner a déclaré à CoinDesk que les développeurs de contrats intelligents pourraient un jour utiliser des outils de vérification formelle pour, par exemple, déterminer si des erreurs imprévues se produisent dans leur travail. Il a indiqué qu'un tel outil pourrait être utilisé pour déterminer si, en additionnant deux soldes, le résultat dépasse le champ alloué par le compilateur.

« Cela pourrait arriver et l'outil de vérification formelle le détecterait automatiquement. On peut le détecter très tôt et réagir en conséquence au sein du contrat intelligent », a-t-il expliqué.

Reitweissner a déclaré que l'équipe Solidity avait déjà étudié comment appliquer la vérification formelle à son travail.en octobre dernier, il existait des prototypes sur la manière dont une boîte à outils appelée Why3 pouvait être utilisée à cette fin, bien que de telles offres ne soient pas encore disponibles pour le langage complet.

Terrain d'essai

Le fait Ethereum puisse être utilisé pour tester la manière dont la vérification formelle pourrait être appliquée à la Finance de manière plus générale a également été un sujet très discuté lors de la conférence.

Passmore, par exemple, a déclaré qu'Aesthetic Integration travaillait sur l'application d'une vérification formelle dans le cadre de son travail avec les institutions financières depuis 2014, et que jusqu'à présent, les clients ont cherché à l'utiliser dans des domaines limités, comme les dark pools, où les traders ont besoin de certitude quant à l'équité.

Dans les contrats intelligents, Passmore a suggéré qu'il considérait Ethereum comme une communauté qui pourrait favoriser davantage l'acceptation.

« Lorsque nous avons commencé à travailler avec de nombreux clients du secteur bancaire, nous avons entendu dire qu'ils étaient intéressés par ce secteur, mais qu'ils s'inquiétaient de l'exactitude des contrats intelligents », a-t-il déclaré.

L'essor de la vérification formelle a également attiré Yoichi Hirai pour des raisons similaires. Ingénieur en vérification formelle, aujourd'hui employé par la Fondation Ethereum , son intérêt pour ce concept a débuté en tant que chercheur et lors de son précédent emploi chez FireEye, leader de la cybersécurité.

Lors d'une conférence, Hirai a parlé de sa frustration d'appliquer la vérification formelle dans des contextes où il n'avait pas accès au code source, ou les tâches étaient peut-être trop vastes pour faire avancer le concept.

« J'ai trouvé Ethereum, j'ai vu l'EVM, le livre jaune, la spécification, il n'y avait que 32 pages et je pensais pouvoir réellement le traduire et écrire des preuves sur les contrats intelligents », a-t-il déclaré.

Ethereum, en revanche, offre ce qu'il appelle une « spécification plus petite » et un « problème soluble » pour les ingénieurs afin de déterminer la meilleure façon de traduire Solidity en bytecode.

« Je crois que de nombreux autres chercheurs en vérification formelle sont à venir », a-t-il déclaré.

Pas de solution miracle

Malgré cet enthousiasme, des mesures sont prises pour limiter les effets de la vérification formelle. Le développeur Alex Beregszaszi, qui travaille sur les mises à niveau de l'EVM, a souligné la nécessité d'une suite de solutions pour aider les développeurs à garantir le bon fonctionnement du code des contrats intelligents.

Passmore a également noté qu'il est difficile de dire si son nouveau système aurait pu détecter les problèmes avec le DAO, car les outils de vérification formels nécessitent toujours une intervention Human .

« Vous pouvez coder les problèmes qui se sont produits avec The DAO et vérifier que vous ne les avez T , mais vous devez savoir quoi rechercher », a-t-il expliqué.

Les limites ont été reconnues par Reitweissner et Passmore, qui ont tous deux mis en garde les développeurs contre le fait de considérer la vérification formelle comme une « solution miracle ».

Reitweissner considère cependant que la méthodologie ONE à mesure qu'elle sera plus largement utilisée, les développeurs devenant progressivement plus aptes à identifier les problèmes et à développer des référentiels où la connaissance des problèmes courants peut être rendue accessible.

De cette façon, Passmore pense que la communauté Ethereum réussit à « évangéliser » le concept, ce qui, selon lui, fera finalement progresser la recherche sur la blockchain.

Passmore conclut :

« Même si beaucoup n'y ont jamais été exposés, la vérification formelle est ce dont nous avons besoin. C'est un apprentissage, mais il faut l'adopter, et c'est passionnant. »

Images via Pete Rizzo pour CoinDesk