Analyse de la sécurité du langage Move : le révolutionnaire des langages de smart contracts
Introduction
Le langage Move est un langage de contrat intelligent qui peut fonctionner dans un environnement blockchain implémentant MoveVM. Sa conception prend en compte de nombreux problèmes de sécurité liés à la blockchain et aux contrats intelligents, s'inspirant de certaines idéologies de conception de sécurité du langage Rust. En tant que nouveau langage de contrat intelligent caractérisé principalement par la sécurité, quelle est la sécurité de Move ? Peut-il éviter les menaces de sécurité courantes des machines virtuelles de contrat comme EVM, WASM, etc., au niveau du langage ou grâce à des mécanismes connexes ? Existe-t-il des problèmes de sécurité spécifiques au Move lui-même ?
Cet article explorera les problèmes de sécurité du langage Move sous trois aspects : les caractéristiques linguistiques, le mécanisme d'exécution et les outils de validation.
1. Les caractéristiques de sécurité du langage Move
Contrairement à de nombreux langages de programmation existants, le langage Move a été conçu pour prendre en charge à la fois l'interaction sécurisée avec du code non fiable et la vérification statique. Move abandonne la logique non linéaire basée sur la flexibilité, ne prend pas en charge l'appel externe dynamique et les appels récursifs, mais utilise des concepts tels que les génériques, le stockage global et les ressources pour mettre en œuvre des modèles de programmation alternatifs. Par exemple, Move omet les caractéristiques de planification dynamique et d'appels récursifs qui pourraient entraîner des vulnérabilités de réentrance.
Les principales caractéristiques de sécurité de Move incluent :
Module : Chaque module Move est composé d'une série de types de structures et de définitions de processus. Un module peut importer des définitions de types et appeler des processus déclarés dans d'autres modules.
Structure : peut être défini comme un type de ressource, indiquant ce qui peut être stocké dans un stockage clé/valeur global persistant.
Processus : définit l'initialisation, le processus sécurisé et le processus non sécurisé.
Stockage global : permet aux programmes Move de stocker des données persistantes, ces données ne peuvent être lues et écrites de manière programmatique que par le module qui les possède.
Vérification d'invariant : prise en charge des invariants pour une vérification statique, garantissant l'intégrité des ressources dans le système.
vérificateur de bytecode : applique le système de types au niveau du bytecode, empêchant les opérations illégales des modules clients malveillants.
Grâce à deux mécanismes, la vérification des invariants et le vérificateur de bytecode, Move réalise une double garantie de sécurité du code au moment de la compilation.
2. Le mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle, et pendant son exécution, il ne peut pas accéder à la mémoire système. Cela permet à Move de s'exécuter en toute sécurité dans un environnement non fiable, sans risque d'être compromis ou abusé.
Le programme Move s'exécute sur la pile, le stockage global est divisé en mémoire ( tas ) et variables globales ( pile ). La mémoire est un stockage de premier niveau, dont les unités ne peuvent pas stocker des pointeurs vers des unités de mémoire. Les variables globales sont utilisées pour stocker des pointeurs vers des unités de mémoire, mais la méthode d'indexation est différente de celle de la mémoire.
Les instructions de bytecode de Move sont exécutées dans un interpréteur basé sur une pile. La machine virtuelle à pile est facile à mettre en œuvre et à contrôler, nécessite peu d'exigences en matière d'environnement matériel, et convient aux scénarios de blockchain. Par rapport à un interpréteur basé sur des registres, un interpréteur basé sur une pile facilite le contrôle et la détection des opérations de copie et de déplacement entre les variables.
L'état d'exécution du programme Move est un quadruplet ⟨C, M, G, S⟩, comprenant la pile d'appels (C), la mémoire (M), les variables globales (G) et les opérandes (S). La pile maintient également une table de fonctions pour résoudre les instructions contenant le corps des fonctions.
MoveVM sépare la logique des processus de stockage de données et de la pile d'appels (, ce qui est la plus grande différence avec l'EVM. Dans MoveVM, les ressources sous l'adresse du compte d'état utilisateur ) sont stockées de manière indépendante, et les appels de programme doivent respecter des règles contraignantes liées aux permissions et aux ressources. Ce design sacrifie une certaine flexibilité, mais contribue considérablement à améliorer la sécurité et l'efficacité d'exécution (, en facilitant l'exécution concurrente ).
3. Move Prover
Move Prover est un outil de vérification formelle basé sur le raisonnement. Il utilise un langage formel pour décrire le comportement des programmes et des algorithmes de raisonnement pour vérifier si le programme correspond aux attentes, aidant ainsi les développeurs à garantir la correctitude des smart contracts et à réduire les risques de transaction.
Move Prover utilise un algorithme de vérification par déduction pour valider si le programme correspond aux attentes. Cela signifie qu'il peut déduire le comportement du programme en fonction des informations connues, garantissant ainsi une correspondance avec le comportement attendu. Cela aide à garantir la correction du programme et à réduire la charge de travail des tests manuels.
Le flux de travail de Move Prover est le suivant :
Recevoir le fichier source Move comme entrée, ce fichier doit définir les spécifications d'entrée du programme.
Move Parser extrait la spécification du code source.
Le compilateur Move compile le fichier source en bytecode, et le transforme en modèle d'objet de validateur en collaboration avec le système de spécification.
Le modèle est traduit en langage intermédiaire Boogie.
Le code Boogie est transmis au système de vérification Boogie pour générer les conditions de vérification.
Conditions de validation passées au solveur Z3 (, le solveur SMT développé par Microsoft ).
Z3 vérifie si la formule SMT est insatisfaisable. Si c'est le cas, cela signifie que la spécification est valide ; sinon, un modèle satisfaisant les conditions est généré.
Restaurer le rapport de diagnostic au niveau du code source.
Move utilise le Move Specification Language pour décrire les spécifications du système. C'est un sous-ensemble du langage Move, qui prend en charge la description statique du comportement de la correction des programmes, sans affecter la production. Il peut être écrit de manière autonome en tant que fichier de spécification dédié, séparant le code métier et le code de vérification formelle.
Move Prover est un outil utile qui aide les développeurs à garantir la correctitude des smart contracts. Il utilise un langage formel pour décrire le comportement des programmes et utilise des algorithmes de raisonnement pour vérifier si le programme correspond aux attentes, aidant ainsi à réduire les risques de transaction et permettant aux développeurs de déployer les smart contracts en toute confiance dans un environnement de production.
4. Résumé
Le langage Move est très performant en matière de conception de sécurité, offrant une réflexion complète sur les caractéristiques du langage, l'exécution de la machine virtuelle et les outils de sécurité. Les caractéristiques du langage sacrifient une certaine flexibilité, imposant une vérification de type stricte et une logique linéaire, facilitant l'automatisation et la vérifiabilité formelle de la vérification de compilation et de la sécurité. La conception de MoveVM sépare l'état de la logique, répondant mieux aux besoins de gestion de la sécurité des actifs sur la blockchain.
Au niveau linguistique, Move peut efficacement éviter les vulnérabilités courantes de l'EVM telles que la réentrance, le débordement, l'injection Call/DeleGateCall, etc. Cependant, des problèmes tels que l'authentification, la logique du code et le débordement des structures d'entiers de grande taille doivent toujours être pris en compte par les développeurs. Move Prover peut ne pas fonctionner si l'ensemble du sens est négligé.
Bien que le langage Move ait beaucoup pris en compte la sécurité pour les programmeurs, il n'existe pas de langage et de programme totalement sûrs. Il est conseillé aux développeurs de smart contracts Move d'utiliser des services d'audit de sociétés de sécurité tierces et de confier la rédaction et la vérification de la spécification de certaines parties du code à des sociétés de sécurité tierces.
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.
18 J'aime
Récompense
18
4
Partager
Commentaire
0/400
DegenRecoveryGroup
· 08-06 15:36
Il y a quelque chose, le goût de la rouille est trop prononcé.
Voir l'originalRépondre0
AlwaysAnon
· 08-06 01:22
La sécurité est mondiale mais l'écosystème est trop faible
Voir l'originalRépondre0
GasGrillMaster
· 08-06 01:15
move c'est lancé ! Il ne reste plus qu'à attendre l'explosion
Analyse de la sécurité du langage Move : un nouveau paradigme pour les smart contracts
Analyse de la sécurité du langage Move : le révolutionnaire des langages de smart contracts
Introduction
Le langage Move est un langage de contrat intelligent qui peut fonctionner dans un environnement blockchain implémentant MoveVM. Sa conception prend en compte de nombreux problèmes de sécurité liés à la blockchain et aux contrats intelligents, s'inspirant de certaines idéologies de conception de sécurité du langage Rust. En tant que nouveau langage de contrat intelligent caractérisé principalement par la sécurité, quelle est la sécurité de Move ? Peut-il éviter les menaces de sécurité courantes des machines virtuelles de contrat comme EVM, WASM, etc., au niveau du langage ou grâce à des mécanismes connexes ? Existe-t-il des problèmes de sécurité spécifiques au Move lui-même ?
Cet article explorera les problèmes de sécurité du langage Move sous trois aspects : les caractéristiques linguistiques, le mécanisme d'exécution et les outils de validation.
1. Les caractéristiques de sécurité du langage Move
Contrairement à de nombreux langages de programmation existants, le langage Move a été conçu pour prendre en charge à la fois l'interaction sécurisée avec du code non fiable et la vérification statique. Move abandonne la logique non linéaire basée sur la flexibilité, ne prend pas en charge l'appel externe dynamique et les appels récursifs, mais utilise des concepts tels que les génériques, le stockage global et les ressources pour mettre en œuvre des modèles de programmation alternatifs. Par exemple, Move omet les caractéristiques de planification dynamique et d'appels récursifs qui pourraient entraîner des vulnérabilités de réentrance.
Les principales caractéristiques de sécurité de Move incluent :
Module : Chaque module Move est composé d'une série de types de structures et de définitions de processus. Un module peut importer des définitions de types et appeler des processus déclarés dans d'autres modules.
Structure : peut être défini comme un type de ressource, indiquant ce qui peut être stocké dans un stockage clé/valeur global persistant.
Processus : définit l'initialisation, le processus sécurisé et le processus non sécurisé.
Stockage global : permet aux programmes Move de stocker des données persistantes, ces données ne peuvent être lues et écrites de manière programmatique que par le module qui les possède.
Vérification d'invariant : prise en charge des invariants pour une vérification statique, garantissant l'intégrité des ressources dans le système.
vérificateur de bytecode : applique le système de types au niveau du bytecode, empêchant les opérations illégales des modules clients malveillants.
Grâce à deux mécanismes, la vérification des invariants et le vérificateur de bytecode, Move réalise une double garantie de sécurité du code au moment de la compilation.
2. Le mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle, et pendant son exécution, il ne peut pas accéder à la mémoire système. Cela permet à Move de s'exécuter en toute sécurité dans un environnement non fiable, sans risque d'être compromis ou abusé.
Le programme Move s'exécute sur la pile, le stockage global est divisé en mémoire ( tas ) et variables globales ( pile ). La mémoire est un stockage de premier niveau, dont les unités ne peuvent pas stocker des pointeurs vers des unités de mémoire. Les variables globales sont utilisées pour stocker des pointeurs vers des unités de mémoire, mais la méthode d'indexation est différente de celle de la mémoire.
Les instructions de bytecode de Move sont exécutées dans un interpréteur basé sur une pile. La machine virtuelle à pile est facile à mettre en œuvre et à contrôler, nécessite peu d'exigences en matière d'environnement matériel, et convient aux scénarios de blockchain. Par rapport à un interpréteur basé sur des registres, un interpréteur basé sur une pile facilite le contrôle et la détection des opérations de copie et de déplacement entre les variables.
L'état d'exécution du programme Move est un quadruplet ⟨C, M, G, S⟩, comprenant la pile d'appels (C), la mémoire (M), les variables globales (G) et les opérandes (S). La pile maintient également une table de fonctions pour résoudre les instructions contenant le corps des fonctions.
MoveVM sépare la logique des processus de stockage de données et de la pile d'appels (, ce qui est la plus grande différence avec l'EVM. Dans MoveVM, les ressources sous l'adresse du compte d'état utilisateur ) sont stockées de manière indépendante, et les appels de programme doivent respecter des règles contraignantes liées aux permissions et aux ressources. Ce design sacrifie une certaine flexibilité, mais contribue considérablement à améliorer la sécurité et l'efficacité d'exécution (, en facilitant l'exécution concurrente ).
3. Move Prover
Move Prover est un outil de vérification formelle basé sur le raisonnement. Il utilise un langage formel pour décrire le comportement des programmes et des algorithmes de raisonnement pour vérifier si le programme correspond aux attentes, aidant ainsi les développeurs à garantir la correctitude des smart contracts et à réduire les risques de transaction.
Move Prover utilise un algorithme de vérification par déduction pour valider si le programme correspond aux attentes. Cela signifie qu'il peut déduire le comportement du programme en fonction des informations connues, garantissant ainsi une correspondance avec le comportement attendu. Cela aide à garantir la correction du programme et à réduire la charge de travail des tests manuels.
Le flux de travail de Move Prover est le suivant :
Move utilise le Move Specification Language pour décrire les spécifications du système. C'est un sous-ensemble du langage Move, qui prend en charge la description statique du comportement de la correction des programmes, sans affecter la production. Il peut être écrit de manière autonome en tant que fichier de spécification dédié, séparant le code métier et le code de vérification formelle.
Move Prover est un outil utile qui aide les développeurs à garantir la correctitude des smart contracts. Il utilise un langage formel pour décrire le comportement des programmes et utilise des algorithmes de raisonnement pour vérifier si le programme correspond aux attentes, aidant ainsi à réduire les risques de transaction et permettant aux développeurs de déployer les smart contracts en toute confiance dans un environnement de production.
4. Résumé
Le langage Move est très performant en matière de conception de sécurité, offrant une réflexion complète sur les caractéristiques du langage, l'exécution de la machine virtuelle et les outils de sécurité. Les caractéristiques du langage sacrifient une certaine flexibilité, imposant une vérification de type stricte et une logique linéaire, facilitant l'automatisation et la vérifiabilité formelle de la vérification de compilation et de la sécurité. La conception de MoveVM sépare l'état de la logique, répondant mieux aux besoins de gestion de la sécurité des actifs sur la blockchain.
Au niveau linguistique, Move peut efficacement éviter les vulnérabilités courantes de l'EVM telles que la réentrance, le débordement, l'injection Call/DeleGateCall, etc. Cependant, des problèmes tels que l'authentification, la logique du code et le débordement des structures d'entiers de grande taille doivent toujours être pris en compte par les développeurs. Move Prover peut ne pas fonctionner si l'ensemble du sens est négligé.
Bien que le langage Move ait beaucoup pris en compte la sécurité pour les programmeurs, il n'existe pas de langage et de programme totalement sûrs. Il est conseillé aux développeurs de smart contracts Move d'utiliser des services d'audit de sociétés de sécurité tierces et de confier la rédaction et la vérification de la spécification de certaines parties du code à des sociétés de sécurité tierces.