Discussion sur la sécurité du langage Move : analyse complète des caractéristiques, mécanismes et outils de validation

Avant-propos

Le langage Move, en tant que nouveau langage de contrat intelligent de génération, se caractérise principalement par sa sécurité. Cet article explorera la question de la sécurité du langage Move sous trois aspects : les caractéristiques du langage, le mécanisme d'exécution et les outils de validation.

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

Le langage Move abandonne la logique non linéaire, ne prend pas en charge l'appel externe dynamique et la récursivité, 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 simple de mise en œuvre d'un actif de jeton :

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

const ADMIN: adresse = @0x1;

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

struct Info a une clé {
    total_supply: u64  
}

// L'offre totale est égale à la somme des valeurs de tous les Coins
invariant pour tout addr: adresse où existe<coin>(addr):
    global\u003cinfo\u003e(ADMIN).total_supply == sum(select Coin.value (global\u003ccoin\u003e(addr)));

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

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

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

}

Les deux mécanismes de sécurité importants du langage Move :

a) Vérification des invariants : définir la conservation de l'état par le langage de réduction.

b) Vérificateur de bytecode : exécution contraignante de types de sécurité et linéarisation, empêchant les opérations illégales.

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. L'état du programme est composé de la pile d'appels, de la mémoire, des variables globales et des tableaux d'opération.

MoveVM sépare le stockage des données et la pile d'appels, améliorant ainsi la sécurité et l'efficacité d'exécution. Le stockage indépendant des ressources et le contrôle d'accès strict évitent efficacement certaines vulnérabilités courantes.

3. Déplacer le Prover

Move Prover est un outil de vérification formelle qui utilise des algorithmes de vérification déductive pour valider la correctivité des programmes. Son architecture est la suivante :

1. Recevoir les fichiers source Move et les spécifications
2. Compiler en bytecode et modèle d'objet de validateur
3. Convertir en langage intermédiaire Boogie
4. Conditions de validation générées
5. Vérification à l'aide du solveur Z3
6. Sortie du rapport de diagnostic

Le Move Specification Language est utilisé pour décrire les spécifications de comportement des programmes, et peut être écrit indépendamment du code métier.

4. Résumé

Le langage Move prend en compte la sécurité de manière exhaustive sur les aspects des caractéristiques du langage, de l'exécution de la machine virtuelle et des outils de sécurité. Il peut efficacement éviter certaines vulnérabilités courantes, mais il est toujours nécessaire de prêter attention aux problèmes d'authentification, de logique, etc. Il est conseillé aux développeurs d'utiliser des audits de sécurité tiers et de confier la validation des normes à des entreprises de sécurité professionnelles.

\u003c/info\u003e\u003c/coin\u003e\u003c/info\u003e\u003c/coin\u003e