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

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

• Analyse statique avec Slither. Tous les chemins du programme sont approximés et analysés en même temps, à travers différentes présentations du programme (ex. control-flow-graph)
• 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 comporte ses avantages et ses inconvénients, et trouve son utilité dans des situations spécifiques :

* si tous les chemins sont analysés sans coupure

Slither analyse les contrats en quelques secondes, cependant, une analyse statique peut conduire à de fausses alertes et sera moins appropriée pour des vérifications complexes (ex. vérifications arithmétiques). Exécutez Slither via l'API pour accéder aux détecteurs intégrés ou via l'API pour des vérifications définies par l'utilisateur.

Echidna a besoin de travailler pendant plusieurs minutes et ne produira que de vrais positifs. Echidna vérifie les propriétés de sécurité fournies par les utilisateurs et écrites en Solidity. Il peut rater des bogues dans la mesure où 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. Il lui faudra plus de temps pour fonctionner, mais peut approuver la validité d'une propriété et ne signalera pas de fausses alertes.

Flux de travail conseillé

Commencez avec les détecteurs intégrés de Slither pour vous assurer qu'aucun bogue mineur n'est présent ou ne sera introduit plus tard. Utilisez Slither pour vérifier les propriétés liées aux héritages, aux dépendances variables et aux problèmes structurels. Au fur et à mesure que le code base grossit, utilisez Echidna pour tester des propriétés plus complexes de la machine d'état. Revisitez Slither pour développer des contrôles personnalisés pour les protections non présentes dans Solidity comme la protection contre le remplacement d'une fonction. Enfin, utiliser Manticore pour effectuer des vérifications ciblées de propriétés critiques de sécurité, par exemple des opérations arithmétiques.

• Utilisez le CLI de Slither pour relever les problèmes courants
• Utilisez Echidna pour tester les propriétés de sécurité de haut niveau dans votre contrat
• Utilisez Slither pour écrire des vérifications statiques personnalisées
• Utilisez Manticore pour vous assurer de façon approfondie des propriétés critiques de sécurité

Note sur les tests unitaires. Les tests unitaires sont nécessaires pour construire des logiciels de haute qualité. Cependant, ces techniques ne sont pas les mieux adaptées pour trouver des failles de sécurité. Ils sont généralement utilisés pour tester les comportements positifs du code (c.-à-d. que le code fonctionne comme prévu dans un contexte normal), tandis que les défauts de sécurité tendent à résider dans des cas particuliers que les développeurs ne considéraient pas. Dans notre étude de dizaines d'examens sur la sécurité des 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és dans le code de notre client.

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. Comme vos ressources consacrées à la sécurité sont limitées, il est important d’optimiser vos efforts pour déterminer la portée des parties faibles ou de grande valeur de votre code base. La modélisation des menaces peut vous aider. Envisagez la révision :

• Évaluation Rapide des Risques(opens in a new tab) (notre approche préférée lorsque le temps se fait court)
• Guide de modélisation des menaces du système centralisé de données(opens in a new tab) (aka NIST 800-154)
• Modélisation des fils de discussion Shostack(opens in a new tab)
• STRIDE(opens in a new tab) / DREAD(opens in a new tab)
• PASTA(opens in a new tab)
• Utilisation des affirmations(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 comprennent :

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

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

• Contrôle d'accès. Si votre système a des utilisateurs dotés de privilèges (par exemple, un propriétaire, des contrôleurs, ...) 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 avec des privilèges supérieurs.

  • Slither, Echidna et Manticore peuvent vérifier les contrôles d’accès corrects. Par exemple, Slither peut vérifier que seules les fonctions de la liste blanche ne disposent pas du modificateur onlyOwner. Echidna et Manticore sont utiles pour un contrôle d’accès plus complexe, comme une autorisation donnée uniquement si le contrat atteint un état donné.

• Opérations arithmétiques. Vérifier la solidité des opérations arithmétiques est absolument essentiel. L’utilisation de SafeMath partout est une bonne étape pour éviter les dépassements supérieurs et inférieurs, cependant, vous devez toujours prendre en compte d’autres défauts arithmétiques, y compris les problèmes d’arrondi et les défauts qui piègent 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.

• Exactitude de l'héritage. Les contrats de solidity reposent fortement sur l’héritage multiple. Des erreurs telles qu’une fonction d’ombrage manquant d’un appel super et un ordre de linéarisation c3 mal interprété peuvent facilement être introduites.

  • Slither est l’outil pour assurer la détection de ces problèmes.

• Interactions externes. Les contrats interagissent les uns avec les autres, et certains contrats externes ne doivent pas être approuvés. Par exemple, si votre contrat repose sur des 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 talonner les contrats externes.

• Conformité standard. Les normes Ethereum (par exemple ERC20) ont un historique de défauts dans leur conception. Soyez conscient des limites de la norme sur laquelle vous vous appuyez.

  • Slither, Echidna et Manticore vous aideront à détecter les écarts par rapport à une norme donnée.

Fiche mémo de sélection d’outils

D’autres domaines devront être vérifiés en fonction de vos objectifs, mais ces domaines généraux représentent 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. Envisagez de lire les sections Test et vérification automatisées des rapports suivants pour examiner les propriétés de sécurité dans le réel :

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