BlockPulseNews
La vérification formelle est une méthode qui démontre mathématiquement qu'un programme, par exemple un smart contract, respecte certaines propriétés précisément définies, quelles que soient les entrées, là où les tests classiques n'examinent qu'un nombre limité de cas.
Thème : Sécurité et arnaques
La démarche commence par une spécification : on écrit, dans un langage logique, les propriétés que le code doit toujours respecter. Par exemple, la somme des soldes est égale à l'offre totale, ou personne ne peut retirer plus qu'il n'a déposé. Des outils spécialisés, comme des solveurs automatiques ou des assistants de preuve, analysent ensuite le code pour démontrer que ces propriétés tiennent dans toutes les situations possibles, ou produisent un contre-exemple.
Pour des contrats qui gèrent des fonds importants et ne peuvent pas être facilement corrigés, cette approche apporte un niveau de confiance supérieur aux tests et aux audits manuels. Elle reste cependant coûteuse et demande une expertise rare. Surtout, elle ne prouve que ce qui a été spécifié : si une propriété importante est oubliée ou mal formulée, une faille peut subsister malgré une vérification réussie.
Imaginons une équipe qui développe un contrat de stablecoin. Elle spécifie qu'aucune fonction ne peut créer de jetons sans dépôt de collatéral correspondant. L'outil de vérification découvre un enchaînement d'appels rare qui viole cette règle. L'équipe corrige le code, relance la preuve, et la propriété est démontrée.
Une vérification formelle ne couvre que les propriétés écrites et le code analysé : une spécification incomplète, une erreur dans l'outil ou des interactions avec des contrats externes non modélisés peuvent laisser passer des failles. Elle ne remplace pas un audit complet.
Non. Elle garantit que les propriétés spécifiées sont respectées, mais une faille peut exister en dehors de ces propriétés ou dans les interactions avec d'autres contrats.
Un audit est une revue experte, en partie manuelle, du code. La vérification formelle est une démonstration mathématique outillée. Les deux sont complémentaires.
Nos articles qui parlent de Vérification formelle, les plus pertinents d'abord.