Modélisation et détection formelles de vulnérabilités logicielles par le test passif

National audience; L'utilisation de modélisations formelles est devenue une partie intégrante du processus de développement de logiciels sûrs. En effet, une bonne modélisation du système à développer permet d'améliorer la qualité des logiciels en détectant, par exemple, certaines vulnérabilités avant même leurs déploiements. Dans cette optique, ce papier propose une nouvelle méthode de modélisation de vulnérabilités ainsi qu'un langage formel pour l'expression précise sans ambiguïté des causes et événements pouvant les produire. La définition d'un tel langage formel permet également la détection automatique des vulnérabilités par des outils de test. Plus précisément, nous illustrons l'utilisation de l'outil de test passif TestInv, développé au sein de notre équipe, pour la détection automatique de vulnérabilités exprimées dans le langage formel ainsi défini. Notre approche a l'avantage de produire un nombre beaucoup plus réduit de faux positifs tout en maintenant à jour la base de connaissances de l'outil TestInv. L'approche proposée est illustrée à travers l'exemple de vulnérabilité CVE-2005-3192 représentant un ``buffer overflow" dans un programme C