Les développeurs de RippleX ont déclaré que le travail de vérification formelle sur le XRP Ledger passe du moteur de paiement de longue date aux nouveaux protocoles DeFi natifs, y compris Single Asset Vault et le prochain protocole de prêt, marquant une transition vers la preuve de l'exactitude du protocole avant l'expédition des fonctionnalités à enjeux élevés.
Dans un article du 8 juin, Vito Tumas, écrivant pour RippleX Developers, a déclaré que cette nouvelle orientation faisait suite à une phase exploratoire plus tôt cette année avec Common Prefix, qui a aidé à définir la portée technique et la stratégie d'application de méthodes formelles à la prochaine génération de primitives financières natives de XRPL.
« Ce pivot représente un changement dans la façon dont nous abordons le développement de fonctionnalités natives de protocole », a écrit Tumas. « Plutôt qu'un filet de sécurité, nous intégrerons des pratiques de vérification formelles dès le premier jour, en spécifiant et en vérifiant de nouvelles fonctionnalités complexes. Nous faisons de l'exactitude prouvable du protocole une propriété de conception. »
Pourquoi cela est important pour le grand livre XRP
La distinction est importante car l'approche de XRPL en matière de DeFi diffère des réseaux où les prêts, les coffres-forts et autres logiques financières résident généralement dans des contrats intelligents distincts. Selon RippleX, le XRP Ledger intègre ses primitives DeFi directement dans son architecture C++ de base. Cette conception peut apporter des avantages en termes de performances et d’intégration, mais elle augmente également le coût d’une défaillance.
Comme le dit le message, un bug dans un contrat intelligent externe peut être isolé ou remplacé. Une vulnérabilité dans le code C++ de base de la couche 1 peut avoir des implications à l’échelle du grand livre. C’est le contexte de sécurité de la campagne de vérification formelle autour du Single Asset Vault et du Lending Protocol, qui introduisent tous deux une logique économique native plus complexe dans XRPL.
RippleX a déclaré que la complexité ne réside pas principalement dans le volume de code. Au lieu de cela, le principal défi réside dans la préservation de la précision numérique sur plusieurs opérations séquentielles, où les petits problèmes d’arrondi ne doivent pas se transformer en erreurs comptables plus importantes. Sur les marchés des prêts et dans les systèmes de coffre-fort, ce type de précision n’est pas un détail secondaire ; cela fait partie de la conception économique.
« La vérification formelle est l'outil naturel pour cette classe de problèmes », a écrit Tumas, la décrivant comme un moyen de prouver mathématiquement l'exactitude de ces mécanismes et d'établir une norme pour les primitives DeFi natives qui suivent.
Le message opposait la vérification formelle aux tests conventionnels. Les tests unitaires, les tests d'intégration et les tests système peuvent valider des scénarios spécifiques anticipés par les ingénieurs, y compris les flux d'utilisateurs attendus et les interactions contradictoires. La limite, selon RippleX, est que les ingénieurs ne peuvent tester que les cas qu’ils pensent écrire.
« Pour un protocole DeFi avec un espace d'état presque infini, ce plafond est bas », a écrit Tumas. « Les tests confirment que le système se comporte correctement dans les scénarios pour lesquels il a été interrogé ; il ne peut pas communiquer avec ceux pour lesquels il ne l'était pas. »
La vérification formelle change la question. Plutôt que de se demander si une entrée donnée produit la bonne sortie, le processus construit un modèle abstrait du comportement prévu du protocole dans un langage précis que les ordinateurs peuvent analyser. La question clé est de savoir si le modèle peut se comporter incorrectement dans n’importe quelle condition exprimable.
RippleX a également expliqué comment ce modèle peut se reconnecter à la mise en œuvre de la production. Un « oracle » dérivé du modèle éprouvé peut servir de source de vérité par rapport à laquelle la mise en œuvre de xrpld est continuellement vérifiée. Les mêmes entrées sont introduites dans l’implémentation Oracle et C++, et tout écart dans la sortie est signalé.
« En collaboration avec Common Prefix, nous appliquons cette méthodologie au Single Asset Vault et au Lending Protocol », a écrit Tumas. « La phase de modélisation a déjà fait apparaître des cas extrêmes que les tests standards ont manqués, non pas comme un signe de faiblesse, mais comme une preuve que la vérification formelle fonctionne exactement comme prévu. Ce sont les premiers résultats, mais ils reflètent une méthodologie appuyée par des décennies de preuves, désormais à la portée de l'ingénierie traditionnelle. »
Au moment de mettre sous presse, le XRP s'échangeait à 1,17 $.
Image en vedette créée avec DALL.E, graphique de TradingView.com
Processus éditorial car Bitcoinist se concentre sur la fourniture d’un contenu minutieusement documenté, précis et impartial. Nous respectons des normes d'approvisionnement strictes et chaque page est soumise à un examen minutieux par notre équipe composée d'experts en technologie de haut niveau et d'éditeurs chevronnés. Ce processus garantit l'intégrité, la pertinence et la valeur de notre contenu pour nos lecteurs.
Voir l’article original en anglais
