Vérification formelle de systèmes de sécurité au moyen de réseaux de Petri temporisés de haut niveau

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

Les organisations qui utilisent Internet sont quotidiennement victimes d'incidents liés à la sécurité (l'infection des ordinateurs par un virus, une panne causant l'arrêt des systèmes d'information, la perte de données et l'usurpation d'identité). Ces incidents pourraient avoir des répercussions néfastes pour ces organisations et leurs clients (pertes de clients, faillite,etc...). Il est alors vital que les systèmes utilisés soient dotés de mécanismes efficaces qui garantissent la sécurité et la protection des données confidentielles qu'ils gèrent. Les méthodes formelles de vérification, parce qu'elles s'appuient sur une base mathématique rigoureuse, sont  fortement recommandées lorsque les requis de sûreté et de sécurité d'un système sont primordiales (système de sécurité). C'est dans ce contexte que ce programme de recherche propose d'utiliser les méthodes formelles pour étudier et vérifier les systèmes de sécurité.  Ce programme comporte quatre objectifs spécifiques : 1. Étude et proposition d'un modèle de sécurité permettant de décrire efficacement les diverses politiques de sécurité qui peuvent cohabiter, à différents niveaux, au sein d'une même application répartie. 2. Élaboration d'un modèle à base de réseau de Petri de haut niveau temporisés pour le modèle de sécurité proposé. 3. Conception de méthodes de vérification par model-checking plus appropriées pour le modèle formel élaboré. Pour appliquer la technique de model-checking au modèle proposé, il faut d'abord établir une procédure convergente de transformation du modèle, qui est en général infini, en un système de transitions fini permettant de vérifier les requis. Cependant, le critère de convergence n'est pas suffisant car cette technique se heurte aussi au problème d'explosion combinatoire. Un intérêt particulier sera accordé à ce problème. 4. Implémentation, test et validation des approches de vérification proposées au cours de ce programme de recherche.