Rejoignez-Nous sur

Vérification officielle des spécifications Ethereum 2.0 Phase 0 | par ConsenSys | Août 2020

News

Vérification officielle des spécifications Ethereum 2.0 Phase 0 | par ConsenSys | Août 2020

Une mise à jour de ConsenSys R&D sur leurs efforts pour apporter la fiabilité à la chaîne Beacon et aux fondations fondamentales d'Eth2.

ConsenSys

Vérification vs test

Nous avons utilisé le primé langage de programmation prenant en charge la vérification Dafny écrire un (fonctionnel et logique) spécification de chaque fonction Beacon Chain, un la mise en oeuvre de chaque fonction, et que l'implémentation est conforme à sa spécification. En d'autres termes, nous avons vérifié mathématiquement l'absence de bogues. Les implémentations que nous avons finalement prouvées correctes sont basées sur les spécifications officielles Eth2.0 avec la mise en garde que nous avons corrigé et signalé quelques bogues et incohérences.

Propriétés que nous avons prouvées

Les propriétés vont de l'absence de arithmétique sous / débordements et index hors limites, la conformité de chaque fonction aux pré / post-conditions logiques (logique du premier ordre) ( exemple merkelise ici), à des plus complexes impliquant des compositions de fonctions. Par exemple, nous avons les éléments suivants propriété de la SSZ Sérialiser / désérialiser fonctions: pour chaque objet x, Deserialise (Serialise (x)) = x, c'est-à-dire que la désérialisation d'un objet sérialisé renvoie l'objet d'origine. Nous avons également établi un nombre d'invariants, et les a utilisées pour prouver que les opérations de base de Beacon Chain et ForkChoice ( state_transition, on_block) réellement construire une chaîne de blocs: pour tout bloc b du magasin, les ancêtres de b forment une séquence finie totalement ordonnée menant au bloc de genèse, qui est la propriété principale d'une blockchain!

Tout méthodiste formel insisterait sur le fait que la vérification est une pratique exemplaire en matière de sécurité. Voici exactement comment cette méthodologie garantit une infrastructure sécurisée et digne de confiance pour Ethereum 2.0.

Spécification fonctionnelle

Tout d'abord, nous avons élevé les spécifications officielles Eth2.0 à un spécification logique et fonctionnelle formelle. Pour chaque fonction, nous définissons formellement ce que la fonction est censée calculer, pas comment. Cela fournit Spécifications de référence conviviales pour les développeurs indépendantes du langage qui peut être utilisé pour développer des implémentations plus sécurisées, avec moins d'effort.

Modularité

Deuxièmement, nos spécifications, implémentations et architecture de preuve sont. En conséquence, nous pouvons facilement expérimenter de nouvelles implémentations (par ex. optimisations) et vérifier leur impact sur l'ensemble du système. Pensez à un hack astucieux pour implémenter une fonction? Modifiez l'implémentation et demandez à Dafny de vérifier qu'elle est toujours conforme à ses spécifications. Si c'est le cas, les preuves des composants qui utilisent cette fonction ne sont pas impactées.

Exécutabilité

Troisièmement, nos implémentations sont exécutable. Nous pouvons compiler et exécuter un programme Dafny. Encore mieux, tu peux automatiquement générer du code dans certains langages de programmation populaires comme C #, Go (et bientôt Java) à partir du code Dafny. Cela peut être utilisé pour compléter les bases de code existantes ou pour générer tests certifiés. L'implémentation à tester peut utiliser nos fonctions prouvées correctes pour calculer le résultat attendu d'un test et le comparer à son propre résultat.

Tout dans une seule langue

Enfin, notre base de code est autonome. Il contient les spécifications, implémentations, documentations et preuves, le tout dans un langage de programmation unique, lisible, simple et sémantiquement bien défini.

Qu'en est-il de la solidité du moteur de vérification?

Vous vous demandez peut-être: «Et si le compilateur / vérificateur Dafny est bogué?» Nous savons en fait que Dafny est en buggy (problèmes de repo dafny), mais nous ne nous appuyons pas sur l'absence de bugs dans Dafny. Nous comptons sur Dafny (et son moteur de vérification) pour être. La solidité signifie que lorsque Dafny rapporte que les preuves sont correctes, elles sont effectivement correctes.

Et si la spécification que nous avons écrite n'est pas la bonne?

Dans ce cas, nous prouverions la conformité à une mauvaise exigence. Oui, cela peut arriver et il n'y a pas de solution miracle pour résoudre ce problème. Cependant, comme nous l'avons mentionné précédemment, Dafny est exécutable. Cela nous permet d'exécuter le code et de nous assurer que nos spécifications sont les bonnes. Et nos spécifications sont écrites dans une logique de premier ordre sans possibilité de contestation sur la signification, donc si vous remarquez un problème, faites-le nous savoir et nous le réglerons.

Et si Dafny ne peut pas prouver qu'une implémentation est conforme à une spécification?

Cela peut arriver, mais dans ce cas, Dafny dispose de certains mécanismes de rétroaction pour aider à déterminer quelles étapes d'une preuve ne peuvent pas être vérifiées. Et jusqu'à présent, nous avons toujours réussi à construire des preuves que Dafny peut vérifier automatiquement.
Nous apprécions vos commentaires, veuillez donc vérifier notre référentiel eth2.0-dafny. Nous avons été ravis de voir le développement d'Ethereum 2.0 atteindre ses récents jalons de testnet, et nous sommes impatients de travailler avec des équipes de tout l'écosystème pour nous assurer que la prochaine phase du réseau repose sur une base solide.



Traduction de l’article de ConsenSys : Article Original

BlockBlog

Le Meilleur de l'Actualité Blockchain Francophone & Internationale | News, Guides, Avis & Tutoriels pour s'informer et démarrer facilement avec Bitcoin, les Crypto-Monnaies et le Blockchain. En Savoir Plus sur L'Équipe BlockBlog

Commenter cet Article

Commenter cet Article

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *

Plus dans News

Les Plus Populaires

Acheter des Bitcoin

Acheter des Alt-Coins

Sécuriser vos Cryptos

Vêtements et Produits Dérivés

Top
massa ut dapibus amet, venenatis, sed elit. ante.