Analyse de la sécurité du langage Move

Le langage Move, en tant que nouveau langage de contrat intelligent de nouvelle génération, a été conçu dès le départ en tenant pleinement compte des problèmes de sécurité liés aux blockchains et aux contrats intelligents. Cet article analysera la sécurité du langage Move sous 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 a abandonné de nombreuses caractéristiques linguistiques flexibles mais peu sûres, telles que la distribution dynamique, les appels externes récursifs, etc., et a adopté des concepts tels que les types de ressources et le stockage global pour réaliser des modes de programmation sécurisés.

Les principales caractéristiques de sécurité de Move incluent :

• Modularité: encapsuler et gérer le code et les ressources par des modules
• Type de ressource : utilisé pour représenter et gérer des actifs numériques
• Stockage global : offre des capacités de stockage persistantes
• Système de types statiques : vérification des types à la compilation
• Logique linéaire : assurer l'unicité et l'irréplicabilité des ressources

Move propose également deux mécanismes de vérification statique importants :

1. Récurrence des invariants : utilisée pour déclarer et vérifier l'invariance de l'état du système.
2. Vérificateur de bytecode : appliquer la sécurité des types et la logique linéaire au niveau du bytecode.

Ces caractéristiques et mécanismes permettent de détecter et de prévenir de nombreux problèmes de sécurité courants dès la compilation.

2. Mécanisme de fonctionnement de Move

Le programme Move s'exécute dans une machine virtuelle, ne pouvant pas accéder directement à la mémoire système, ce qui garantit la sécurité à l'exécution. MoveVM utilise une structure en pile, séparant la gestion des données et de la pile d'appels.

• Le stockage global se divise en mémoire ( tas ) et variables globales ( pile )
• Utiliser la pile d'appels pour gérer les appels de fonction
• Les instructions sont exécutées dans l'interpréteur basé sur la pile
• La valeur des ressources ne peut être déplacée, mais pas copiée.
• Appel de fonction statique, éviter la distribution dynamique

Ce design améliore l'efficacité d'exécution et la sécurité, empêchant efficacement des attaques telles que les réentrées.

3. Move Prover

Move Prover est un outil de vérification formelle fourni par le langage Move, capable de réaliser une analyse de sécurité automatisée. Il utilise un algorithme de vérification déductive pour valider la correctitude des programmes en se basant sur des spécifications écrites dans le Move Specification Language.

Flux de travail de Move Prover :

1. Analyser le code source et les spécifications de Move
2. Générer un modèle d'objet validateur
3. Convertir en langage intermédiaire Boogie
4. Générer les conditions de validation
5. Vérification à l'aide du solveur SMT Z3
6. Générer un rapport de résultats de vérification

Move Prover est un puissant outil d'assistance qui peut aider les développeurs à améliorer la sécurité des contrats intelligents.

Résumé

Le langage Move a soigneusement pris en compte la sécurité à plusieurs niveaux, y compris la conception du langage, l'exécution de la machine virtuelle et les outils de validation. Il peut efficacement éviter de nombreuses vulnérabilités courantes des contrats intelligents, mais il est toujours nécessaire que les développeurs restent vigilants et il est recommandé d'utiliser des services d'audit de sécurité tiers pour renforcer davantage la sécurité des contrats.