Analyse de la sécurité du langage Move : le réformateur des langages de smart contracts
Le langage Move est un langage de contrats intelligents qui peut s'exécuter dans un environnement blockchain implémentant MoveVM. Dès sa conception, il a pris en compte de nombreux problèmes de sécurité liés aux blockchains et aux contrats intelligents, en s'inspirant de la conception sécuritaire du langage RUST. En tant que langage de contrats intelligents de nouvelle génération axé sur la sécurité, quelle est son niveau de sécurité ? Peut-il éviter, au niveau du langage ou par des mécanismes associés, les menaces de sécurité courantes des machines virtuelles de contrats comme EVM ou WASM ? Existe-t-il des problèmes de sécurité spécifiques à 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'écriture de programmes interagissant en toute sécurité avec du code non fiable et la validation statique. Move possède ces caractéristiques de sécurité car il abandonne la logique non linéaire basée sur la flexibilité, ne prend pas en charge le dispatch dynamique et n'autorise pas les appels externes récursifs, mais utilise des concepts tels que les génériques, le stockage global et les ressources pour réaliser certains modèles de programmation alternatifs. Par exemple, Move omet les caractéristiques de planification dynamique et d'appels récursifs, qui entraînent des vulnérabilités de réentrance coûteuses dans d'autres langages de contrats intelligents.
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.
Structures) : peuvent être définis comme types de ressources, indiquant qu'ils peuvent être stockés dans un stockage clé/valeur global persistant.
3( processus ) Fonction ) : définit la logique commerciale du contrat.
4( Stockage global : permet aux programmes Move de stocker des données persistantes, ces données ne peuvent être lues/écrites par programmation que par le module qui les possède.
Vérification des invariants : il est possible de définir des invariants de vérification statiques, représentant la conservation des ressources dans le système.
vérificateur de bytecode : vérifie la sécurité des types et la linéarisation du bytecode, impose les règles de création, de destruction et d'accès aux ressources.
Grâce à ces caractéristiques, Move peut garantir une sécurité élevée lors de la compilation. Passons maintenant à l'analyse du mécanisme d'exécution de Move et voyons comment MoveVM garantit la sécurité à l'exécution.
![Analyse de la sécurité de Move : le changeur de jeu du langage des smart contracts])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp)
2. Mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle et ne peut pas accéder à la mémoire système lors de son exécution. Cela permet à Move de fonctionner en toute sécurité dans un environnement non fiable, sans ê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 ) deux parties. La mémoire est un stockage de premier ordre et ne peut pas stocker de 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 basée sur une pile est facile à mettre en œuvre et à contrôler, nécessite peu d'exigences matérielles et convient aux scénarios de blockchain. En même temps, par rapport à un interpréteur basé sur des registres, l'interpréteur basé sur une pile facilite le contrôle et la détection des copies et des mouvements entre les variables.
L'état d'exécution du programme Move est un quadruplet ⟨C, M, G, S⟩, composé de la pile d'appels (C), de la mémoire (M), des variables globales (G) et des opérandes (S). La pile maintient également une table de fonctions pour résoudre les instructions contenant des corps de fonction.
La pile d'appels contient toutes les informations contextuelles et les numéros d'instruction de l'exécution du processus. Un nouvel objet de pile d'appels est créé lors de l'exécution de l'instruction Call, stockant les paramètres d'appel, puis les instructions du nouveau contrat sont exécutées. Lorsqu'une instruction de branchement est rencontrée, un saut statique est effectué à l'intérieur du processus. Ce design évite la distribution dynamique, renforce l'immuabilité des appels de fonction, évitant ainsi la possibilité de réentrance.
MoveVM sépare le stockage des données et la logique de processus 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 obligatoires liées aux permissions et aux ressources. Bien que cette conception sacrifie une certaine flexibilité, elle a considérablement amélioré la sécurité et l'efficacité d'exécution.
![Analyse de la sécurité de Move : le changeur de jeu des langages de contrats intelligents])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. Déplacer 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 emploie des algorithmes de raisonnement pour vérifier si le programme répond aux attentes, aidant ainsi les développeurs à garantir la correctitude des smart contracts, réduisant ainsi le risque de transaction.
Move Prover utilise des algorithmes de vérification par déduction pour valider si un programme répond aux attentes. Il peut déduire le comportement d'un programme en se basant sur des informations connues et s'assurer qu'il correspond au comportement attendu. Cela aide à garantir la correctitude du programme et réduit 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 les fichiers source en bytecode, et les transforme en un modèle d'objet de validateur avec le système de spécification.
Le modèle est traduit en langage intermédiaire Boogie.
Le système de validation Boogie génère des "conditions de validation" pour les entrées.
Les conditions de vérification sont transmises au solveur Z3 pour vérification.
Si la norme est établie, la validation est réussie ; sinon, un rapport de diagnostic est généré.
Pour décrire le système de spécifications, Move utilise le Move Specification Language, qui est un sous-ensemble du langage Move, introduisant un support pour la description statique du comportement de la programme correct. Le Move Specification Language peut être utilisé indépendamment comme un fichier de spécification dédié, permettant ainsi de séparer le code métier et le code de validation formelle.
Move Prover est un outil très utile qui aide les développeurs à garantir la validité 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 répond aux attentes. Cela aide à réduire les risques de transaction et permet aux développeurs de déployer les smart contracts en toute confiance dans un environnement de production.
![Analyse de la Sécurité de Move : Le Game Changer des smart contracts])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Résumé
Le langage Move excelle dans la conception de la sécurité, offrant une considération complète en termes de caractéristiques du langage, d'exécution de la machine virtuelle et d'outils de sécurité. Il sacrifie une partie de la flexibilité au niveau des caractéristiques du langage, avec des vérifications de type strictes et une logique linéaire, facilitant ainsi l'automatisation et la vérifiabilité de la sécurité lors des vérifications de compilation et de validation formelle. 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 du langage, Move peut efficacement éviter les vulnérabilités courantes telles que la réentrance, le dépassement, l'injection Call/DeleGateCall dans l'EVM. Cependant, des problèmes tels que l'authentification, la logique du code et le dépassement de la structure des grands entiers nécessitent encore une attention particulière de la part des développeurs. Bien que Move Prover soit puissant, il peut ne pas fonctionner en cas de négligence générale.
Bien que le langage Move prenne en compte de nombreux aspects de la sécurité pour les programmeurs, il n'existe pas de langage et de programme totalement sûrs. Il est recommandé 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 certaines parties du code de specification à des sociétés de sécurité tierces, afin d'améliorer davantage la sécurité des contrats.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
Analyse approfondie de la sécurité du langage Move : un nouveau standard pour le développement de smart contracts
Analyse de la sécurité du langage Move : le réformateur des langages de smart contracts
Le langage Move est un langage de contrats intelligents qui peut s'exécuter dans un environnement blockchain implémentant MoveVM. Dès sa conception, il a pris en compte de nombreux problèmes de sécurité liés aux blockchains et aux contrats intelligents, en s'inspirant de la conception sécuritaire du langage RUST. En tant que langage de contrats intelligents de nouvelle génération axé sur la sécurité, quelle est son niveau de sécurité ? Peut-il éviter, au niveau du langage ou par des mécanismes associés, les menaces de sécurité courantes des machines virtuelles de contrats comme EVM ou WASM ? Existe-t-il des problèmes de sécurité spécifiques à 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'écriture de programmes interagissant en toute sécurité avec du code non fiable et la validation statique. Move possède ces caractéristiques de sécurité car il abandonne la logique non linéaire basée sur la flexibilité, ne prend pas en charge le dispatch dynamique et n'autorise pas les appels externes récursifs, mais utilise des concepts tels que les génériques, le stockage global et les ressources pour réaliser certains modèles de programmation alternatifs. Par exemple, Move omet les caractéristiques de planification dynamique et d'appels récursifs, qui entraînent des vulnérabilités de réentrance coûteuses dans d'autres langages de contrats intelligents.
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.
Structures) : peuvent être définis comme types de ressources, indiquant qu'ils peuvent être stockés dans un stockage clé/valeur global persistant.
3( processus ) Fonction ) : définit la logique commerciale du contrat.
4( Stockage global : permet aux programmes Move de stocker des données persistantes, ces données ne peuvent être lues/écrites par programmation que par le module qui les possède.
Vérification des invariants : il est possible de définir des invariants de vérification statiques, représentant la conservation des ressources dans le système.
vérificateur de bytecode : vérifie la sécurité des types et la linéarisation du bytecode, impose les règles de création, de destruction et d'accès aux ressources.
Grâce à ces caractéristiques, Move peut garantir une sécurité élevée lors de la compilation. Passons maintenant à l'analyse du mécanisme d'exécution de Move et voyons comment MoveVM garantit la sécurité à l'exécution.
![Analyse de la sécurité de Move : le changeur de jeu du langage des smart contracts])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp)
2. Mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle et ne peut pas accéder à la mémoire système lors de son exécution. Cela permet à Move de fonctionner en toute sécurité dans un environnement non fiable, sans ê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 ) deux parties. La mémoire est un stockage de premier ordre et ne peut pas stocker de 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 basée sur une pile est facile à mettre en œuvre et à contrôler, nécessite peu d'exigences matérielles et convient aux scénarios de blockchain. En même temps, par rapport à un interpréteur basé sur des registres, l'interpréteur basé sur une pile facilite le contrôle et la détection des copies et des mouvements entre les variables.
L'état d'exécution du programme Move est un quadruplet ⟨C, M, G, S⟩, composé de la pile d'appels (C), de la mémoire (M), des variables globales (G) et des opérandes (S). La pile maintient également une table de fonctions pour résoudre les instructions contenant des corps de fonction.
La pile d'appels contient toutes les informations contextuelles et les numéros d'instruction de l'exécution du processus. Un nouvel objet de pile d'appels est créé lors de l'exécution de l'instruction Call, stockant les paramètres d'appel, puis les instructions du nouveau contrat sont exécutées. Lorsqu'une instruction de branchement est rencontrée, un saut statique est effectué à l'intérieur du processus. Ce design évite la distribution dynamique, renforce l'immuabilité des appels de fonction, évitant ainsi la possibilité de réentrance.
MoveVM sépare le stockage des données et la logique de processus 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 obligatoires liées aux permissions et aux ressources. Bien que cette conception sacrifie une certaine flexibilité, elle a considérablement amélioré la sécurité et l'efficacité d'exécution.
![Analyse de la sécurité de Move : le changeur de jeu des langages de contrats intelligents])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. Déplacer 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 emploie des algorithmes de raisonnement pour vérifier si le programme répond aux attentes, aidant ainsi les développeurs à garantir la correctitude des smart contracts, réduisant ainsi le risque de transaction.
Move Prover utilise des algorithmes de vérification par déduction pour valider si un programme répond aux attentes. Il peut déduire le comportement d'un programme en se basant sur des informations connues et s'assurer qu'il correspond au comportement attendu. Cela aide à garantir la correctitude du programme et réduit la charge de travail des tests manuels.
Le flux de travail de Move Prover est le suivant :
Pour décrire le système de spécifications, Move utilise le Move Specification Language, qui est un sous-ensemble du langage Move, introduisant un support pour la description statique du comportement de la programme correct. Le Move Specification Language peut être utilisé indépendamment comme un fichier de spécification dédié, permettant ainsi de séparer le code métier et le code de validation formelle.
Move Prover est un outil très utile qui aide les développeurs à garantir la validité 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 répond aux attentes. Cela aide à réduire les risques de transaction et permet aux développeurs de déployer les smart contracts en toute confiance dans un environnement de production.
![Analyse de la Sécurité de Move : Le Game Changer des smart contracts])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Résumé
Le langage Move excelle dans la conception de la sécurité, offrant une considération complète en termes de caractéristiques du langage, d'exécution de la machine virtuelle et d'outils de sécurité. Il sacrifie une partie de la flexibilité au niveau des caractéristiques du langage, avec des vérifications de type strictes et une logique linéaire, facilitant ainsi l'automatisation et la vérifiabilité de la sécurité lors des vérifications de compilation et de validation formelle. 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 du langage, Move peut efficacement éviter les vulnérabilités courantes telles que la réentrance, le dépassement, l'injection Call/DeleGateCall dans l'EVM. Cependant, des problèmes tels que l'authentification, la logique du code et le dépassement de la structure des grands entiers nécessitent encore une attention particulière de la part des développeurs. Bien que Move Prover soit puissant, il peut ne pas fonctionner en cas de négligence générale.
Bien que le langage Move prenne en compte de nombreux aspects de la sécurité pour les programmeurs, il n'existe pas de langage et de programme totalement sûrs. Il est recommandé 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 certaines parties du code de specification à des sociétés de sécurité tierces, afin d'améliorer davantage la sécurité des contrats.