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.
1. Introduction
Dans cet article, nous montrons comment les outils actuels de spécification et de vérification formelles révèlent très tôt des vulnérabilités qui seraient difficiles à corriger au moment de l’implémentation. Avec un outil d’animation, il est possible de « jouer » avec la spécification du protocole pour varier les scénarios d’exécution, et même tenter des exécutions a priori idiotes. Ce faisant, on retrouve une démarche de type essai/erreur proche du fuzzing, mais appliquée au modèle du protocole plutôt qu’à son implémentation : du fuzzing de spécification.
Tout d’abord, quels avantages peut-on attendre de la vérification automatique ?
1.1 Retrouver des vulnérabilités connues
Cela peut sembler inutile a priori : si des vulnérabilités sont connues, pourquoi se donner la peine de les retrouver automatiquement ? Nous voyons pourtant deux bonnes raisons de le faire : augmenter la…
- Accédez à tous les contenus de Connect en illimité
- Découvrez des listes de lecture et des contenus Premium
- Consultez les nouveaux articles en avant-première