Un guide des outils de sécurité pour les contrats intelligents

Nous allons utiliser trois techniques de test et d'analyse de programme distinctes :

• Analyse statique avec Slither. Tous les chemins du programme sont approchés et analysés en même temps, à travers différentes présentations du programme (p. ex., graphe de contrôle de flux)
• Fuzzing avec Echidna. Le code est exécuté avec une génération pseudo-aléatoire de transactions. Le fuzzer tentera de trouver une séquence de transactions pour violer une propriété donnée.
• Exécution symbolique avec Manticore. Une technique de vérification formelle qui traduit chaque chemin d'exécution en une formule mathématique, sur laquelle on pourra vérifier les contraintes.

Chaque technique a ses avantages et ses inconvénients, et sera utile dans des cas spécifiques :

* si tous les chemins sont explorés sans expiration de délai

Slither analyse les contrats en quelques secondes. Cependant, l'analyse statique peut générer des faux positifs et sera moins adaptée aux vérifications complexes (p. ex., les vérifications arithmétiques). Exécutez Slither via l'API pour un accès en un clic aux détecteurs intégrés ou via l'API pour des vérifications définies par l'utilisateur.

Echidna doit s'exécuter pendant plusieurs minutes et ne produit que de vrais positifs. Echidna vérifie les propriétés de sécurité fournies par l'utilisateur, écrites en Solidity. Il peut passer à côté de bogues, car il est basé sur une exploration aléatoire.

Manticore effectue l'analyse la plus poussée. Comme Echidna, Manticore vérifie les propriétés fournies par l'utilisateur. Son exécution prendra plus de temps, mais il peut prouver la validité d'une propriété et ne signalera pas de faux positifs.

Flux de travail suggéré

Commencez par les détecteurs intégrés de Slither pour vous assurer qu'aucun bogue simple n'est présent ou ne sera introduit ultérieurement. Utilisez Slither pour vérifier les propriétés liées à l'héritage, aux dépendances entre les variables et aux problèmes structurels. À mesure que la base de code s'agrandit, utilisez Echidna pour tester les propriétés plus complexes de la machine d'état. Revenez à Slither pour développer des vérifications personnalisées pour des protections non disponibles dans Solidity, comme la protection contre la redéfinition d'une fonction. Enfin, utilisez Manticore pour effectuer une vérification ciblée des propriétés de sécurité critiques, p. ex., les opérations arithmétiques.

• Utilisez la CLI de Slither pour détecter les problèmes courants
• Utilisez Echidna pour tester les propriétés de sécurité de haut niveau de votre contrat
• Utilisez Slither pour écrire des vérifications statiques personnalisées
• Utilisez Manticore lorsque vous souhaitez une assurance approfondie des propriétés de sécurité critiques

Remarque sur les tests unitaires. Les tests unitaires sont nécessaires pour créer des logiciels de haute qualité. Cependant, ces techniques ne sont pas les plus adaptées pour trouver des failles de sécurité. Ils sont généralement utilisés pour tester les comportements positifs du code (c'est-à-dire que le code fonctionne comme prévu dans le contexte normal), tandis que les failles de sécurité ont tendance à se trouver dans des cas limites que les développeurs n'ont pas envisagés. Dans notre étude portant sur des dizaines d'audits de sécurité de contrats intelligents, la couverture des tests unitaires n'a eu aucun effet sur le nombre ou la gravité des failles de sécurité (opens in a new tab) que nous avons trouvées dans le code de nos clients.

Détermination des propriétés de sécurité

Pour tester et vérifier efficacement votre code, vous devez identifier les zones qui nécessitent une attention particulière. Vos ressources en matière de sécurité étant limitées, il est important de cibler les parties faibles ou à forte valeur de votre base de code afin d'optimiser vos efforts. La modélisation des menaces peut vous aider. Envisagez de consulter :

• Rapid Risk Assessments (opens in a new tab) (notre approche privilégiée lorsque le temps est limité)
• Guide to Data-Centric System Threat Modeling (opens in a new tab) (alias NIST 800-154)
• Shostack threat modeling (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Use of Assertions (opens in a new tab)

Composants

Savoir ce que vous voulez vérifier vous aidera également à sélectionner le bon outil.

Les grands domaines qui sont souvent pertinents pour les contrats intelligents sont les suivants :

• Machine d'état. La plupart des contrats peuvent être représentés comme une machine d'état. Envisagez de vérifier que (1) aucun état non valide ne peut être atteint, (2) si un état est valide, il peut être atteint, et (3) aucun état ne bloque le contrat.

  • Echidna et Manticore sont les outils à privilégier pour tester les spécifications des machines d'état.

• Contrôles d'accès. Si votre système a des utilisateurs privilégiés (p. ex., un propriétaire, des contrôleurs, etc.) vous devez vous assurer que (1) chaque utilisateur ne peut effectuer que les actions autorisées et (2) aucun utilisateur ne peut bloquer les actions d'un utilisateur plus privilégié.

  • Slither, Echidna et Manticore peuvent vérifier la correction des contrôles d'accès. Par exemple, Slither peut vérifier que seules les fonctions sur liste blanche n'ont pas le modificateur onlyOwner. Echidna et Manticore sont utiles pour un contrôle d'accès plus complexe, comme une autorisation accordée uniquement si le contrat atteint un état donné.

• Opérations arithmétiques. La vérification de la justesse des opérations arithmétiques est essentielle. L'utilisation de SafeMath partout est une bonne mesure pour empêcher les dépassements/soupassements de capacité. Cependant, vous devez toujours tenir compte des autres défauts arithmétiques, y compris les problèmes d'arrondi et les défauts qui bloquent le contrat.

  • Manticore est ici le meilleur choix. Echidna peut être utilisé si l'arithmétique est hors du champ d'application du solveur SMT.

• Correction de l'héritage. Les contrats Solidity reposent fortement sur l'héritage multiple. Des erreurs telles qu'une fonction masquée omettant un appel super et un ordre de linéarisation C3 mal interprété peuvent facilement être introduites.

  • Slither est l'outil qui permet de garantir la détection de ces problèmes.

• Interactions externes. Les contrats interagissent les uns avec les autres, et il ne faut pas faire confiance à certains contrats externes. Par exemple, si votre contrat dépend d'oracles externes, restera-t-il sécurisé si la moitié des oracles disponibles sont compromis ?

  • Manticore et Echidna sont le meilleur choix pour tester les interactions externes avec vos contrats. Manticore dispose d'un mécanisme intégré pour simuler les contrats externes.

• Conformité aux standards. Les standards Ethereum (p. ex., ERC20) ont un historique de failles dans leur conception. Soyez conscient des limites du standard sur lequel vous vous basez.

  • Slither, Echidna et Manticore vous aideront à détecter les écarts par rapport à un standard donné.

Aide-mémoire de sélection d'outils

D'autres domaines devront être vérifiés en fonction de vos objectifs, mais ces grands axes de travail constituent un bon point de départ pour tout système de contrat intelligent.

Nos audits publics contiennent des exemples de propriétés vérifiées ou testées. Pensez à lire les sections Test et vérification automatisés des rapports suivants pour examiner des propriétés de sécurité du monde réel :

• 0x (opens in a new tab)
• Balancer (opens in a new tab)

Dernière mise à jour de la page : 22 octobre 2025

p (opens in a new tab)

m (opens in a new tab)

c (opens in a new tab)

+9

Voir les contributeurs