Les méthodes formelles ont pour but de permettre une analyse mathématique rigoureuse d’un système en vue de son analyse. Elles sont particulièrement cruciales dans le contexte des systèmes critiques d’un point de vue sécurité (dans la suite : « systèmes de sécurité ») pour lesquels une analyse de tous les comportements est nécessaire — incluant une compréhension précise de l’attaquant et des propriétés voulues. En effet, afin de déceler les attaques pouvant être lancées par des agents malveillants, ou réaliser une analyse de risques, il est important d’être exhaustif et de ne rien oublier. D’autre part, de nombreuses vulnérabilités dans les systèmes de sécurité proviennent d’une mauvaise interprétation de la description du système lors de sa mise en oeuvre. En proposant des descriptions claires et précises des systèmes, les méthodes formelles jouent un rôle important.

Les méthodes formelles pour la sécurité recouvrent naturellement de nombreux domaines applications, potentiellement couverts par d’autres GTs, comme les protocoles de sécurité, la mise en oeuvre de politique de contrôle d’accès, la détection d’intrusion ou encore la sécurisation de code source ou binaire. L’originalité de ce GT est l’utilisation et l’adaptation systématique des méthodes formelles aux problèmes de sécurité. Ainsi les travaux menés au sein du GT auront en commun l’objectif de s’appliquer à des systèmes de sécurité, de suivre une approche sémantique (système, propriétés à assurer, modèle de l’attaquant) et de s’attacher à identifier les garanties apportées. Par ailleurs, les analyses peuvent être réalisées à différents niveaux (protocole, modèle, algorithme, code source ou code machine), et les techniques utilisées pour réaliser ces analyses pourront être variées: systèmes de réécriture, algèbres de calcul, types, systèmes de contraintes, automates, interprétation abstraite, vérification déductive, model checking, …
Il pourra s’agir de la mise au point d’abstraction pour permettre de raisonner sur ces systèmes, ou de la mise au point de techniques automatiques ou interactives pour permettre leur analyse.

Mots clefs:

•  systèmes: protocoles de sécurité, code (source, binaire, script), librairies cryptographiques, bases de données, applications web, etc.
•  propriétés: intégrité, confidentialité, contrôle d’accès, authentification, privacy, flux d’information, intégrité du flot de contrôle, obscurcissement et anti-altération du code, etc.
• types d’approches: sécurité à la construction, analyse à posteriori, durcissement, analyse de risque, détection d’intrusion
• méthodes: spécifications, langages et types, compilation, analyse de code (source, binaire, script)
•  modèles d’attaquants
• spécification des classes de vulnérabilités
• raisonnements qualitatifs et quantitatifs