Aller au contenu
Financial Context Wiki

Comment lire un audit de smart contract

Un audit de smart contract est une revue délimitée de code, builds, déploiements, hypothèses et propriétés spécifiés ; ses constats et correctifs doivent être rapprochés du système en production.

Mis à jour

À des fins éducatives uniquement ; ne constitue ni un conseil en investissement ni une recommandation d’investissement. Les investissements peuvent entraîner des pertes.

Réponse directe

Un audit examine pendant une période déclarée des exigences, du code source, des entrées de build, une logique de déploiement et des hypothèses de sécurité spécifiés. Des méthodes complémentaires détectent les défauts, démontrent les chemins d’exploitation, évaluent l’impact et contrôlent les correctifs. La conclusion ne vaut que pour l’instantané et les preuves du rapport.

L’instantané fixe dépôt, commit ou empreinte d’arbre, sous-modules, dépendances, compilateur, paramètres, code généré, scripts, réseaux, adresses, proxy, implémentation ou beacon, données du constructeur ou de l’initialiseur, bibliothèques, administrateurs, timelocks et bloc ou heure. Les exclusions comptent : frontend, keeper, oracle, bridge, gouvernance ou signataire hors chaîne peuvent dominer le risque sans être audités.

Il faut modèle de menace et spécification : actifs, acteurs, rôles privilégiés, frontières de confiance, capacités, ordre et réorganisations, dépendances, transitions et propriétés mesurables de sûreté et de disponibilité. Un invariant sans unités, préconditions, quantificateurs ni exceptions peut parfaitement vérifier le mauvais comportement.

Tenez quatre registres : identité du périmètre, du build et du déploiement ; exigences, menaces et invariants ; constats, preuves et retest ; risque résiduel, acceptation et divulgation. Aucun critical ne certifie la sécurité, resolved ne signifie pas déployé et une preuve couvre seulement sa propriété, son modèle et ses hypothèses.

Fonctionnement

La revue manuelle suit architecture, flux de fonds, état entre fonctions et intention économique. L’analyse statique trouve motifs et flux, mais produit faux positifs et négatifs. Tests unitaires, d’intégration, sur fork et différentiels comparent des cas concrets. Fuzzing avec état et invariants dépendent des handlers, sélecteurs, seeds, corpus, exécutions, profondeur et environnement modélisé.

Exécution symbolique et vérification formelle démontrent certaines assertions sous les sémantiques et hypothèses prises en charge. unknown, timeout ou comportement non pris en charge ne sont pas des preuves. Une propriété démontrée peut omettre économie de l’oracle, gouvernance, configuration ou exigence réellement voulue. La revue humaine assume spécification et interprétation ; une observation d’IA n’est pas une méthode d’assurance indépendante.

Chaque constat identifie artefact et déploiement, prérequis, preuve minimale, chemin, accessibilité, privilèges, capital, répétabilité, impact, méthode de gravité et recommandation. Exploitabilité ou probabilité et impact sont distincts. Maximum théorique, nom de faille ou label d’outil n’établissent aucune perte exécutable.

open, acknowledged, risk accepted, partially fixed, resolved et retested ne sont pas des normes universelles. Une clôture défendable lie le problème au commit exact et consigne chemins modifiés et voisins, qui a retesté quoi et quand. Un risque accepté reste un risque ; un retest limité n’étend pas le périmètre.

Les déploiements actualisables exigent le rapprochement des slots du proxy, de l’implémentation ou du beacon et de l’administrateur ; initialiseur/réinitialiseur, verrouillage de l’implémentation, compatibilité du stockage, autorisation, timelock ou contournement, migration et retour arrière. Reproduisez les bytecodes de création et runtime, puis comparez bibliothèques, paramètres, rôles et état sur chaque réseau.

Le rapport final indique révision, auditeurs, dates, périmètre, méthodes, configurations, limites, constats, preuves, remédiation, risques et divulgation. Ensuite, surveillez empreintes, rôles, paramètres, dépendances et incidents. Toute modification substantielle crée un nouveau delta ; un ancien badge ne suit pas le code futur.

Processus :

  1. Geler le manifeste : dépôt, commit, dépendances, compilateur, paramètres, code généré et de déploiement, réseaux, adresses, pile proxy, paramètres, bloc, révision, inclusions et exclusions.
  2. Définir actifs, acteurs, rôles, frontières, capacités, cycle de vie, ordre, disponibilité, dépendances et invariants mesurables.
  3. Reproduire le build ; cartographier architecture, stockage, données, fonds et contrôle ; rapprocher source, artefacts, bibliothèques, bytecode, initialiseur, rôles et déploiement.
  4. Exécuter méthodes manuelles, statiques, unitaires, intégration, fork, différentielles, fuzz, invariants, symboliques ou formelles en consignant versions, configuration, seeds, corpus, couverture, timeouts et inconnues.
  5. Consigner artefact, prérequis, preuve, exploitabilité, impact, gravité, exposition, recommandation et preuves confidentielles sans confondre label d’outil et jugement.
  6. Geler le correctif et retester problème, chemins et invariants ; valider stockage, initialisation, migration, rollback, build et reçus avant d’attribuer un statut.
  7. Publier périmètre, méthodes, limites et risques ; rapprocher les artefacts de chaque réseau et maintenir surveillance, divulgation, réponse et bug bounty à jour.

Exemples

  • L’inflation d’un vault exige un registre complet. L’attaquant dépose 1 asset, reçoit 1 share, donne 1,000,000 assets ; totaux 1,000,001 assets et 1 share. La victime dépose 500,000 assets ; l’arrondi donne floor(500,000 * 1 / 1,000,001) = 0 shares. Si accepté, le vault détient 1,500,001 assets ; l’attaquant récupère 500,000 assets de plus que son apport de 1,000,001-asset. Un revert sur zéro share bloque ce chemin.
  • Couverture des fichiers n’est pas couverture du déploiement. Manifeste : 24 source units, 4 deployment scripts, 3 keeper services, soit 31 items. Inclus : 20 source units et 2 scripts, donc 22 / 31 = 70.96774194%; exclus : 9 items. Si le proxy utilise une unité exclue, couverture live 0% malgré 70.96774194%.
  • Le fuzzing ne prouve pas l’absence. Exécution : 2,000 sequences * 64 calls = 128,000 calls ; échec dans 3 sequences, soit 3 / 2,000 = 0.15%. Après correctif : 10,000 sequences * 64 calls = 640,000 calls, zéro échec. Sous hypothèses pédagogiques, borne supérieure approximative à 95% : 3 / 10,000 = 0.03% par séquence, pas une preuve.
  • Clôture et identité sont indépendantes. 12 findings : 2 critical, 3 high, 4 medium, 3 low. Fermés : 2 + 2 + 3 + 2 = 9, donc 9 / 12 = 75%; restent high, medium et low. Audité H1, live H2 : vérification en échec. H1 exact plus slot, initialiseur et rôles ne prouve l’identité qu’au bloc contrôlé.

Risques

  • Dépôt, commit, sous-module ou source générée sont ambigus.
  • Compilateur, optimiseur, bibliothèques ou dépendances ne sont pas figés.
  • Scripts, constructeur, initialiseur ou salt CREATE2 sont exclus.
  • Mauvais réseau, adresse, proxy, beacon ou implémentation sont examinés.
  • Source, artefact et bytecode ne se rapprochent pas.
  • Le modèle omet acteur, privilège, actif ou frontière.
  • Spécification ou invariant a unités, préconditions ou exceptions erronées.
  • Chemins admin, guardian, timelock, pause, upgrade ou migration sont omis.
  • Hypothèses d’oracle, jeton, bridge, keeper, gouvernance ou réseau échouent.
  • L’analyse statique produit un faux positif non trié.
  • Revue, test ou fuzzing omettent un chemin.
  • Harness, sélecteur, seed, corpus, profondeur ou modèle sont biaisés.
  • Timeout, sémantique non prise en charge ou unknown sont pris pour preuve.
  • Une preuve correcte formalise une exigence ou un système incomplet.
  • La gravité suit le nom au lieu de l’exploitabilité et de l’impact.
  • Valeur théorique est confondue avec perte atteignable ou bénéfice.
  • Le correctif introduit une régression ou brise un invariant économique.
  • Stockage, initialiseur, upgrade ou migration corrompent l’état.
  • Un problème accepté, ouvert ou partiel est masqué par le badge.
  • Le rapport est traité comme assurance, certification ou couverture permanente.

Idées reçues

  • « Sans critical, le contrat est sûr. » Cela décrit seulement les constats dans un périmètre, temps et méthodes limités.
  • « Forte couverture ou zéro échec fuzz prouvent l’absence. » Ces mesures portent sur du code et des chemins sélectionnés.
  • « La vérification formelle prouve tout le protocole. » Elle prouve des propriétés du modèle sous hypothèses.
  • « Resolved signifie tous les déploiements corrigés. » Il faut retest et rapprochement du build, bytecode, proxy, paramètres et rôles.
  • « Un auditeur réputé garantit indemnisation ou upgrades. » La responsabilité dépend du contrat ; les changements futurs sont hors instantané.

Sujets connexes

Sources

Navigation

Rechercher dans le wiki...