Fuzzing Logique de Protocoles Cryptographiques – ProtoFuzz

Notre société de l'information dépend des protocoles cryptographiques, ces programmes distribués utilisant des primitives cryptographiques pour établir divers objectifs de sécurité tels que la confidentialité ou l'intégrité. Toute faille dans ces protocoles a souvent des conséquences dramatiques, amplifiées par leur rôle central par exemple dans la finance, le commerce et la communication. Pourtant, les spécifications et les implémentations de ces protocoles ne cessent d'être cassées par des attaques logiques. Ces attaques, quand elles concernent les spécifications, peuvent être détectées et réparées par des méthodes formelles telles que la vérification symbolique. Cependant, ces méthodes ne fournissent aucune garantie sur les implémentations, qui sont les produits finaux qui doivent être sûrs. Le testing, en particulier le fuzzing, opère sur les implémentations et a démontré son efficacité pour trouver les failles de bas niveau, mais reste incapable de capturer les attaques logiques.

Pour combler cette lacune, nous développerons les fondements et la conception d'une approche hybride combinant la vérification symbolique et le fuzzing. Nous allons :
(a) concevoir un langage simplifié de protocole et un extracteur de modèle qui permettent d'extraire des modèles formels à partir d'implémentations légèrement annotées, puis de raffiner ces modèles sur la base de contre-exemples de correction fonctionnelle et
(b) développer une nouvelle méthodologie de test, le fuzzing guidé par des modèles symboliques, qui, assistée par des vérificateurs symboliques, capture efficacement les attaques logiques. Cette méthode s'appuiera sur une connexion entre modèles formels symboliques et implémentations qui leur permettront de s'animer mutuellement.

Les ambitions de ce projet sont de faire progresser les techniques de fuzzing, d'établir cette approche hybride en tant que nouveau sujet de recherche, ainsi que d'attaquer et d'améliorer les protocoles cryptographiques largement utilisés.