Analyse de la sécurité du langage Move

Le langage Move, en tant que nouveau langage de contrat intelligent de génération, a été conçu dès le départ en mettant l'accent sur la sécurité. 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 été conçu en abandonnant certaines caractéristiques plus flexibles mais moins sûres, telles que l'appel dynamique et l'appel externe récursif. En revanche, il introduit des concepts tels que les génériques, le stockage global et les ressources pour réaliser un modèle de programmation sécurisé.

Voici un exemple simple d'implémentation de jeton :

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

const ADMIN: adresse = @0x1;

struct Coin a une clé { valeur: u64 }
struct Info a une clé { total_supply: u64 }

invariant pour tout a: adresse où existe<coin>(a):
    global\u003ccoin\u003e(a).value \u003c= global\u003cinfo\u003e(ADMIN).total_supply;

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

fonction publique mint(compte: &signataire, montant: u64): Pièce {
    assert!(signer::address_of(account) == ADMIN, 0);
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    Coin { value: montant }
}

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

}

Cet exemple présente certaines caractéristiques importantes du langage Move :

1. Modularité : le code est organisé en modules et peut importer des types et des fonctions d'autres modules.

2. Structure : Utilisez struct pour définir des structures de données, vous pouvez ajouter des balises de capacité comme key.

3. Stockage global : gérer l'état global via des opérations telles que move_to et borrow_global_mut.

4. Sécurité des ressources : garantir l'utilisation sécurisée des ressources grâce au système de capacités et aux types linéaires.

5. Invariants : il est possible de définir des règles d'invariants pour une vérification statique.

Le langage Move garantit la sécurité à la compilation grâce à un vérificateur de bytecode et à des contrôles d'invariants:

• Vérificateur de bytecode : vérifie la validité de la structure, la sémantique logique des processus, les erreurs de liaison, etc.

• Vérification des invariants : vérifier si l'état du programme satisfait les règles d'invariant prédéfinies.

2. Le mécanisme de fonctionnement de Move

Le programme Move s'exécute dans une machine virtuelle, dont l'état d'exécution est composé de la pile d'appels, de la mémoire, des variables globales et de la pile d'opérandes. Les principales caractéristiques incluent :

1. Exécuter dans un environnement contrôlé, sans accès direct à la mémoire système.

2. Utiliser un interpréteur basé sur une pile, facilitant la mise en œuvre et le contrôle.

3. Les ressources ne peuvent être déplacées, pas copiées.

4. La pile d'appels enregistre le contexte d'exécution, prenant en charge les sauts statiques.

5. Séparation de la logique de stockage et d'appel des données, améliorant la sécurité et l'efficacité d'exécution.

Ce design évite certains problèmes de sécurité courants, tels que les attaques par réinjection.

3. Déplacer le prouveur

Move Prover est un outil de vérification formelle qui aide les développeurs à vérifier la correctitude des contrats intelligents. Son flux de travail est le suivant :

1. Recevoir le code source et les spécifications Move comme entrée.

2. Analyser le code source, extraire la norme.

3. Convertir le code et les spécifications en modèle d'objet de validateur.

4. Générer le code intermédiaire Boogie.

5. Utiliser le solveur SMT Z3 pour vérifier si la spécification est valable.

6. Générer un rapport de diagnostic, en signalant les problèmes potentiels.

Move Prover utilise le Move Specification Language pour décrire les spécifications de comportement des programmes, pouvant être rédigé indépendamment du code métier. Cela fournit un support de vérification formelle puissant pour les contrats intelligents.

Résumé

Le langage Move a été conçu en tenant pleinement compte de la sécurité, offrant une protection complète grâce aux caractéristiques du langage, à l'exécution de la machine virtuelle et aux outils de vérification. Il peut efficacement éviter de nombreuses vulnérabilités courantes des contrats intelligents, telles que les réentrées et les débordements. Cependant, les erreurs logiques et les problèmes de gestion des autorisations nécessitent encore une attention particulière de la part des développeurs. Il est recommandé aux développeurs de contrats intelligents Move, en plus d'utiliser les caractéristiques du langage et les outils de vérification, de rechercher également des services d'audit de sécurité tiers pour garantir davantage la sécurité des contrats.