Votre protocole est-il vérifié ?
Comme l’indiquent plusieurs articles de ce dossier, des techniques de fuzzing peuvent être appliquées aux protocoles. Elles permettent alors de détecter des vulnérabilités sur des implémentations particulières. Mais qu’en est-il de la détection des erreurs de conception ? Comment s’assurer qu’un nouveau protocole est sain d’un point de vue purement logique avant même de disposer de son implémentation ? Les techniques récentes de vérification automatique de protocoles s’avèrent à cet égard très utiles. Plusieurs outils d’animation et de vérification existent : tout au long de cet article, nous utilisons conjointement SPAN (http://people.irisa.fr/Thomas.Genet/span/) et AVISPA (http://www.avispa-project.org/). D’une certaine manière, l’animation est à la spécification ce que le fuzzing est à l’implémentation.