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 pris en compte de nombreux problèmes de sécurité dès sa conception. 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 présente les caractéristiques de sécurité suivantes :

• A abandonné la distribution dynamique, les appels externes récursifs et autres logiques non linéaires, évitant ainsi les vulnérabilités comme la réentrance.
• Utiliser des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation sécurisés
• Conception modulaire, chaque module est composé d'un type de structure et d'une définition de processus
• Une structure peut être définie comme un type de ressource, stockée dans un stockage clé-valeur global.
• Le stockage global permet de persister des données, accessibles uniquement par les modules qui en possèdent.
• Utilisation de la réduction d'invariance et du vérificateur de bytecode pour les vérifications statiques

Le vérificateur de bytecode effectue principalement :

1. Vérification de la validité de la structure
2. Détection sémantique de la logique de processus
3. Vérification des erreurs lors de la connexion

Grâce à ces mécanismes, le langage Move peut garantir la sécurité du code au moment de la compilation.

2. Mécanisme de fonctionnement de Move

Le programme Move s'exécute dans une machine virtuelle, ses principales caractéristiques incluent :

• Impossible d'accéder à la mémoire système, peut fonctionner en toute sécurité dans un environnement non fiable
• Exécution sur la pile, le stockage global est divisé en mémoire ( pile ) et variables globales ( pile )
• Exécuter des instructions de bytecode à l'aide d'un interpréteur basé sur une pile
• La valeur des ressources ne peut être déplacée que de manière destructive, elle ne peut pas être copiée.
• L'état du programme est composé de la pile d'appels, de la mémoire, des variables globales et des tableaux d'opérations.
• La pile d'appels contient le contexte d'exécution, prend en charge le saut statique.
• La séparation du stockage des données et de la pile d'appels améliore la sécurité et l'efficacité d'exécution.

3. Déplacer le Prover

Move Prover est un outil de vérification formelle capable d'effectuer des audits automatisés :

• Utiliser un algorithme de vérification déductive pour valider la correction du programme
• Recevoir les fichiers sources Move et les spécifications comme entrée
• Convertir le code en langage intermédiaire Boogie
• Utiliser le solveur Z3 SMT pour vérifier si la spécification est valable
• Prend en charge la spécification du langage Move Specification Language
• Peut rédiger des documents de spécifications de manière indépendante, sans affecter le code métier

Move Prover peut aider les développeurs à garantir la validité des contrats intelligents et à réduire les risques de transaction.

Résumé

Le langage Move prend en compte la sécurité de manière exhaustive, y compris les caractéristiques du langage, l'exécution de la machine virtuelle et les outils de sécurité. Il peut efficacement éviter les vulnérabilités courantes telles que les réentrées et les débordements, mais il est toujours nécessaire de prêter attention aux problèmes d'authentification et de logique. Il est recommandé d'utiliser les services d'audit d'entreprises de sécurité tierces et de faire rédiger des codes de spécification de vérification par des professionnels.