Analyse de la sécurité du langage Move

Introduction

Move est un langage de contrat intelligent qui fonctionne dans un environnement blockchain implémentant MoveVM. Dès sa création, il a pris en compte de nombreux problèmes de sécurité liés aux blockchains et aux contrats intelligents, tout en s'inspirant de certaines conceptions de sécurité du langage RUST. En tant que nouveau langage de contrat intelligent principalement axé sur la sécurité, quelle est la sécurité de Move ? Peut-il éviter les menaces de sécurité courantes des machines virtuelles de contrat comme EVM, WASM, etc., au niveau du langage ou des mécanismes connexes ? Existe-t-il des vulnérabilités de sécurité particulières à lui-même ?

Cet article explorera les problèmes de sécurité du langage Move sous trois aspects : les caractéristiques linguistiques, le mécanisme d'exécution et les outils de vérification.

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

Contrairement à de nombreux langages de programmation existants, Move a été conçu pour prendre en charge à la fois une interaction sécurisée avec du code non fiable et la vérification statique. Move possède ces caractéristiques de sécurité parce qu'il abandonne la logique non linéaire basée sur la flexibilité, ne prend pas en charge la dispatch dynamique, ni les appels externes récursifs, mais utilise des concepts tels que les génériques, le stockage global, les ressources, etc., pour réaliser des modèles de programmation alternatifs. Par exemple, Move omet les caractéristiques de dispatch dynamique et d'appels récursifs qui pourraient entraîner des vulnérabilités de réentrance.

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

Le module 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 les définitions de types déclarées par d'autres modules et appeler leurs 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 ) fonction ( : définir les fonctions spécifiques du module.

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

5. Vérification des invariants : des invariants pouvant être définis par des vérifications statiques garantissent l'intégrité des ressources dans le système.

6. Vérificateur de bytecode : vérifie les types de sécurité et la linéarisation, empêche la création, la modification ou la destruction illégale de valeurs sensibles.

![Analyse de la sécurité de Move : le changeur de règles du jeu pour les langages de contrat intelligent])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

2. Mécanisme de fonctionnement de Move

Le programme Move s'exécute dans une machine virtuelle et n'a pas accès directement à la mémoire système. Le programme s'exécute sur la pile, le stockage global est divisé en mémoire ), tas ( et variables globales ) pile (.

Les instructions de bytecode Move s'exécutent dans un interpréteur basé sur une pile, cette méthode est facile à mettre en œuvre et à contrôler, nécessite peu de matériel et est adaptée aux scénarios de blockchain. De plus, 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 copies et les déplacements entre les variables.

Au cours de l'exécution, l'état du programme Move est composé de la pile d'appels, de la mémoire, des variables globales et des opérations. La pile d'appels contient toutes les informations contextuelles de l'exécution du processus. Lors de l'exécution de l'instruction Call, un nouvel objet de pile d'appels est créé. Lorsqu'une instruction de branchement est rencontrée, il y a un saut statique à l'intérieur du processus.

Contrairement à EVM, MoveVM sépare le stockage des données et la pile d'appels, ce qui est mieux adapté aux besoins de gestion de la sécurité des actifs sur la blockchain. Cette conception améliore considérablement la sécurité et l'efficacité d'exécution.

![Analyse de la sécurité de Move : le changeur de jeu du langage des contrats intelligents])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

3. Déplacer le 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 est conforme aux attentes. Il peut aider les développeurs à garantir la correctitude des contrats intelligents et à réduire les risques de transaction.

Move Prover utilise un algorithme de vérification par déduction, inférant le comportement du programme à partir des informations connues, afin de s'assurer qu'il correspond au comportement attendu. Cela aide à garantir la correctivité du programme 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
2. Extraire les spécifications et compiler en bytecode
3. Convertir en modèle d'objet de validateur
4. Traduire en langage intermédiaire Boogie
5. Générer les conditions de vérification
6. Vérifier les formules SMT avec le solveur Z3
7. Générer un rapport de diagnostic et le restaurer en tant qu'erreur au niveau du code source.

Le Move Specification Language est utilisé pour décrire des systèmes de spécifications, c'est un sous-ensemble du langage Move, et il prend en charge la description statique du comportement de correction des programmes.

Dans l'ensemble, Move Prover est un outil très utile qui peut aider les développeurs à assurer la validité des contrats intelligents, à réduire les risques de transaction et à accroître la confiance dans le déploiement des contrats intelligents.

![Analyse de la sécurité de Move : le changeur de jeu du langage de contrat intelligent])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(

4. Résumé

Le langage Move excelle dans la conception de la sécurité, en tenant compte de manière globale des caractéristiques du langage, de l'exécution de la machine virtuelle et des outils de sécurité. Il sacrifie une partie de la flexibilité, impose une vérification de type stricte et une logique linéaire, facilitant ainsi la vérification par compilation et la validation formelle. MoveVM sépare l'état de la logique, ce qui le rend plus adapté aux besoins de gestion de la sécurité des actifs blockchain.

Le langage Move peut efficacement éviter les vulnérabilités courantes telles que la réentrance, le débordement, l'injection Call/DeleGateCall dans l'EVM. Cependant, des problèmes tels que l'authentification, la logique de code et le débordement de structures de grands entiers nécessitent encore une attention particulière de la part des développeurs. Bien que Move Prover offre une vérification formelle, cela ne peut pas compenser les lacunes de la conception globale.

Bien que Move ait pris de nombreuses considérations en matière de sécurité, il n'existe pas de langage ou de programme complètement sécurisé. Il est conseillé aux développeurs de contrats intelligents Move d'utiliser les services d'audit d'entreprises de sécurité tierces et de confier la rédaction et la vérification des normes à des équipes de sécurité professionnelles.