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 :

1. Vérification des invariants : définition de la conservation de l'état du système par un langage de spécification.

2. 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 :

1. Recevoir le fichier source Move et les spécifications
2. Compiler en bytecode et modèle d'objet de validateur
3. Convertir en langage intermédiaire Boogie
4. Générer des conditions de validation
5. Vérification avec le solveur Z3
6. 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é.