Analyse de la sécurité du langage Move : percée du nouveau langage de smart contracts
Le langage Move est un langage de smart contracts conçu pour l'environnement blockchain, avec des caractéristiques de sécurité uniques. Cet article examine 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 abandonné des caractéristiques plus flexibles mais peu sûres, telles que la dispatch dynamique et les appels externes récursifs, pour adopter des concepts comme les génériques, le stockage global et les ressources afin de réaliser des modèles de programmation alternatifs. Ces conceptions aident à éviter des vulnérabilités courantes telles que la réentrée.
Le mécanisme de sécurité central de Move comprend :
Module : chaque module est composé d'un type de structure et d'une définition de processus, et peut importer les définitions de type d'autres modules et appeler leurs processus.
Structure : peut être défini comme un type de ressource, stocké dans le stockage clé-valeur global.
Processus : définit les fonctionnalités et la logique du contrat.
Stockage global : permet le stockage persistant des données, qui ne peut être lu ou écrit que par le module propriétaire de manière programmatique.
Vérification d'invariant : définir la conservation de l'état du système à l'aide d'un langage de spécification.
Vérificateur de bytecode : impose un système de types au niveau du bytecode, empêchant les opérations illégales sur les valeurs sensibles.
2. Mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle et ne peut pas accéder directement à la mémoire système. MoveVM utilise un interpréteur basé sur une pile pour exécuter des instructions de bytecode, séparant la gestion des données et de la pile d'appels.
L'état du programme Move est composé de la pile d'appels, de la mémoire, des variables globales et des opérations. Pendant l'exécution, la pile d'appels conserve des informations contextuelles, le saut statique évite la distribution dynamique, renforçant ainsi l'immuabilité des appels de fonctions.
Ce design sépare l'état des utilisateurs (, les ressources ) et la logique du programme, ce qui améliore la sécurité et l'efficacité d'exécution.
3. Move Prover
Move Prover est un outil de vérification formelle qui utilise un algorithme de vérification déductive pour vérifier si un programme répond aux attentes. Son flux de travail est le suivant :
Recevoir les fichiers sources Move et les spécifications
Compiler en bytecode et modèle d'objet de validateurs
Convertir en langage intermédiaire Boogie
Générer des conditions de vérification
Utiliser le solveur Z3 pour vérifier la satisfaisabilité de la formule
Générer un rapport de diagnostic
Le Move Specification Language est utilisé pour décrire les spécifications du comportement des programmes, et peut être écrit indépendamment du code métier. Cela fournit une voie de validation supplémentaire pour les sociétés de sécurité tierces.
Résumé
Le langage Move a été conçu en tenant compte de la sécurité, avec une optimisation complète des caractéristiques du langage, de l'exécution de la machine virtuelle aux outils de vérification. Il peut efficacement éviter des vulnérabilités courantes telles que les réinjections et les débordements, mais il est toujours nécessaire de prêter attention aux problèmes de sécurité liés à l'authentification et à la logique.
Bien que Move offre une meilleure sécurité, il est recommandé aux développeurs d'utiliser des services d'audit tiers et de considérer la rédaction et la validation des spécifications par une équipe de sécurité professionnelle pour améliorer davantage la sécurité des smart contracts.
Cette page peut inclure du contenu de tiers fourni à des fins d'information uniquement. Gate ne garantit ni l'exactitude ni la validité de ces contenus, n’endosse pas les opinions exprimées, et ne fournit aucun conseil financier ou professionnel à travers ces informations. Voir la section Avertissement pour plus de détails.
11 J'aime
Récompense
11
9
Partager
Commentaire
0/400
DaoResearcher
· 07-23 18:12
D'après le chapitre trois du document de gouvernance de Vitalik, ce design en pile est plus sûr que l'EVM dans plus de 67 % des cas.
Voir l'originalRépondre0
ShibaOnTheRun
· 07-23 17:08
L'audit, l'audit, il faut encore faire l'audit.
Voir l'originalRépondre0
BearMarketSurvivor
· 07-23 03:14
move est si puissant ? Apprends-le.
Voir l'originalRépondre0
NullWhisperer
· 07-23 01:37
théoriquement sécurisé, nécessite encore des tests de pénétration... typique de la confiance excessive dans les méthodes formelles à vrai dire
Voir l'originalRépondre0
MEVHunterLucky
· 07-20 19:12
La spéculation sur move est de retour.
Voir l'originalRépondre0
MEVHunterBearish
· 07-20 19:11
move doit encore grimper
Voir l'originalRépondre0
¯\_(ツ)_/¯
· 07-20 19:11
Test est test, la sécurité avant tout
Voir l'originalRépondre0
LowCapGemHunter
· 07-20 19:07
Je m'en vais, je m'en vais, l'audit reste le plus fiable.
Analyse des caractéristiques de sécurité du langage Move : créer un environnement de développement de smart contracts plus sûr
Analyse de la sécurité du langage Move : percée du nouveau langage de smart contracts
Le langage Move est un langage de smart contracts conçu pour l'environnement blockchain, avec des caractéristiques de sécurité uniques. Cet article examine 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 abandonné des caractéristiques plus flexibles mais peu sûres, telles que la dispatch dynamique et les appels externes récursifs, pour adopter des concepts comme les génériques, le stockage global et les ressources afin de réaliser des modèles de programmation alternatifs. Ces conceptions aident à éviter des vulnérabilités courantes telles que la réentrée.
Le mécanisme de sécurité central de Move comprend :
Module : chaque module est composé d'un type de structure et d'une définition de processus, et peut importer les définitions de type d'autres modules et appeler leurs processus.
Structure : peut être défini comme un type de ressource, stocké dans le stockage clé-valeur global.
Processus : définit les fonctionnalités et la logique du contrat.
Stockage global : permet le stockage persistant des données, qui ne peut être lu ou écrit que par le module propriétaire de manière programmatique.
Vérification d'invariant : définir la conservation de l'état du système à l'aide d'un langage de spécification.
Vérificateur de bytecode : impose un système de types au niveau du bytecode, empêchant les opérations illégales sur les valeurs sensibles.
2. Mécanisme de fonctionnement de Move
Le programme Move s'exécute dans une machine virtuelle et ne peut pas accéder directement à la mémoire système. MoveVM utilise un interpréteur basé sur une pile pour exécuter des instructions de bytecode, séparant la gestion des données et de la pile d'appels.
L'état du programme Move est composé de la pile d'appels, de la mémoire, des variables globales et des opérations. Pendant l'exécution, la pile d'appels conserve des informations contextuelles, le saut statique évite la distribution dynamique, renforçant ainsi l'immuabilité des appels de fonctions.
Ce design sépare l'état des utilisateurs (, les ressources ) et la logique du programme, ce qui améliore la sécurité et l'efficacité d'exécution.
3. Move Prover
Move Prover est un outil de vérification formelle qui utilise un algorithme de vérification déductive pour vérifier si un programme répond aux attentes. Son flux de travail est le suivant :
Le Move Specification Language est utilisé pour décrire les spécifications du comportement des programmes, et peut être écrit indépendamment du code métier. Cela fournit une voie de validation supplémentaire pour les sociétés de sécurité tierces.
Résumé
Le langage Move a été conçu en tenant compte de la sécurité, avec une optimisation complète des caractéristiques du langage, de l'exécution de la machine virtuelle aux outils de vérification. Il peut efficacement éviter des vulnérabilités courantes telles que les réinjections et les débordements, mais il est toujours nécessaire de prêter attention aux problèmes de sécurité liés à l'authentification et à la logique.
Bien que Move offre une meilleure sécurité, il est recommandé aux développeurs d'utiliser des services d'audit tiers et de considérer la rédaction et la validation des spécifications par une équipe de sécurité professionnelle pour améliorer davantage la sécurité des smart contracts.