Logo du pré-GDR Sécurité Informatique
Groupe de travail : Méthodes formelles pour la sécurité

Responsables : Sébastien bardin, Stéphanie Delaune

Lien vers la page du GT : http://gtmfsec.irisa.fr/

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


Liste de diffusion : Vous pouvez vous abonner à la liste du GT "Méthodes formelles pour la sécurité" en envoyant un message à :

sympa_inria@inria.fr

avec l'un des titres suivants :

subscribe gt-mfs.permanents@irisa.fr

subscribe gt-mfs.doctorants@irisa.fr

subscribe gt-mfs.industriels@irisa.fr

subscribe gt-mfs.autres@irisa.fr

Notez que permanents correspond aux membres permanents d'un laboratoire académique, et que doctorants correspond aux doctorants, postdoctorants, étudiants ou tout autre personne susceptible d'être intéressée par un stage, un emploi, des offres de bourses, etc.

Contenu thématique :

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 d'application, potentiellement couverts par d'autres GT, 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.

Revues représentatives des activités du GT :
  • Journal of Computer Security
  • ACM Transactions on Privacy and Security (TOPS)
  • Foundations and Trends (FnT) in Security and Privacy

Les activités du GT peuvent également trouver leur place dans des revues plus orientées méthodes formelles : LMCS, TCS, TOCL,...

Conférences représentatives des activités du GT :
  • IEEE Computer Security Foundations Symposium (CSF)
  • International Conference on Principles of Security and Trust (POST)
  • IEEE Symposium on Security and Privacy (S&P)
  • IEEE European Symposium on Security and Privacy (EuroS&P)
  • European Symposium on Research in Computer Security (ESORICS)
  • ACM Conference on Computer and Communications Security (CCS)

Les activités du GT peuvent également trouver leur place dans des conférences plus orientées méthodes formelles : TACAS, CAV, POPL,...

Interfaces avec d'autres GDR :
  • GDR IM pour la vérification formelle
  • GDR GPL pour la compilation (GT compilation), les approches langages (LTP) et le test formel (MTV2)
Nombre évalué de personnes concernées par les activités du GT : 50 personnes