Analyse de la sécurité du langage Move : le révolutionnaire des nouveaux langages de smart contracts

Le langage Move, en tant que nouveau type de smart contracts, a été conçu dès le départ en tenant compte des problèmes de sécurité liés à la blockchain et aux smart contracts, tout en s'inspirant de certaines idées de conception sécuritaire du langage Rust. Cet article explorera la sécurité du langage Move à travers trois aspects : 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 dans sa conception de nombreuses logiques non linéaires basées sur la flexibilité, ne supporte pas les appels externes dynamiques et récursifs, mais introduit des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation alternatifs. Ces caractéristiques aident à éviter les vulnérabilités courantes telles que la réentrance dans d'autres langages de smart contracts.

Les principales composantes du langage Move comprennent :

• Module (: composé d'une série de types de structures et de définitions de processus
• Structures ) : peuvent être définies comme des types de ressources, stockées dans un stockage clé/valeur global persistant.
• processus ( fonction ) : définir les fonctionnalités spécifiques du contrat

Les deux concepts importants du langage Move sont les types de ressources et le stockage global. Le stockage global permet aux programmes Move de stocker des données persistantes, qui ne peuvent être lues et écrites de manière programmatique que par le module qui les possède, mais qui sont stockées dans un grand livre public et peuvent être consultées. Les types de ressources garantissent un accès exclusif au stockage global.

Le langage Move assure la sécurité du code au moment de la compilation grâce à deux mécanismes : la vérification des invariants et le vérificateur de bytecode.

• Vérification des invariants : définir la conservation de l'état du système à travers un langage de spécification
• Vérificateur de bytecode : effectue des vérifications de type de sécurité et de linéarisation, y compris la vérification de la légalité des structures, la détection sémantique de la logique des processus et la vérification des erreurs au moment de la liaison, etc.

2. Mécanisme de fonctionnement de Move

Le programme Move s'exécute dans une machine virtuelle, et il ne peut pas accéder à la mémoire système pendant l'exécution, ce qui garantit un fonctionnement sécurisé dans un environnement non fiable.

Le programme Move s'exécute sur la pile, son état est composé de la pile d'appels, de la mémoire, des variables globales et des opérations. Les instructions bytecode de Move s'exécutent dans un interpréteur basé sur la pile, ce qui facilite la copie et le contrôle du déplacement entre les variables.

Move VM sépare le stockage des données et la pile d'appels, ce qui diffère considérablement de l'EVM. L'état utilisateur est stocké de manière indépendante, et les appels de programme doivent respecter les règles d'autorisation et de ressources, ce qui améliore la sécurité et l'efficacité d'exécution, tout en sacrifiant une certaine flexibilité.

3. Déplacer le Prover

Move Prover est un outil de vérification formelle fourni par le langage Move, utilisant un algorithme de vérification déductive pour vérifier si le programme est conforme aux attentes. Son flux de travail est le suivant :

1. Recevoir le fichier source Move et les spécifications comme entrée
2. Extraire les spécifications et compiler le fichier source en bytecode
3. Convertir en modèle d'objet validateurs
4. Traduire en langage intermédiaire Boogie
5. Générer les conditions de vérification
6. Utiliser le solveur Z3 pour vérifier la satisfaisabilité des formules
7. Générer le rapport de diagnostic

Move Prover utilise le Move Specification Language pour décrire des systèmes de spécification, qui est un sous-ensemble du langage Move.

Résumé

Le langage Move prend en compte la sécurité de manière exhaustive en termes de caractéristiques linguistiques, d'exécution de la machine virtuelle et d'outils de sécurité. Il peut éviter efficacement les vulnérabilités courantes telles que les réentrées, les dépassements et les injections, mais ne peut toujours pas éviter complètement les problèmes d'authentification et de logique. Il est conseillé aux développeurs de smart contracts Move d'utiliser des services d'audit de sécurité tiers et de confier la rédaction de codes de spécification de vérification.