Blockchain3 jours
Tests avancés : fuzzing, invariants et vérification formelle
Developpeurs Solidity experimentes, auditeurs souhaitant maitriser les techniques avancees de testing et verification formelle
21h de formationdistanciel
Objectifs pedagogiques
- Maitriser le fuzzing (property-based testing) avec Foundry et Echidna
- Definir et tester des invariants systeme
- Utiliser la verification formelle avec SMT solvers
- Implementer des strategies de testing avancees
- Atteindre une couverture de code maximale
- Integrer fuzzing et verification dans CI/CD
Programme
- •Introduction au fuzzing : property-based testing vs unit tests
- •Foundry fuzz tests : invariant_*, fuzz parameters
- •Strategies de fuzzing : random, weighted, dictionary
- •Handler-based fuzzing : actions sequences, state transitions
- •Bounded vs unbounded fuzzing : runs, depth, seed
- •Shrinking : reduction des inputs en cas de failure
- •Coverage-guided fuzzing : maximiser la couverture
- •Atelier : ecrire des fuzz tests pour un contrat ERC-20
- •Invariants : definition, proprietes mathematiques, system-wide checks
- •Invariant testing avec Foundry : invariant_* functions
- •Echidna : fuzzer specialise smart contracts
- •Configuration Echidna : echidna.yaml, corpus, coverage
- •Property testing : assert-based vs boolean properties
- •Stateful fuzzing : sequences d'actions, oracles
- •Differential testing : comparer implementations
- •Atelier : definir et tester des invariants pour un AMM
- •Introduction a la verification formelle : theoremes, preuves
- •SMT solvers : Z3, CVC4, application aux smart contracts
- •Certora Prover : CVL (Certora Verification Language)
- •Specifications formelles : preconditions, postconditions, invariants
- •Runtime verification : K Framework, KEVM
- •Limitations de la verification formelle : scalability, expressiveness
- •Integration dans workflow : CI/CD, pre-deployment checks
- •Atelier : verifier formellement les proprietes d'un contrat avec Certora
Prerequis
- •Solidity avance
- •Experience significative en tests unitaires
- •Connaissance de Foundry ou Hardhat
Modalites d'evaluation
Projet de fuzzing complet avec invariants, verification formelle d'un protocole, rapport de couverture
Feuilles d'emargement, suivi de connexion pour le distanciel, evaluation des acquis en fin de formation.
Accessibilite handicap
Formation accessible aux personnes en situation de handicap. Referent handicap disponible pour adapter les modalites.