Analyse de la sécurité du langage Move : le révolutionnaire des smart contracts

Le langage Move est un langage de contrat intelligent qui peut être compilé et exécuté dans un environnement blockchain implémentant MoveVM. En tant que langage de contrat intelligent de nouvelle génération axé sur la sécurité, quelle est sa sécurité ? Peut-il éviter les menaces de sécurité courantes des machines virtuelles de contrat comme EVM, WASM, etc. ? Cet article explorera les problèmes de 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

Contrairement à de nombreux langages de programmation existants, le langage Move a été conçu pour prendre en charge à la fois des interactions sécurisées avec du code non fiable et une 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 utilise des concepts tels que les génériques, le stockage global et les ressources pour réaliser des modèles de programmation alternatifs.

Voici un exemple d'implémentation d'un actif token dans le langage Move :

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

const ADMIN: address = @0x1;

struct Coin a une clé, stocke { 
    value: u64
}

struct Info a une clé {
    total_supply: u64  
}

module de spécification {
    invariant forall addr: address where exists<coin>(addr):
        global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}

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

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let coin = Coin { value: amount } ;
    let info = borrow_global_mut\u003cinfo\u003e(ADMIN);
    info.total_supply = info.total_supply + amount;
    pièce
}

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

}

Cet exemple montre certaines caractéristiques de sécurité clés du langage Move :

1. Modulaire : chaque module Move est composé de définitions de types de structure et de procédures, et peut importer des définitions de types d'autres modules et appeler des procédures d'autres modules.

2. Type de ressource : Un type de ressource est défini par une structure marquée par has key ou store, et peut être stocké dans un stockage clé-valeur global persistant.

3. Stockage global : permet aux programmes Move de stocker des données persistantes, qui ne peuvent être lues ou écrites par programmation que par les modules propriétaires, mais qui peuvent être consultées par d'autres modules dans le grand livre public.

4. Contrôle d'accès : Il est possible de réaliser un contrôle d'accès sur les opérations critiques par des assertions et d'autres moyens.

5. Récurrence des invariants : permet de définir des invariants pour une vérification formelle.

6. Vérification du bytecode : inclut les types de sécurité et la vérification de la linéarisation, empêchant les opérations illégales sur les types de ressources.

Ces caractéristiques garantissent ensemble la sécurité du langage Move lors de la compilation.

2. Le mécanisme de fonctionnement de Move

Le programme Move s'exécute dans une machine virtuelle, ne peut pas accéder à la mémoire du système et peut fonctionner en toute sécurité dans un environnement non fiable.

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 ne peut pas stocker de pointeurs vers des cellules de mémoire, les variables globales sont utilisées pour stocker des pointeurs vers des cellules de mémoire.

Les instructions de bytecode de Move s'exécutent dans un interpréteur basé sur une pile, ce qui facilite leur mise en œuvre et leur contrôle, et convient aux scénarios de blockchain. La valeur des types de ressources ne peut être déplacée que de manière destructrice.

L'état d'exécution du programme Move est un quadruplet ⟨C, M, G, S⟩, qui comprend la pile d'appels, la mémoire, les variables globales et les opérandes. Au cours de l'exécution, l'appel de fonction crée un nouvel objet de pile d'appels, et les instructions de branchement effectuent un saut statique, évitant ainsi la dispatch dynamique.

MoveVM sépare le stockage des données et la pile d'appels, contrairement à la conception de l'EVM. Bien que ce design sacrifie la flexibilité, il améliore la sécurité et l'efficacité d'exécution.

3. Move Prover

Move Prover est un outil de vérification formelle basé sur le raisonnement, utilisant un langage formel pour décrire le comportement des programmes et des algorithmes de raisonnement pour vérifier si le programme est conforme aux attentes.

L'architecture de Move Prover est la suivante :

1. Recevoir le fichier source Move en entrée, y compris les spécifications du programme.
2. Le parseur extrait la spécification, le compilateur compile le code source en bytecode.
3. Convertir en modèle d'objet validateur.
4. Traduire en langage intermédiaire Boogie.
5. Le système de vérification Boogie génère les conditions de vérification.
6. Le solveur Z3 vérifie si la formule SMT est insatisfaisable.
7. Générer un rapport de diagnostic et le restaurer en erreurs au niveau du code source.

Move utilise le Move Specification Language pour décrire les spécifications, qui est un sous-ensemble du langage Move.

Move Prover est un outil utile qui aide les développeurs à garantir la correction des smart contracts et à réduire les risques de transaction.

Résumé

Le langage Move excelle dans la conception de la sécurité, en prenant en compte de manière exhaustive les caractéristiques du langage, l'exécution de la machine virtuelle et les outils de sécurité. Il sacrifie une partie de la flexibilité pour renforcer la vérification des types et la logique linéaire, facilitant ainsi la vérification par compilation et la vérification formelle. MoveVM sépare l'état de la logique, ce qui répond mieux aux besoins de gestion de la sécurité des actifs blockchain.

Le langage Move peut efficacement éviter les vulnérabilités courantes de l'EVM telles que les réentrées, les débordements et les injections, mais les problèmes d'authentification, de logique et de débordement de grands entiers doivent toujours être surveillés par les développeurs. Bien que Move prenne en compte la sécurité, il est tout de même recommandé d'utiliser les services d'audit d'entreprises de sécurité tierces et de confier la rédaction et la vérification du code aux équipes de sécurité professionnelles.