Analyse approfondie de la sécurité du langage Move : caractéristiques du langage, mécanismes d'exécution et audit automatisé

Introduction

Le langage Move est un langage de contrat intelligent pouvant fonctionner dans un environnement blockchain qui met en œuvre MoveVM. Il a été conçu en tenant compte de nombreux problèmes de sécurité liés à la blockchain et aux contrats intelligents, et s'inspire de certaines conceptions de sécurité du langage RUST. En tant que langage de contrat intelligent de nouvelle génération, dont la principale caractéristique est la sécurité, quelle est réellement la sécurité de Move ? Peut-il éviter, au niveau du langage ou grâce à des mécanismes connexes, les menaces de sécurité courantes des machines virtuelles de contrat telles que EVM et WASM ? Existe-t-il des problèmes de sécurité spécifiques à lui-même ?

Cet article examinera 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 validation.

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

Écrire un code correct est difficile, même après de nombreux tests, il n'est pas possible de garantir que le code est complètement exempt de vulnérabilités. Il est encore plus difficile d'écrire un code capable de maintenir des propriétés de sécurité clés lors de l'interaction avec du code non fiable. Il existe de nombreuses techniques pour faire respecter la sécurité d'exécution, telles que les sandbox, l'isolement des processus, les verrous d'objets et d'autres modèles de programmation ; il est également possible de spécifier la sécurité statique à la compilation, comme l'imposition de types statiques ou les vérifications d'assertion.

Il est parfois possible d'utiliser des outils d'analyse sémantique et d'analyse statique pour s'assurer que le code respecte les règles de sécurité, même lors d'interactions avec du code non fiable, afin de maintenir certaines invariants logiques démontrables.

Ces solutions semblent intéressantes, car elles peuvent éviter les frais d'exécution et détecter les problèmes de sécurité à l'avance. Mais malheureusement, la sécurité obtenue par les langages de programmation grâce à ces méthodes est extrêmement limitée, pour deux raisons principales : premièrement, elles présentent généralement des caractéristiques qui ne peuvent pas être utilisées avec des outils d'analyse statique, comme la dispatch dynamique, la mutabilité partagée et la réflexion, qui violent les règles d'invariance de sécurité, offrant ainsi aux hackers une large surface d'attaque. Deuxièmement, la plupart des langages de programmation sont difficiles à étendre avec des outils statiques liés à la sécurité ou des langages de spécification fortement expressifs. Bien que ces deux types d'extensions soient importants, ils peuvent être définis à l'avance.

Contrairement à de nombreux langages de programmation existants, le langage Move a été conçu en tenant compte du soutien à l'écriture de programmes interagissant en toute sécurité avec du code non fiable, tout en prenant en charge la validation statique. Move possède ces caractéristiques de sécurité car il a abandonné toute logique non linéaire basée sur la flexibilité, ne prend pas en charge la dispatch dynamique et n'autorise pas les appels externes récursifs, mais utilise plutôt des concepts tels que les génériques, le stockage global et les ressources pour réaliser certains modèles de programmation alternatifs. Par exemple, Move omet les caractéristiques de planification dynamique et d'appels récursifs, des caractéristiques qui entraînent des vulnérabilités de réentrance coûteuses dans d'autres langages de contrats intelligents.

Pour mieux comprendre les caractéristiques du langage Move, examinons un programme exemple :

déplacer module 0x1::TestCoin { utiliser 0x1::signer;

const ADMIN: adresse = @0x1;

struct Coin a une clé, un magasin {
    valeur : u64
}

struct Info a une clé {
    total_supply: u64
}

module de spécifications {
    invariant pour tout addr: adresse où existe<coin>(addr):
        global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 0);
    move_to(compte, Info { total_supply: 0 })
}

public fun mint(compte: &signer, montant: u64): Coin acquires Info {
    assert!(signer::address_of(account) == ADMIN, 0);
    
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    
    Coin { valeur: montant }
}

fonction publique value(coin: &Coin): u64 {
    coin.value
}

public fun value_mut(coin: &mut Coin): &mut u64 {
    &mut coin.value  
}

}

a) Module(: Chaque module Move est composé d'une série de types de structures et de définitions de processus. Les modules peuvent importer des définitions de types et appeler des processus déclarés dans d'autres modules. Le nom complètement qualifié d'un module commence par l'adresse de compte de 16 octets qui stocke le code du module. L'adresse du compte sert d'espace de noms pour distinguer les modules portant le même nom.

b) Structures): Ce module définit deux structures, Coin et Info. Coin représente les jetons attribués aux utilisateurs, Info enregistre la quantité totale de jetons. Les deux structures sont définies comme des types de ressources et peuvent être stockées dans un stockage clé/valeur global persistant.

c( processus)function): le code définit un processus d'initialisation, un processus sécurisé et un processus non sécurisé. Le processus initialize doit être appelé avant de créer un Coin, pour initialiser la valeur total_supply de l'instance Info à zéro. signer est un type spécial, représentant un utilisateur validé par une logique externe Move. L'assertion garantit que seul le compte administrateur spécifié peut appeler ce processus. Le processus mint permet à l'administrateur de créer de nouveaux jetons, avec également un contrôle d'accès. Le processus value_mut accepte une référence mutable à Coin et retourne une référence mutable au champ value.

La structure des contrats est similaire à celle d'autres langages de contrat intelligent, mais les types de ressources et le stockage global sont des mécanismes clés pour la sécurité du stockage et des ressources dans le langage Move.

Le 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, mais qui sont stockées dans un grand livre public, accessible aux utilisateurs d'autres modules. Chaque clé dans le stockage global est composée d'un nom de type entièrement qualifié et de l'adresse du compte qui stocke la valeur de ce type. Bien que le stockage global soit partagé entre tous les modules, chaque module a un accès exclusif en lecture et écriture à la clé qu'il déclare.

Les modules déclarant le type de ressource peuvent : • Publier la valeur dans le stockage global via l'instruction move_to • Supprimer la valeur du stockage global à l'aide de l'instruction move_from • Obtenir une référence à une valeur dans le stockage global via l'instruction borrow_global_mut.

Le module peut imposer des contraintes sur le stockage global qu'il contrôle. Par exemple, il garantit que seule l'adresse du compte ADMIN peut détenir des structures de type Info, en définissant un processus d'initialisation qui utilise move_to sur le type Info et impose les conditions préalables pour appeler move_to à l'adresse ADMIN.

Voici deux mécanismes de vérification statique qui garantissent la sécurité du code de ce module : la réduction d'invariant et le vérificateur de bytecode.

a( Vérification d'invariance ) Vérification de contrat ) : La ligne 10 du module indique l'invariance de vérification statique - la somme des champs de valeur de tous les objets Coin dans le système doit être égale au champ total_value de l'objet Info stocké à l'adresse ADMIN. L'invariance est un terme de vérification formelle, indiquant la conservation des états. Cette propriété de conservation s'applique à tous les clients possibles du module.

b( Vérificateur de bytecode : le type de sécurité et la linéarisation sont les principaux domaines de vérification du vérificateur de bytecode. Bien que d'autres modules ne puissent pas accéder à l'unité de stockage global contrôlée par 0x1::TestCoin::Coin, ils peuvent utiliser ce type dans leurs propres déclarations de processus et de structure.

Move dispose d'un vérificateur de bytecode ) qui applique un système de types au niveau du bytecode ), permettant aux propriétaires de modules d'empêcher des résultats indésirables. Seuls les modules déclarant le type de structure Coin peuvent : • Créer une valeur de type Coin • "Déballer" la valeur du type de Coin dans ses champs composants • Obtenir une référence au champ Coin via un emprunt mutable ou immuable de style rust.

Le validateur impose également que la structure par défaut soit linéaire, afin d'empêcher de manière linéaire la copie et la destruction en dehors des modules déclarant la structure. De plus, le validateur effectuera des vérifications obligatoires sur certains types de problèmes de mémoire courants.

Le processus de détection se divise principalement en trois catégories : 1( Vérification de légitimité de la structure : garantir l'intégrité du code byte, détecter les erreurs de références illégales, les entités de ressources dupliquées et les signatures de type illégales, etc. 2) Détection sémantique de la logique de processus : inclut les erreurs de type de paramètre, les index de boucle, les index vides et les variables redéfinies, etc. 3) Erreur de lien, appel illégal d'un processus interne, ou processus de lien déclarant et définissant non correspondants.

Le validateur crée d'abord le CFG), puis détecte la portée d'accès de l'appelant dans la pile, garantissant que l'appelant du contrat ne peut pas accéder à l'espace de la pile de l'appelant. En même temps, pour vérifier les types, chaque pile de valeurs maintient une pile de types correspondante.

Ensuite, il y a une vérification des ressources et une vérification des références. La vérification des ressources se concentre principalement sur des contraintes telles que l'inabsence de double dépense, l'irrévocabilité et l'obligation d'appartenance. La vérification des références combine une analyse dynamique et statique, utilisant un mécanisme de vérification d'emprunt similaire à celui du système de types rust.

Enfin, il est nécessaire de vérifier à nouveau si les objets de lien et les déclarations correspondent, ainsi que le contrôle d'accès du processus.

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

) 2. Mécanisme de fonctionnement de Move

Tout d'abord, le programme Move s'exécute dans une machine virtuelle et n'a pas accès à la mémoire système pendant l'exécution. Cela permet à Move de fonctionner en toute sécurité dans un environnement non fiable, sans risque d'être compromis ou abusé.

Deuxièmement, le programme Move s'exécute sur la pile. Le stockage global est divisé en mémoire ( tas ) et variables globales ### pile (. La mémoire est un stockage de premier ordre, dont les unités ne peuvent 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. Lors de l'accès aux variables globales, le code fournit l'adresse et le type lié à cette adresse. Cette division simplifie les opérations, rendant la sémantique du langage Move plus facile à formaliser.

Les instructions de bytecode Move s'exécutent dans un interpréteur basé sur une pile. La machine virtuelle basée sur une pile est facile à mettre en œuvre et à contrôler, exige peu de l'environnement matériel, ce qui la rend adaptée aux scénarios de blockchain. Par rapport à un interpréteur basé sur des registres, l'interpréteur basé sur une pile facilite le contrôle et la détection des copies et des mouvements entre les variables.

Dans Move, une valeur définie comme ressource ne peut être déplacée de manière destructrice que si l'emplacement de stockage qui a précédemment sauvegardé cette valeur est invalidé, mais certaines valeurs, comme les entiers, peuvent être copiées.

Lorsque le programme Move s'exécute sur la pile, son état est un quadruplet ⟨C, M, G, S⟩, composé de la pile d'appels )C(, de la mémoire )M(, des variables globales )G( et des opérandes )S(. La pile maintient également une table des fonctions ) pour le module lui-même ( afin d'analyser les instructions contenant le corps de la fonction.

La pile d'appels contient toutes les informations contextuelles et les numéros d'instruction de l'exécution du processus. Lors de l'exécution de l'instruction Call, un nouvel objet de pile d'appels est créé, les paramètres d'appel sont stockés en mémoire et dans des variables globales, puis l'interpréteur exécute les instructions du nouveau contrat. Lorsqu'une instruction de branchement est rencontrée, un saut statique se produit à l'intérieur de ce processus. La dépendance des processus au sein du module est acyclique, et l'absence de désignation dynamique dans le module renforce l'immuabilité des appels de fonction pendant l'exécution : le cadre d'appel du processus procedure doit nécessairement être adjacent, évitant ainsi les possibilités de réentrance. L'appel return met fin à l'appel, la valeur de retour est placée au sommet de la pile.

L'étude du code MoveVM montre que MoveVM sépare le stockage des données et la logique des processus de la pile d'appels ), ce qui constitue la plus grande différence avec l'EVM. Dans l'EVM, la mise en œuvre du Token ERC20 nécessite d'écrire la logique dans un contrat et d'enregistrer l'état de chaque utilisateur, tandis que dans MoveVM, l'état de l'utilisateur ( est stocké de manière indépendante sous l'adresse du compte ), et les appels de programme doivent respecter des règles de permission et des règles obligatoires concernant les ressources. Bien que cela sacrifie une certaine flexibilité, cela contribue à améliorer la sécurité et l'efficacité d'exécution (, permettant ainsi d'obtenir un grand gain en matière d'exécution concurrente ).

( 3. Déplacer le Preuveur

Enfin, découvrons l'outil d'audit automatisé d'assistance fourni par Move, Move prover.

Move Prover est un outil de vérification formelle basé sur le raisonnement. Il utilise un langage formel pour décrire le comportement des programmes et utilise des algorithmes de raisonnement pour vérifier si le programme correspond aux attentes, aidant ainsi les développeurs à garantir la correctitude des contrats intelligents et à réduire les risques de transaction. En d'autres termes, la vérification formelle consiste à prouver sans erreur un système à l'aide de méthodes mathématiques.

Les algorithmes de vérification automatique de logiciels courants reposent actuellement sur des solveurs SMT basés sur la théorie de la satisfaisabilité )SMT solver(. Le solveur SMT est en réalité un solveur de formules. Les algorithmes de vérification de logiciels de niveau supérieur décomposent les objectifs de vérification en formules, qui sont ensuite résolues par le solveur SMT. En fonction des résultats, une analyse plus approfondie est effectuée, et finalement, un rapport est établi pour indiquer si l'objectif de vérification est atteint ou si un contre-exemple a été trouvé.

L'algorithme de vérification de base est la vérification déductive ) dedutive verification (, et il existe d'autres algorithmes de vérification tels que le model checking borné, la méthode d'induction k, l'abstraction de prédicat et l'abstraction de chemin, etc.

Move Prover utilise un algorithme de vérification déductive pour vérifier si un programme se conforme aux attentes. Cela signifie que Move Prover peut inférer le comportement du programme en fonction des informations connues, garantissant ainsi une correspondance avec le comportement attendu. Cela aide à assurer la justesse du programme et à réduire la charge de travail des tests manuels.

L'architecture globale de Move Prover est la suivante :

Tout d'abord, Move Prover reçoit le fichier source Move contenant la spécification d'entrée du programme )specification(. Move Parser extrait la spécification du code source. Le compilateur Move compile le fichier source en bytecode, qui est transformé en modèle d'objet de vérificateur )Prover Object Model### avec le système de spécifications.

Ce modèle est traduit en langage intermédiaire Boogie. Le code Boogie est passé au système de vérification Boogie pour "génération de conditions de vérification". Les conditions de vérification sont passées au solveur Z3 (, un solveur SMT développé par Microsoft ).

Après que VC soit passé à Z3, le vérificateur vérifie si le code du programme SMT ( satisfait à la spécification ) ou s'il 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é, converti de nouveau au format Boogie et un rapport de diagnostic est publié. Le rapport de diagnostic est restauré sous forme d'erreurs au niveau du code source, similaires aux erreurs des compilateurs standards.

![Move安