Analyse de la sécurité du langage Move : un changeur de règles pour le langage des smart contracts
Le langage Move est un langage de contrat intelligent pouvant être compilé et exécuté dans un environnement blockchain mettant en œuvre MoveVM. Dès sa création, il a pris en compte de nombreux problèmes de sécurité liés aux blockchains et aux contrats intelligents, s'inspirant de certaines conceptions de sécurité du langage RUST. En tant que nouveau langage de contrat intelligent axé principalement sur la sécurité, quelle est réellement la sécurité de Move ? Peut-il éviter les menaces de sécurité courantes rencontrées dans des machines virtuelles de contrat comme EVM, WASM, etc., au niveau du langage ou des mécanismes connexes ? Existe-t-il des vulnérabilités de sécurité particulières à lui-même ?
Cet article explorera les questions de sécurité du langage Move sous trois aspects : les caractéristiques linguistiques, le mécanisme d'exécution et les outils de vérification.
1. Les caractéristiques de sécurité du langage Move
Contrairement à de nombreux langages de programmation existants, le langage Move a pour objectif de supporter l'écriture de programmes capables d'interagir en toute sécurité avec du code non fiable, tout en prenant en charge la validation statique. Pour atteindre cet objectif, Move a abandonné la logique non linéaire basée sur la flexibilité, ne prenant pas en charge le dispatch dynamique et les appels externes récursifs, mais a plutôt introduit des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation alternatifs. Par exemple, Move a omis les caractéristiques de planification dynamique et d'appels récursifs, des caractéristiques qui pourraient entraîner des vulnérabilités de réentrance coûteuses dans d'autres langages de smart contracts.
Les caractéristiques de sécurité fondamentales de Move incluent :
Module (: Chaque module Move est composé d'une série de types de structure et de définitions de processus. Un module peut importer des définitions de types déclarées dans d'autres modules et appeler des processus.
Structures) : peuvent être définies comme un type de ressource, représentant ce qui peut être stocké dans un stockage clé/valeur global persistant.
3( processus ) Fonction ) : définir la logique de comportement du module.
4( 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 des invariants : il est possible de définir des invariants pour la vérification statique, afin d'assurer la conservation de l'état du système.
vérificateur de bytecode : applique un système de types au niveau du bytecode, empêchant les opérations illégales.
Move garantit la sécurité du code à la compilation grâce à ces caractéristiques. Analysons ensuite le mécanisme d'exécution de Move et voyons comment MoveVM assure la sécurité à l'exécution.
![Analyse de la sécurité de Move : le changeur de jeu des langages de smart contracts])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp)
2. 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, ce qui permet à Move de fonctionner en toute sécurité dans un environnement non fiable. Les programmes Move s'exécutent sur la pile, et le stockage global est divisé en mémoire ( tas ) et variables globales ( pile ). La mémoire est un stockage de premier niveau 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 l'indexation est différente de celle de la mémoire.
Les instructions de bytecode Move s'exécutent dans un interpréteur basé sur une pile. Les machines virtuelles basées sur une pile sont faciles à mettre en œuvre et à contrôler, nécessitent peu d'exigences matérielles et conviennent aux scénarios de blockchain. Par rapport aux interprètes basés sur des registres, les interprètes basés sur une pile sont plus faciles à contrôler et à détecter la copie et le mouvement entre les variables.
Lors de l'exécution d'un programme Move, son état est un quadruplet ⟨C, M, G, S⟩, qui comprend : la pile d'appels (C), la mémoire (M), les variables globales (G) et les opérandes (S). La pile maintient également une table des fonctions ( et le module lui-même ) pour résoudre les instructions contenant le corps de la fonction.
MoveVM sépare la logique de processus de stockage des données et de la pile d'appels (, ce qui constitue la plus grande différence avec l'EVM. Dans MoveVM, les ressources ) sous l'adresse de 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 autorisations et aux ressources. Bien que cela sacrifie une certaine flexibilité, cela contribue à améliorer la sécurité et l'efficacité d'exécution ), permettant ainsi un gain significatif en matière d'exécution concurrente (.
![Analyse de la sécurité de Move : le changeur de jeu des smart contracts])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
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 utilise des algorithmes de raisonnement pour vérifier si le programme répond aux attentes, aidant ainsi les développeurs à garantir la correction des smart contracts, réduisant ainsi les risques de transaction.
Move Prover utilise un algorithme de vérification par déduction pour vérifier si le programme répond aux attentes. Cela signifie que Move Prover peut déduire le comportement du programme en fonction des informations connues et s'assurer qu'il correspond au comportement attendu. Cela aide à garantir la correction du programme et à réduire la charge de travail des tests manuels.
Le workflow de Move Prover est le suivant :
Recevoir le fichier source Move en entrée, ce fichier doit définir la spécification d'entrée du programme )specification(.
Move Parser extrait les spécifications du code source.
Le compilateur Move compile le fichier source en bytecode, et le transforme avec le système standard en modèle d'objet vérificateur )Prover Object Model(.
Traduire le modèle en langage intermédiaire Boogie.
Le système de vérification Boogie effectue la "génération de conditions de vérification" ) verification condition generation (.
Passer les conditions de validation au solveur Z3 ), le solveur SMT développé par Microsoft (.
Z3 vérifie si le code du programme SMT ) satisfait la specification ( ou s'il est insatisfaisable.
Si cela ne peut être satisfait, cela signifie que la spécification est établie ; sinon, générez un modèle satisfaisant les conditions et convertissez-le au format Boogie pour publier le rapport de diagnostic.
Restaurer le rapport de diagnostic en erreurs au niveau du code source.
Move utilise le Move Specification Language pour décrire les spécifications du système. Ce langage est un sous-ensemble de Move, supporte la description statique du comportement correct des programmes, sans affecter la production. Il est possible d'écrire indépendamment des fichiers de spécifications dédiés, 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 correction 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. Cela contribue à réduire les risques de transaction, permettant 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 changeur de jeu du langage des smart contracts])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
4. Résumé
Le langage Move est très performant en matière de conception de sécurité, avec une prise en compte complète des caractéristiques du langage, de l'exécution de la machine virtuelle et des 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 de la vérification par compilation et la vérifiabilité formelle et sécurisée. 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ébordement, l'injection Call/DeleGateCall, qui sont fréquentes dans l'EVM. Cependant, les problèmes d'authentification, de logique de code et de débordement de structures d'entiers de grande taille doivent toujours être pris en compte par les développeurs. Move Prover peut ne pas être efficace en cas de négligence globale.
Bien que le langage Move ait beaucoup considéré la sécurité pour les programmeurs, il n'existe pas de langage totalement sécurisé, ni de programme totalement sécurisé. Il est conseillé aux développeurs de smart contracts Move d'utiliser les services d'audit d'entreprises de sécurité tierces, et de confier la rédaction et la validation de certaines parties du code de la spécification à des entreprises de sécurité tierces.
![Analyse de la sécurité de Move : un changeur de jeu pour le langage des smart contracts])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
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.
16 J'aime
Récompense
16
3
Partager
Commentaire
0/400
AirdropBlackHole
· 07-20 03:29
3 ans Mineur cherche une personne compatible pour l'accompagner !
Voir l'originalRépondre0
PumpBeforeRug
· 07-20 03:29
Regardez ce nouveau favori de move, il peut également prévenir les failles.
Voir l'originalRépondre0
CoinBasedThinking
· 07-20 03:24
La sécurité linguistique, peu importe sa force, n'a pas d'utilité.
Analyse de la sécurité du langage Move : le nouveau gardien de la sécurité des smart contracts
Analyse de la sécurité du langage Move : un changeur de règles pour le langage des smart contracts
Le langage Move est un langage de contrat intelligent pouvant être compilé et exécuté dans un environnement blockchain mettant en œuvre MoveVM. Dès sa création, il a pris en compte de nombreux problèmes de sécurité liés aux blockchains et aux contrats intelligents, s'inspirant de certaines conceptions de sécurité du langage RUST. En tant que nouveau langage de contrat intelligent axé principalement sur la sécurité, quelle est réellement la sécurité de Move ? Peut-il éviter les menaces de sécurité courantes rencontrées dans des machines virtuelles de contrat comme EVM, WASM, etc., au niveau du langage ou des mécanismes connexes ? Existe-t-il des vulnérabilités de sécurité particulières à lui-même ?
Cet article explorera les questions de sécurité du langage Move sous trois aspects : les caractéristiques linguistiques, le mécanisme d'exécution et les outils de vérification.
1. Les caractéristiques de sécurité du langage Move
Contrairement à de nombreux langages de programmation existants, le langage Move a pour objectif de supporter l'écriture de programmes capables d'interagir en toute sécurité avec du code non fiable, tout en prenant en charge la validation statique. Pour atteindre cet objectif, Move a abandonné la logique non linéaire basée sur la flexibilité, ne prenant pas en charge le dispatch dynamique et les appels externes récursifs, mais a plutôt introduit des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation alternatifs. Par exemple, Move a omis les caractéristiques de planification dynamique et d'appels récursifs, des caractéristiques qui pourraient entraîner des vulnérabilités de réentrance coûteuses dans d'autres langages de smart contracts.
Les caractéristiques de sécurité fondamentales de Move incluent :
Module (: Chaque module Move est composé d'une série de types de structure et de définitions de processus. Un module peut importer des définitions de types déclarées dans d'autres modules et appeler des processus.
Structures) : peuvent être définies comme un type de ressource, représentant ce qui peut être stocké dans un stockage clé/valeur global persistant.
3( processus ) Fonction ) : définir la logique de comportement du module.
4( 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 des invariants : il est possible de définir des invariants pour la vérification statique, afin d'assurer la conservation de l'état du système.
vérificateur de bytecode : applique un système de types au niveau du bytecode, empêchant les opérations illégales.
Move garantit la sécurité du code à la compilation grâce à ces caractéristiques. Analysons ensuite le mécanisme d'exécution de Move et voyons comment MoveVM assure la sécurité à l'exécution.
![Analyse de la sécurité de Move : le changeur de jeu des langages de smart contracts])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp)
2. 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, ce qui permet à Move de fonctionner en toute sécurité dans un environnement non fiable. Les programmes Move s'exécutent sur la pile, et le stockage global est divisé en mémoire ( tas ) et variables globales ( pile ). La mémoire est un stockage de premier niveau 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 l'indexation est différente de celle de la mémoire.
Les instructions de bytecode Move s'exécutent dans un interpréteur basé sur une pile. Les machines virtuelles basées sur une pile sont faciles à mettre en œuvre et à contrôler, nécessitent peu d'exigences matérielles et conviennent aux scénarios de blockchain. Par rapport aux interprètes basés sur des registres, les interprètes basés sur une pile sont plus faciles à contrôler et à détecter la copie et le mouvement entre les variables.
Lors de l'exécution d'un programme Move, son état est un quadruplet ⟨C, M, G, S⟩, qui comprend : la pile d'appels (C), la mémoire (M), les variables globales (G) et les opérandes (S). La pile maintient également une table des fonctions ( et le module lui-même ) pour résoudre les instructions contenant le corps de la fonction.
MoveVM sépare la logique de processus de stockage des données et de la pile d'appels (, ce qui constitue la plus grande différence avec l'EVM. Dans MoveVM, les ressources ) sous l'adresse de 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 autorisations et aux ressources. Bien que cela sacrifie une certaine flexibilité, cela contribue à améliorer la sécurité et l'efficacité d'exécution ), permettant ainsi un gain significatif en matière d'exécution concurrente (.
![Analyse de la sécurité de Move : le changeur de jeu des smart contracts])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
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 utilise des algorithmes de raisonnement pour vérifier si le programme répond aux attentes, aidant ainsi les développeurs à garantir la correction des smart contracts, réduisant ainsi les risques de transaction.
Move Prover utilise un algorithme de vérification par déduction pour vérifier si le programme répond aux attentes. Cela signifie que Move Prover peut déduire le comportement du programme en fonction des informations connues et s'assurer qu'il correspond au comportement attendu. Cela aide à garantir la correction du programme et à réduire la charge de travail des tests manuels.
Le workflow de Move Prover est le suivant :
Recevoir le fichier source Move en entrée, ce fichier doit définir la spécification d'entrée du programme )specification(.
Move Parser extrait les spécifications du code source.
Le compilateur Move compile le fichier source en bytecode, et le transforme avec le système standard en modèle d'objet vérificateur )Prover Object Model(.
Traduire le modèle en langage intermédiaire Boogie.
Le système de vérification Boogie effectue la "génération de conditions de vérification" ) verification condition generation (.
Passer les conditions de validation au solveur Z3 ), le solveur SMT développé par Microsoft (.
Z3 vérifie si le code du programme SMT ) satisfait la specification ( ou s'il est insatisfaisable.
Si cela ne peut être satisfait, cela signifie que la spécification est établie ; sinon, générez un modèle satisfaisant les conditions et convertissez-le au format Boogie pour publier le rapport de diagnostic.
Restaurer le rapport de diagnostic en erreurs au niveau du code source.
Move utilise le Move Specification Language pour décrire les spécifications du système. Ce langage est un sous-ensemble de Move, supporte la description statique du comportement correct des programmes, sans affecter la production. Il est possible d'écrire indépendamment des fichiers de spécifications dédiés, 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 correction 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. Cela contribue à réduire les risques de transaction, permettant 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 changeur de jeu du langage des smart contracts])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
4. Résumé
Le langage Move est très performant en matière de conception de sécurité, avec une prise en compte complète des caractéristiques du langage, de l'exécution de la machine virtuelle et des 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 de la vérification par compilation et la vérifiabilité formelle et sécurisée. 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ébordement, l'injection Call/DeleGateCall, qui sont fréquentes dans l'EVM. Cependant, les problèmes d'authentification, de logique de code et de débordement de structures d'entiers de grande taille doivent toujours être pris en compte par les développeurs. Move Prover peut ne pas être efficace en cas de négligence globale.
Bien que le langage Move ait beaucoup considéré la sécurité pour les programmeurs, il n'existe pas de langage totalement sécurisé, ni de programme totalement sécurisé. Il est conseillé aux développeurs de smart contracts Move d'utiliser les services d'audit d'entreprises de sécurité tierces, et de confier la rédaction et la validation de certaines parties du code de la spécification à des entreprises de sécurité tierces.
![Analyse de la sécurité de Move : un changeur de jeu pour le langage des smart contracts])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(