Input Output présente Blaster pour la vérification des contrats intelligents Cardano

Cardano Community a publié une présentation de Blaster, un outil de vérification automatisée conçu pour vérifier si les contrats intelligents Cardano respectent des règles spécifiées. Les ingénieurs de Input Output Romain Soulat et Jean-Frédéric Etienne montrent comment l’outil examine ces propriétés et peut produire un contre-exemple lorsqu’il détecte une violation. Ils évoquent également les travaux en cours sur la reconstruction de preuves et les moyens de rendre les résultats plus faciles à inspecter.

Définir ce qu’un contrat Cardano doit faire

Les contrats intelligents fixent des conditions pour les transactions sur la blockchain et déterminent la manière dont les applications gèrent les actifs. Un développeur peut spécifier, par exemple, que seul un utilisateur autorisé peut débloquer des fonds détenus par un contrat. La vérification formelle utilise des méthodes mathématiques pour vérifier si un système satisfait des propriétés énoncées dans une spécification. Tandis qu’un test classique examine des cas choisis, la vérification formelle vise à établir si une propriété donnée tient sur l’ensemble des cas couverts par le modèle.

Soulat, responsable technique de Cardano High Assurance, a expliqué que Blaster a pour but d’automatiser une grande partie du travail de preuve. Les développeurs doivent toujours définir le comportement qu’ils veulent vérifier et fournir la spécification correspondante. Lorsque l’outil trouve une violation, il peut produire un contre-exemple à examiner. Soulat a décrit une transaction ou une séquence de transactions qui pourrait montrer quelqu’un d’autre que l’utilisateur autorisé déverrouillant une sortie.

Comment Blaster vérifie les propriétés des contrats

Blaster utilise Lean 4, un système pour exprimer des énoncés mathématiques et travailler avec des preuves, aux côtés d’un solveur automatisé. Il simplifie d’abord le problème; si la propriété n’est pas résolue durant cette phase, le problème restant peut être envoyé au solveur. Pour rendre les vérifications pertinentes pour Cardano, l’équipe a formalisé des parties de l’environnement dans lequel les contrats s’exécutent, y compris l’exécution des scripts et les règles de transaction.

Etienne, ingénieur principal en méthodes formelles, a présenté trois résultats possibles: une propriété peut être signalée comme valide, falsifiée ou indéterminée. Un contre-exemple associé à un résultat falsifié peut aider les développeurs à identifier un bogue de contrat, une hypothèse manquante ou une erreur dans la spécification. Un résultat indéterminé signifie que le solveur n’a pas établi si la propriété tient. La portée d’une vérification dépend des propriétés que les développeurs choisissent d’exprimer.

[NEWSBREAK]

La reconstruction de preuves est en développement

Les développeurs peuvent compiler des contrats écrits dans des langages tels que Plinth, Aiken ou Plutarch vers Untyped Plutus Core, la représentation utilisée pour exécuter les scripts Cardano. Ils peuvent ensuite importer le code compilé dans Lean 4 et spécifier les propriétés à vérifier. Input Output a précédemment publié deux bibliothèques open source qui fournissent les modèles spécifiques à Cardano pour ce processus. Lors d’une démonstration antérieure, l’équipe a utilisé la chaîne de traitement sur un contrat d’exercice issu d’un défi de sécurité, générant un contexte de transaction qui montrait comment le contrat pouvait être exploité.

Etienne a expliqué que la reconstruction de preuves est encore en développement. L’objectif est de permettre à Lean de vérifier de façon indépendante les éléments étayant un résultat valide; l’outil actuel ne produit pas encore une preuve Lean reconstruite lorsque le solveur renvoie ce résultat. Soulat a également présenté des projets pour des vues de contre-exemples plus claires, permettant aux développeurs d’inspecter les détails de transaction derrière une propriété en échec.