Le langage Move, en tant que nouveau langage de contrat intelligent de génération, a pris en compte la sécurité de la blockchain et des contrats intelligents dès sa conception. Cet article explorera la sécurité du langage Move sous trois angles : les caractéristiques du langage, le mécanisme d'exécution et les outils de vérification.
1. Les caractéristiques de sécurité du langage Move
Le langage Move abandonne la logique non linéaire basée sur la flexibilité, ne supporte pas l'envoi dynamique et les appels externes récursifs, et utilise des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation alternatifs. Ces conceptions aident à éviter les vulnérabilités de sécurité telles que la réentrance.
Les principales composantes du langage Move comprennent :
Module : composé de définitions de types de structure et de processus, il peut importer des définitions de types d'autres modules et appeler des processus d'autres modules.
Structure : peut être défini comme un type de ressource, stocké dans le stockage clé-valeur global.
Processus : définir les fonctionnalités du module, pouvant inclure des processus d'initialisation, de sécurité et d'insécurité.
Le mécanisme de stockage global du langage Move permet aux modules de stocker des données persistantes et d'avoir un accès en lecture et en écriture exclusif aux types de ressources qu'ils déclarent. Ce mécanisme aide à faire respecter les contraintes de sécurité.
Les deux caractéristiques importantes de vérification statique du langage Move :
Vérification des invariants : définition de la conservation de l'état du système par un langage de spécification.
Validateur de bytecode : impose des types de sécurité et une linéarisation, empêchant les opérations illégales.
2. Mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle et ne peut pas accéder directement à la mémoire système. L'exécution du programme est basée sur la pile, le stockage global est divisé en mémoire (, tas ) et variables globales (, pile ).
L'état d'exécution de Move VM est composé de la pile d'appels, de la mémoire, des variables globales et des opérations. Ses caractéristiques comprennent :
Saut statique, éviter la dispatch dynamique
Appel de pile adjacent, prévenir la réentrante
Séparation de la pile de stockage et d'appel des données
Ce design améliore la sécurité et l'efficacité d'exécution.
3. Move Prover
Move Prover est un outil de vérification formelle qui utilise des algorithmes de vérification déductive pour valider si un programme répond aux attentes. Son flux de travail :
Recevoir le fichier source Move et les spécifications
Compiler en bytecode et modèle d'objet de validateur
Convertir en langage intermédiaire Boogie
Générer des conditions de validation
Vérification avec le solveur Z3
Générer un rapport de diagnostic
Le langage de spécification Move est utilisé pour décrire les spécifications de comportement des programmes, et peut être écrit indépendamment du code métier.
Résumé
Le langage Move prend en compte de manière exhaustive les caractéristiques du langage, l'exécution de la machine virtuelle et les outils de sécurité, ce qui permet d'éviter efficacement de nombreuses vulnérabilités courantes. Cependant, il est toujours recommandé d'utiliser des services d'audit de sécurité tiers et de faire rédiger et valider le code conforme par des entreprises de sécurité.
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.
17 J'aime
Récompense
17
8
Partager
Commentaire
0/400
HashBard
· Il y a 6h
il y a encore des exploits cependant... du théâtre de la sécurité à son meilleur pour être honnête
Voir l'originalRépondre0
AirdropHarvester
· Il y a 18h
Bull, la sécurité avant tout !
Voir l'originalRépondre0
CryptoNomics
· Il y a 18h
*soupir* encore une autre L1 tentant la vérification formelle... statistiquement insignifiant sans une analyse appropriée de l'équilibre de Nash à mon avis
Voir l'originalRépondre0
ForumMiningMaster
· Il y a 18h
J'aime ce genre de valeur sûre.
Voir l'originalRépondre0
DegenGambler
· Il y a 18h
C'est tout pour le contrôle statique ?
Voir l'originalRépondre0
ponzi_poet
· Il y a 18h
Il faut encore voir la performance spécifique, le statique reste statique.
Voir l'originalRépondre0
fork_in_the_road
· Il y a 18h
Vous écrivez encore en solidity ? Entrez dans une position Move
Analyse complète de la sécurité du langage Move : des caractéristiques aux outils de vérification
Analyse de la sécurité du langage Move
Le langage Move, en tant que nouveau langage de contrat intelligent de génération, a pris en compte la sécurité de la blockchain et des contrats intelligents dès sa conception. Cet article explorera la sécurité du langage Move sous trois angles : les caractéristiques du langage, le mécanisme d'exécution et les outils de vérification.
1. Les caractéristiques de sécurité du langage Move
Le langage Move abandonne la logique non linéaire basée sur la flexibilité, ne supporte pas l'envoi dynamique et les appels externes récursifs, et utilise des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation alternatifs. Ces conceptions aident à éviter les vulnérabilités de sécurité telles que la réentrance.
Les principales composantes du langage Move comprennent :
Module : composé de définitions de types de structure et de processus, il peut importer des définitions de types d'autres modules et appeler des processus d'autres modules.
Structure : peut être défini comme un type de ressource, stocké dans le stockage clé-valeur global.
Processus : définir les fonctionnalités du module, pouvant inclure des processus d'initialisation, de sécurité et d'insécurité.
Le mécanisme de stockage global du langage Move permet aux modules de stocker des données persistantes et d'avoir un accès en lecture et en écriture exclusif aux types de ressources qu'ils déclarent. Ce mécanisme aide à faire respecter les contraintes de sécurité.
Les deux caractéristiques importantes de vérification statique du langage Move :
Vérification des invariants : définition de la conservation de l'état du système par un langage de spécification.
Validateur de bytecode : impose des types de sécurité et une linéarisation, empêchant les opérations illégales.
2. Mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle et ne peut pas accéder directement à la mémoire système. L'exécution du programme est basée sur la pile, le stockage global est divisé en mémoire (, tas ) et variables globales (, pile ).
L'état d'exécution de Move VM est composé de la pile d'appels, de la mémoire, des variables globales et des opérations. Ses caractéristiques comprennent :
Ce design améliore la sécurité et l'efficacité d'exécution.
3. Move Prover
Move Prover est un outil de vérification formelle qui utilise des algorithmes de vérification déductive pour valider si un programme répond aux attentes. Son flux de travail :
Le langage de spécification Move est utilisé pour décrire les spécifications de comportement des programmes, et peut être écrit indépendamment du code métier.
Résumé
Le langage Move prend en compte de manière exhaustive les caractéristiques du langage, l'exécution de la machine virtuelle et les outils de sécurité, ce qui permet d'éviter efficacement de nombreuses vulnérabilités courantes. Cependant, il est toujours recommandé d'utiliser des services d'audit de sécurité tiers et de faire rédiger et valider le code conforme par des entreprises de sécurité.