Méthodes formelles d'analyse quantitative de la sécurité de l'information partiellement observable dans les systèmes ouverts

点击翻译按钮获取中文摘要

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 de l'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 le flux d'information probabiliste et prévenir ainsi les attaques basées sur l'analyse statistique capable 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écessaires mises en oeuvre par l'environnement pour réussir son attaque. Un tel modèle poserait les jalons d'un modèle formel d'analyse de risque sécuritaire. Ce programme vise donc à: Développer un contexte théorique général pour exprimer les propriétés de flux d'information quantitatives qui étende celui de l'opacité dans les systèmes de transitions au cas où le flux d'information considéré est probabiliste et pondéré; Développer des algorithmes de vérification de ces propriétés; et étudier le problème de compositionalité des systèmes ouverts, relativement aux opérateur de séquentialité et de concurrence, qui préserve la mesure de sécurité de ces systèmes i.e. celui de décider quand une composante du système peut être substituée à une autre de manière sécuritaire. Le contexte méthodologique est celui des systèmes de transitions probabilistes et pondérés pour la modélisation et celui des séries formelles pour la spécification des propriétés de flux d'information quantifiés. Les méthodes de la vérification sont celles du calcul de mesures dans les Processus de Décisions Markoviens pondérés (PDMP) et de diverses notions de simulation entre PDMP qui préservent les mesures de sécurité définies.