MULLINS John

Research activity

L’analyse formelle de la sécurité des systèmes ouverts conçus pour protéger l’information est devenu un champ de recherche très actif. Il recouvre aussi bien le développement d’une théorie de la sécurité de l’information que ces systèmes doivent assurer que celui de méthodes aptes à assurer leur correction. L’approche de la théorie du flux d’information est une approche booléenne au sens où le comportement d’un système est soit bon, soit mauvais relativement à la sécurité requise. Toutefois, cette approche est trop grossière pour décrire les aspects probabilistes du flux d’information et prévenir ainsi les attaques basées sur l’analyse statistique, capables d’inférer un secret à partir de ses observations, ou encore pour analyser le coût computationnel du flux d’information et prévenir ainsi les attaques contre la disponibilité des ressources. Ces toutes dernières années, un champ de recherche sur les modèles probabilistes de flux d’information a émergé. Mais aucun modèle n’a encore été proposé pour quantifier aussi les ressources néces- saires mises en oeuvre par l’environnement pour réussir une attaque. Un tel modèle poserait les jalons d’un modèle formel d’analyse de risque sécuritaire. Ce projet de recherche vise donc à développer un modèle général pour exprimer ce type de mesures de flux d’information qui étende le modèle probabiliste défini conjointement par des chercheurs de l’École Polytechnique de Montréal (EPM) et de l’Université Pierre & Marie Curie (UPMC) et à étudier le problème de compositionalité de ces mesures, relativement aux opérateurs de séquentialité. Le contexte méthodologique naturel est celui des Processus de Décisions Markoviens Pondérés (PDMP) pour la modélisation et des séries formelles pour la spécification des mesures de flux d’information.