Selon Mars Finance, EthSystems, une organisation dédiée aux technologies de confidentialité pour Ethereum, a annoncé avoir achevé la vérification formelle de son pool de confidentialité (shielded pool), couvrant l'ensemble du processus, depuis la spécification écrite jusqu'au bytecode exécuté sur le réseau de test Sepolia. La vérification a utilisé différents outils par couche : Lean pour les modèles, les circuits et les hachages ; Halmos et Kontrol pour les contrats ; Aeneas et Verus pour les portefeuilles ; la vérification et le déploiement ont été validés par une reconstitution mot à mot. Les attaques de double dépense et la conservation de la valeur ont été vérifiées par un système de théorèmes Lean. Six problèmes ont été identifiés lors de la vérification, dont trois provenaient des outils de vérification eux-mêmes. L'équipe a également listé les hypothèses toujours en vigueur : absence de collisions dans les fonctions de hachage, rejet des preuves falsifiées par le vérificateur, et cohérence du comportement du contrat avec le modèle.
EthSystems termine la vérification formelle du Privacy Pool
MarsBitPartager
Résumé
EthSystems, une entreprise de technologie de confidentialité sur Ethereum, a achevé la vérification formelle de son pool de confidentialité, couvrant les spécifications jusqu'au bytecode sur la testnet Sepolia. Le processus a utilisé plusieurs outils à travers les couches : modèles, circuits et hachages avec Lean ; contrats avec Halmos et Kontrol ; wallets avec Aeneas et Verus ; et validateurs via des vérifications byte à byte. Les machines de théorèmes Lean ont vérifié la résistance à la double dépense et la conservation de la valeur. Six problèmes ont été identifiés, dont trois dans les outils. Les hypothèses restantes incluent la résistance aux collisions de hachage et la cohérence des contrats avec les modèles. Cet effort s'aligne sur les débats en cours entre les modèles de sécurité Proof of Work (PoW) et Proof of Stake (PoS).
Source:Afficher l'original
Clause de non-responsabilité : les informations sur cette page peuvent avoir été obtenues auprès de tiers et ne reflètent pas nécessairement les points de vue ou opinions de KuCoin. Ce contenu est fourni à titre informatif uniquement, sans aucune représentation ou garantie d’aucune sorte, et ne doit pas être interprété comme un conseil en investissement. KuCoin ne sera pas responsable des erreurs ou omissions, ni des résultats résultant de l’utilisation de ces informations.
Les investissements dans les actifs numériques peuvent être risqués. Veuillez évaluer soigneusement les risques d’un produit et votre tolérance au risque en fonction de votre propre situation financière. Pour plus d’informations, veuillez consulter nos conditions d’utilisation et divulgation des risques.