Analyse de la sécurité du langage Move : un innovateur dans le domaine des smart contracts

Le langage Move est un langage de contrat intelligent qui peut s'exécuter dans un environnement blockchain prenant en charge MoveVM. Son design prend en compte de nombreux problèmes de sécurité liés à la blockchain et aux contrats intelligents, tout en s'inspirant de certaines idées de conception de sécurité du langage Rust. En tant que langage de contrat intelligent de nouvelle génération axé sur la sécurité, quelle est réellement la sécurité de Move ? Peut-il éviter les menaces de sécurité courantes des machines virtuelles de contrats telles que EVM et WASM au niveau du langage ou grâce à des mécanismes connexes ? Existe-t-il des vulnérabilités de sécurité uniques à Move ?

Cet article explorera les problèmes de sécurité du langage Move sous trois aspects : les caractéristiques linguistiques, le mécanisme de fonctionnement et les outils de validation.

1. Les caractéristiques de sécurité du langage Move

Contrairement à de nombreux langages de programmation existants, le langage Move est conçu pour permettre l'écriture de programmes capables d'interagir en toute sécurité avec du code non fiable, tout en soutenant la vérification statique. Move abandonne la logique non linéaire basée sur la flexibilité, ne prend pas en charge le dispatch dynamique et les appels externes 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. Par exemple, Move omet les caractéristiques de planification dynamique et d'appels récursifs, qui peuvent facilement conduire à des vulnérabilités de réentrance coûteuses dans d'autres langages de smart contracts.

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

1. Module: Chaque module Move est composé d'une série de types de structures 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.

2. Structure : peut être défini comme un type de ressource, représentant ce qui peut être stocké dans un stockage clé/valeur global persistant.

3. Processus : définir les fonctionnalités et la logique du module.

4. Stockage global : permet aux programmes Move de stocker des données persistantes, ces données ne peuvent être lues et écrites par programmation que par le module qui les possède.

5. Vérification des invariants : il est possible de définir des invariants pour une vérification statique, garantissant la conservation de l'état du système.

6. vérificateur de code d'octets : applique le système de types au niveau du code d'octets pour empêcher les opérations illégales.

Grâce à ces caractéristiques de sécurité, Move offre un environnement de programmation plus sûr et fiable pour le développement de smart contracts.

2. Mécanisme d'exécution 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 permet à Move de fonctionner en toute sécurité dans des environnements non fiables.

Le programme Move s'exécute sur la pile, le stockage global est divisé en deux parties : la mémoire (, la pile ) et les variables globales (. La mémoire est un stockage de premier ordre, elle 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 la méthode d'indexation est différente de celle de la mémoire.

Les instructions de bytecode de Move sont exécutées dans un interpréteur basé sur une pile. Par rapport à un interpréteur basé sur des registres, un interpréteur basé sur une pile est plus facile à contrôler et à détecter les opérations de copie et de déplacement entre les variables.

L'état d'exécution du programme Move est un quadruplet ⟨C, M, G, S⟩, comprenant la pile d'appels )C(, la mémoire )M(, les variables globales )G( et les opérandes )S(. La pile maintient également une table de fonctions 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 principale différence avec l'EVM. 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 permissions et aux ressources. Bien que cette conception sacrifie une certaine flexibilité, elle permet d'obtenir des améliorations significatives en matière de sécurité et d'efficacité d'exécution.

3. Move Prover

Move Prover est un outil de vérification formelle basé sur le raisonnement, qui décrit le comportement des programmes à l'aide d'un langage formel et utilise des algorithmes de raisonnement pour vérifier si le programme répond aux attentes. Il peut aider les développeurs à garantir la correctitude des smart contracts et à réduire le risque de transaction.

Move Prover utilise un algorithme de vérification par déduction pour inférer le comportement des programmes en fonction des informations connues, garantissant qu'il correspond au comportement attendu. Cela contribue à assurer la correction des programmes et à réduire la charge de travail des tests manuels.

Le flux de travail de Move Prover est le suivant :

1. Recevoir le fichier source Move comme entrée, qui contient les spécifications d'entrée du programme.

2. Move Parser extrait les normes du code source.

3. Le compilateur Move compile le fichier source en bytecode, qui est ensuite transformé en modèle d'objet validateur avec le système de normes.

4. Le modèle d'objet est traduit en langage intermédiaire Boogie.

5. Le système de vérification Boogie génère des "conditions de vérification" pour les entrées.

6. Conditions de vérification transmises au solveur Z3 (, le solveur SMT développé par Microsoft ).

7. Z3 vérifie si la formule SMT est insatisfaisable. Si c'est le cas, cela signifie que la spécification est valide ; sinon, un modèle satisfaisant les conditions est généré.

8. Restaurer le rapport de diagnostic au niveau du code source.

Move utilise le Move Specification Language pour décrire les spécifications du système, qui est un sous-ensemble du langage Move, supportant la description statique du comportement de la correction des programmes, sans affecter la production. Les spécifications peuvent être écrites de manière indépendante, facilitant la séparation du code métier et du code de vérification formelle.

Move Prover est un outil puissant qui aide les développeurs à garantir la correctitude des smart contracts, à réduire les risques de transaction et à renforcer la confiance lors du déploiement des smart contracts en environnement de production.

4. Résumé

Le langage Move excelle dans la conception de la sécurité, prenant en compte de manière exhaustive les caractéristiques linguistiques, l'exécution de la machine virtuelle et les outils de sécurité. Les caractéristiques du langage sacrifient une certaine flexibilité, imposant des vérifications de type strictes et une logique linéaire, ce qui favorise l'automatisation et la vérifiabilité des vérifications de compilation et des validations formelles. La conception de MoveVM sépare l'état de la logique, répondant mieux aux besoins de gestion de la sécurité des actifs blockchain.

Sur le plan linguistique, Move peut efficacement éviter les vulnérabilités courantes de l'EVM telles que la réentrance, le débordement, l'injection Call/DeleGateCall, etc. Cependant, des problèmes tels que l'authentification, la logique du code et le débordement des structures de grands entiers doivent encore être traités avec prudence par les développeurs. Bien que Move Prover soit puissant, il peut ne pas fonctionner correctement en cas de négligence dans la conception globale.

Bien que le langage Move offre aux programmeurs plusieurs garanties de sécurité, il n'existe pas de langage et de programme totalement sûrs. Il est conseillé aux développeurs de smart contracts Move d'utiliser des services d'audit de sociétés de sécurité tierces et de confier la rédaction et la vérification de certaines parties du code de specification à des équipes de sécurité professionnelles, afin d'améliorer davantage la sécurité des contrats.