/ Vérification formelle avancée de la pile logicielle complète Web3 /
CertiK a récemment publié un rapport de vérification formelle avancée sur le module Cosmos SDK Bank, qui, à notre connaissance, est la première tentative réussie de vérification formelle du SDK Cosmos. La vérification formelle est une technique qui utilise la logique mathématique pour garantir qu'un système est conforme aux spécifications afin qu'il se comporte comme prévu sous toutes les entrées et conditions possibles. Dans cet article, nous présenterons les étapes spécifiques de la vérification formelle du module Cosmos SDK Bank, ainsi que certains résultats de vérification.
Qu'est-ce que le SDK Cosmos ?
Le Cosmos Software Development Kit (SDK en abrégé) est un framework qui permet aux développeurs de créer des applications blockchain personnalisées. Grâce au SDK Cosmos, les développeurs peuvent facilement lancer leur propre blockchain de couche 1 sans avoir à se soucier de la conception et de la mise en œuvre de la couche consensus à la couche application. Le SDK Cosmos fournit des modules de base standard qui peuvent être directement importés et utilisés par n'importe quelle chaîne, tels que les modules de jalonnement, d'authentification, gov et mint.
source:
###Module Banque
Le module bancaire du SDK Cosmos est responsable de toutes les fonctions liées à la gestion des jetons, telles que le transfert de jetons natifs. L'envoi de jetons doit répondre à de nombreuses restrictions et conditions. Par exemple, le compte doit disposer d'un nombre suffisant de jetons disponibles, à l'exclusion des jetons qui ont été mis en jeu, verrouillés ou en cours de dégroupage. Avec le support de modules tels que le staking et l'authentification, le module bancaire gère l'ensemble du processus d'envoi de tokens. Bien que le module bancaire dépende de plusieurs autres modules, n'entrant pas dans le cadre de cette vérification formelle, nous avons fait quelques hypothèses sur sa fonctionnalité afin de simplifier le processus.
Le module bancaire du SDK se compose de plusieurs sous-modules, dont keeper et types, qui sont des composants essentiels qui définissent le comportement du module et les types de données. Nous nous concentrerons sur le sous-module keeper car il couvre les principales fonctions et caractéristiques du module.
Le sous-module keeper comporte deux composants clés : la visualisation et l'envoi. Le gardien de vue est responsable de la gestion des comptes et des soldes, tandis que le gardien d'envoi est responsable de la modification des soldes des comptes, comme le transfert et le jalonnement des jetons verrouillés ou déverrouillés. Le flux du module bancaire est illustré dans la figure ci-dessous. Les flèches indiquent la direction des composants vers les fonctions ou les gardiens.
source:
Méthode d'authentification
Comme mentionné précédemment, la portée de cette vérification est limitée au module bancaire. Avant de commencer la vérification, nous formulons d'abord des spécifications formelles pour les types de données dans le module bancaire. Par exemple, il existe une structure de données de jeton dans le module bancaire, qui contient la dénomination du type chaîne et la quantité de type big.Int, qui est définie dans le code source comme suit :
Cette structure est très simple, nous utilisons Coq (notre langage de modélisation et de vérification formelle) pour la définir comme suit :
Sur la base de cette définition, nous prouvons d'abord certaines propriétés sur les opérations de base des pièces afin de jeter les bases de l'intégrité fonctionnelle du module bancaire, ce qui nécessite des modifications et des manipulations fréquentes du type de pièce. Par exemple:
Ce lemme prouve une invariance fondamentale : la soustraction de deux pièces ne change pas leur dénomination, ni ne provoque un solde négatif.
Semblable à l'exemple précédent, les composants sous-jacents de chaque transition d'état sont modélisés dans Coq, notamment KV Store, GasMeter, Error Handling et Context.
Pour les spécifications détaillées des types de données et leur validation, voir :
Modélisez le gardien
Après avoir terminé la modélisation des composants de base, nous pouvons modéliser le core keeper du module bancaire pour décrire les fonctions du module. Le teneur de banque dispose de deux interfaces, l'une pour l'accès en lecture seule aux données des jetons et l'autre pour le transfert des jetons et la maintenance de l'approvisionnement.
View keeper est responsable de la gestion de l'accès en lecture seule aux soldes des comptes et contient quatre fonctions pour calculer les soldes des comptes :
GetBalance : recherchez le solde du compte d'une dénomination spécifique via l'adresse. Il considère deux cas : une séquence d'octets nuls et une séquence d'octets non nuls. La vérification formelle garantit que la fonction GetBalance produit des résultats corrects dans les deux cas.
LockedCoins : renvoie tous les jetons non dépensés du compte correspondant à une adresse. En raison de contraintes de temps, nous avons fait des hypothèses sur certaines implémentations du module auth.
GetAllBalances : renvoie tous les soldes des comptes sous l'adresse spécifiée.
GetAccountsBalances : renvoie tous les soldes des comptes du stockage, avec les champs BAddress et BCoins comme enregistrements.
Le gestionnaire d'envoi est responsable de la gestion des transferts et de l'approvisionnement des jetons. Pendant les transferts, il maintient l’approvisionnement en jetons afin qu’aucun nouveau jeton ne soit émis.
SetBalance : définissez le solde du jeton pour le compte via l'adresse. Cette fonction considère deux cas : un solde mis à zéro et un solde mis à non zéro. Dans les deux cas, l’exactitude de SetBalance est prouvée.
subUnlockedCoin : déduisez le montant spécifié (jeton) d'une adresse. La fonction récursive subUnlockedCoins effectue la même opération sur un ensemble de pièces. Les propriétés pertinentes de ces fonctions sont considérées comme des hypothèses axiomatiques.
addCoin : ajoutez le montant spécifié (jetons) à une adresse. La fonction récursive addCoins effectue la même opération sur un ensemble de pièces. Les propriétés pertinentes de ces fonctions sont considérées comme des hypothèses axiomatiques.
SendCoins : envoyez le montant d'une adresse de compte à une autre adresse de compte afin que les fonds des deux adresses soient mis à jour. Si le destinataire n'existe pas, un nouveau compte sera créé pour lui.
En utilisant le modèle ci-dessus des composants de base, nous pouvons commencer la vérification.
Processus de vérification
Notre vérification se fait en décrivant formellement les propriétés invariantes de ces fonctions et en les prouvant dans un système de preuve auxiliaire, en se concentrant principalement sur les fonctionnalités de base de "View Keeper" et "Send Keeper".
Par exemple, la spécification et le lemme setBalance_ok prouvent l'exactitude de la fonction setBalance du module BaseSendKeeper, prouvant spécifiquement les propriétés suivantes :
Lorsque send.setBalance revient à l'état "Ok", il y a un newMultiStore. À ce moment, l'environnement mis à jour uctx est dérivé de l'ancien environnement d'origine ctx en mettant à jour newMultiStore.
Le solde en cours de définition est un jeton valide (il possède les propriétés requises d'un jeton dans le système).
La relation setBalance_prop est maintenue pour garantir que la fonction met à jour le solde dans newMultiStore de la manière attendue et génère l'environnement uctx mis à jour.
Une fois le réglage du solde terminé, utilisez l'adresse du compte et le solde de dénomination. (Denom) pour appeler view.GetBalance sur l'environnement mis à jour uctx, et il renverra le même solde défini par send.setBalance.
Ces propriétés sont décrites dans le langage de spécification Coq comme suit :
Pour le code Coq d'une autre nature, visitez :
future carrière
La base de cette vérification repose sur plusieurs hypothèses et axiomes, que nous pouvons vérifier plus en profondeur pour élargir la portée de la vérification. Les priorités des travaux futurs comprennent les domaines suivants :
Vérification des hypothèses : La vérification actuelle repose sur une série d'hypothèses comme base de preuve. Ces hypothèses pourront être testées à l’avenir pour garantir qu’elles reflètent fidèlement le comportement et les propriétés attendus du système.
Vérification du module d'authentification : ce module est responsable de la gestion des données de compte et du mécanisme de signature et constitue le composant principal du SDK Cosmos. À l'avenir, il pourra être entièrement vérifié formellement pour garantir que la mise en œuvre du module et l'interaction avec d'autres modules sont exactes.
Plus de théorèmes sur la confiance, la frappe et la vente des pièces : élargir la portée de la vérification et introduire davantage de théorèmes sur la confiance, la frappe et la vente des pièces aideront à comprendre le mécanisme de fonctionnement du système de manière plus complète. Ces théorèmes peuvent être combinés avec la vérification du module d'authentification pour garantir la cohérence et l'exactitude globales du système.
Développez l'ensemble de l'infrastructure Cosmos SDK : le travail de vérification actuel se concentre principalement sur le module bancaire et ses composants associés. À l'avenir, le processus de vérification formelle pourra être étendu à l'ensemble de l'infrastructure du SDK Cosmos, améliorant ainsi la précision, la sécurité et la stabilité globales de la plate-forme et offrant aux développeurs et aux utilisateurs un environnement plus stable et plus fiable.
Intégrer avec d'autres modules : étant donné que le SDK Cosmos comprend une variété de modules interconnectés, il est très avantageux d'explorer les interactions et les dépendances entre eux. Cela nécessite de vérifier l'exactitude des interactions entre les modules et de s'assurer que toute modification apportée à un module n'affecte pas négativement les autres modules.
Modélisation et vérification des mécanismes d'incitation : Cosmos SDK intègre également des mécanismes d'incitation tels que le jalonnement et la distribution de récompenses. Les recherches futures modéliseront et valideront ces mécanismes pour garantir qu’ils sont corrects et cohérents avec les incitations économiques attendues.
Cet article présente le premier cas réussi de vérification formelle avancée du module Cosmos SDKbank, effectuant un travail efficace pour construire les bases de sécurité et de fiabilité de l'écosystème blockchain. Les travaux futurs développeront cette réalisation en validant les hypothèses, en validant d'autres modules et en couvrant l'ensemble de l'infrastructure du SDK Cosmos, créant ainsi une plate-forme plus solide et plus fiable pour les développeurs et les utilisateurs.
Voir l'original
Cette page peut inclure du contenu de tiers fourni à des fins d'information uniquement. Gate ne garantit ni l'exactitude ni la validité de ces contenus, n’endosse pas les opinions exprimées, et ne fournit aucun conseil financier ou professionnel à travers ces informations. Voir la section Avertissement pour plus de détails.
Expliquer en détail la vérification formelle des modules standards du SDK Cosmos
/ Vérification formelle avancée de la pile logicielle complète Web3 /
CertiK a récemment publié un rapport de vérification formelle avancée sur le module Cosmos SDK Bank, qui, à notre connaissance, est la première tentative réussie de vérification formelle du SDK Cosmos. La vérification formelle est une technique qui utilise la logique mathématique pour garantir qu'un système est conforme aux spécifications afin qu'il se comporte comme prévu sous toutes les entrées et conditions possibles. Dans cet article, nous présenterons les étapes spécifiques de la vérification formelle du module Cosmos SDK Bank, ainsi que certains résultats de vérification.
Qu'est-ce que le SDK Cosmos ?
Le Cosmos Software Development Kit (SDK en abrégé) est un framework qui permet aux développeurs de créer des applications blockchain personnalisées. Grâce au SDK Cosmos, les développeurs peuvent facilement lancer leur propre blockchain de couche 1 sans avoir à se soucier de la conception et de la mise en œuvre de la couche consensus à la couche application. Le SDK Cosmos fournit des modules de base standard qui peuvent être directement importés et utilisés par n'importe quelle chaîne, tels que les modules de jalonnement, d'authentification, gov et mint.
source:
###Module Banque
Le module bancaire du SDK Cosmos est responsable de toutes les fonctions liées à la gestion des jetons, telles que le transfert de jetons natifs. L'envoi de jetons doit répondre à de nombreuses restrictions et conditions. Par exemple, le compte doit disposer d'un nombre suffisant de jetons disponibles, à l'exclusion des jetons qui ont été mis en jeu, verrouillés ou en cours de dégroupage. Avec le support de modules tels que le staking et l'authentification, le module bancaire gère l'ensemble du processus d'envoi de tokens. Bien que le module bancaire dépende de plusieurs autres modules, n'entrant pas dans le cadre de cette vérification formelle, nous avons fait quelques hypothèses sur sa fonctionnalité afin de simplifier le processus.
Le module bancaire du SDK se compose de plusieurs sous-modules, dont keeper et types, qui sont des composants essentiels qui définissent le comportement du module et les types de données. Nous nous concentrerons sur le sous-module keeper car il couvre les principales fonctions et caractéristiques du module.
Le sous-module keeper comporte deux composants clés : la visualisation et l'envoi. Le gardien de vue est responsable de la gestion des comptes et des soldes, tandis que le gardien d'envoi est responsable de la modification des soldes des comptes, comme le transfert et le jalonnement des jetons verrouillés ou déverrouillés. Le flux du module bancaire est illustré dans la figure ci-dessous. Les flèches indiquent la direction des composants vers les fonctions ou les gardiens.
source:
Méthode d'authentification
Comme mentionné précédemment, la portée de cette vérification est limitée au module bancaire. Avant de commencer la vérification, nous formulons d'abord des spécifications formelles pour les types de données dans le module bancaire. Par exemple, il existe une structure de données de jeton dans le module bancaire, qui contient la dénomination du type chaîne et la quantité de type big.Int, qui est définie dans le code source comme suit :
Cette structure est très simple, nous utilisons Coq (notre langage de modélisation et de vérification formelle) pour la définir comme suit :
Sur la base de cette définition, nous prouvons d'abord certaines propriétés sur les opérations de base des pièces afin de jeter les bases de l'intégrité fonctionnelle du module bancaire, ce qui nécessite des modifications et des manipulations fréquentes du type de pièce. Par exemple:
Ce lemme prouve une invariance fondamentale : la soustraction de deux pièces ne change pas leur dénomination, ni ne provoque un solde négatif.
Semblable à l'exemple précédent, les composants sous-jacents de chaque transition d'état sont modélisés dans Coq, notamment KV Store, GasMeter, Error Handling et Context.
Pour les spécifications détaillées des types de données et leur validation, voir :
Modélisez le gardien
Après avoir terminé la modélisation des composants de base, nous pouvons modéliser le core keeper du module bancaire pour décrire les fonctions du module. Le teneur de banque dispose de deux interfaces, l'une pour l'accès en lecture seule aux données des jetons et l'autre pour le transfert des jetons et la maintenance de l'approvisionnement.
View keeper est responsable de la gestion de l'accès en lecture seule aux soldes des comptes et contient quatre fonctions pour calculer les soldes des comptes :
GetBalance : recherchez le solde du compte d'une dénomination spécifique via l'adresse. Il considère deux cas : une séquence d'octets nuls et une séquence d'octets non nuls. La vérification formelle garantit que la fonction GetBalance produit des résultats corrects dans les deux cas.
LockedCoins : renvoie tous les jetons non dépensés du compte correspondant à une adresse. En raison de contraintes de temps, nous avons fait des hypothèses sur certaines implémentations du module auth.
GetAllBalances : renvoie tous les soldes des comptes sous l'adresse spécifiée.
GetAccountsBalances : renvoie tous les soldes des comptes du stockage, avec les champs BAddress et BCoins comme enregistrements.
Le gestionnaire d'envoi est responsable de la gestion des transferts et de l'approvisionnement des jetons. Pendant les transferts, il maintient l’approvisionnement en jetons afin qu’aucun nouveau jeton ne soit émis.
SetBalance : définissez le solde du jeton pour le compte via l'adresse. Cette fonction considère deux cas : un solde mis à zéro et un solde mis à non zéro. Dans les deux cas, l’exactitude de SetBalance est prouvée.
subUnlockedCoin : déduisez le montant spécifié (jeton) d'une adresse. La fonction récursive subUnlockedCoins effectue la même opération sur un ensemble de pièces. Les propriétés pertinentes de ces fonctions sont considérées comme des hypothèses axiomatiques.
addCoin : ajoutez le montant spécifié (jetons) à une adresse. La fonction récursive addCoins effectue la même opération sur un ensemble de pièces. Les propriétés pertinentes de ces fonctions sont considérées comme des hypothèses axiomatiques.
SendCoins : envoyez le montant d'une adresse de compte à une autre adresse de compte afin que les fonds des deux adresses soient mis à jour. Si le destinataire n'existe pas, un nouveau compte sera créé pour lui.
En utilisant le modèle ci-dessus des composants de base, nous pouvons commencer la vérification.
Processus de vérification
Notre vérification se fait en décrivant formellement les propriétés invariantes de ces fonctions et en les prouvant dans un système de preuve auxiliaire, en se concentrant principalement sur les fonctionnalités de base de "View Keeper" et "Send Keeper".
Par exemple, la spécification et le lemme setBalance_ok prouvent l'exactitude de la fonction setBalance du module BaseSendKeeper, prouvant spécifiquement les propriétés suivantes :
Lorsque send.setBalance revient à l'état "Ok", il y a un newMultiStore. À ce moment, l'environnement mis à jour uctx est dérivé de l'ancien environnement d'origine ctx en mettant à jour newMultiStore.
Le solde en cours de définition est un jeton valide (il possède les propriétés requises d'un jeton dans le système).
La relation setBalance_prop est maintenue pour garantir que la fonction met à jour le solde dans newMultiStore de la manière attendue et génère l'environnement uctx mis à jour.
Une fois le réglage du solde terminé, utilisez l'adresse du compte et le solde de dénomination. (Denom) pour appeler view.GetBalance sur l'environnement mis à jour uctx, et il renverra le même solde défini par send.setBalance.
Ces propriétés sont décrites dans le langage de spécification Coq comme suit :
Pour le code Coq d'une autre nature, visitez :
future carrière
La base de cette vérification repose sur plusieurs hypothèses et axiomes, que nous pouvons vérifier plus en profondeur pour élargir la portée de la vérification. Les priorités des travaux futurs comprennent les domaines suivants :
Vérification des hypothèses : La vérification actuelle repose sur une série d'hypothèses comme base de preuve. Ces hypothèses pourront être testées à l’avenir pour garantir qu’elles reflètent fidèlement le comportement et les propriétés attendus du système.
Vérification du module d'authentification : ce module est responsable de la gestion des données de compte et du mécanisme de signature et constitue le composant principal du SDK Cosmos. À l'avenir, il pourra être entièrement vérifié formellement pour garantir que la mise en œuvre du module et l'interaction avec d'autres modules sont exactes.
Plus de théorèmes sur la confiance, la frappe et la vente des pièces : élargir la portée de la vérification et introduire davantage de théorèmes sur la confiance, la frappe et la vente des pièces aideront à comprendre le mécanisme de fonctionnement du système de manière plus complète. Ces théorèmes peuvent être combinés avec la vérification du module d'authentification pour garantir la cohérence et l'exactitude globales du système.
Développez l'ensemble de l'infrastructure Cosmos SDK : le travail de vérification actuel se concentre principalement sur le module bancaire et ses composants associés. À l'avenir, le processus de vérification formelle pourra être étendu à l'ensemble de l'infrastructure du SDK Cosmos, améliorant ainsi la précision, la sécurité et la stabilité globales de la plate-forme et offrant aux développeurs et aux utilisateurs un environnement plus stable et plus fiable.
Intégrer avec d'autres modules : étant donné que le SDK Cosmos comprend une variété de modules interconnectés, il est très avantageux d'explorer les interactions et les dépendances entre eux. Cela nécessite de vérifier l'exactitude des interactions entre les modules et de s'assurer que toute modification apportée à un module n'affecte pas négativement les autres modules.
Modélisation et vérification des mécanismes d'incitation : Cosmos SDK intègre également des mécanismes d'incitation tels que le jalonnement et la distribution de récompenses. Les recherches futures modéliseront et valideront ces mécanismes pour garantir qu’ils sont corrects et cohérents avec les incitations économiques attendues.
Cet article présente le premier cas réussi de vérification formelle avancée du module Cosmos SDKbank, effectuant un travail efficace pour construire les bases de sécurité et de fiabilité de l'écosystème blockchain. Les travaux futurs développeront cette réalisation en validant les hypothèses, en validant d'autres modules et en couvrant l'ensemble de l'infrastructure du SDK Cosmos, créant ainsi une plate-forme plus solide et plus fiable pour les développeurs et les utilisateurs.