Auditorium (IMAG)
7 novembre 2016 - 14h00
Sécurité de Flux d'Information dans les Modèles à Base de Composant: De la Vérification à l'Implementation (Phd Defense)
par Najah BEN SAID de Verimag, Grenoble Alpes University
Résumé : Il est reconnu que garantir une sécurité de bout-en-bout pour les systèmes distribués est un problème très complexe. En effet, la communication bas niveau entre les différentes parties du programme demande l'implémentation d'un protocole de communication complexe pour garantir une sécurité “globale” à partir de la sécurité “locale” de chaque composant. Il est à noter que la décomposition du système en sous-système est très souvent liée à un objectif fonctionnel et est indépendante de l'objectif de sécurité à atteindre. Donc, les données sont très souvent manipulées par des sous systèmes dont les niveaux de sécurité sont différents. Par ailleurs, il est souvent rare de trouver des programmeurs qui ont un expertise suffisant sur les mécanismes de sécurité à utiliser pour implémenter de tels protocoles de coordination de composants.
Dans le cadre de cette thèse, nous avons opté pour le développement de procédures automatiques pour garantir des propriétés de non-inférence dès la conception jusqu'à l'implémentation d'un système distribué fiable. Pour ce faire, nous avons étendue la plateforme BIP pour la création et vérification de la sécurité de flux d'information des systèmes à base de composants. Une combinaison de deux notions de non-interférence (d'événements et de données), garantissant l'objectif de sécurité, sont définies et formellement prouvés à travers des unwinding relations fortement utilisées pour vérifier la non-interférence. Une méthode automatisé basé sur l'utilisation de conditions syntactiques, inspiré d’analyse statique, est utilisée pour valider qu’un modèle annoté par des labels de sécurité satisfait la propriété. Cette méthode est raffiné d'avantage avec l'utilisation d'un algorithme de synthèse (d'inférence) d'annotation de sécurité visant à simplifier et rendre plus pratique la procédure d'annotation du modèle.
La distribution du modèle peut introduire des difficultés de gestion de concurrence (conflits) entre composants et nécessite forcement une re-vérification des notions de sécurités, ce qui rend la tâche fastidieuse. Dans cette thèse nous introduisons une méthode de distribution qui permet de préserver la satisfaction des conditions syntactiques de sécurité une fois vérifiés dans le modèle centralisé. Cette méthode est dite sécurisé-par-construction.
Prof. SADDEK BENSALEM - Directeur de these
Prof. AXEL LEGAY - Rapporteur
Prof. GILLES BARTHE - Rapporteur
Prof. JEAN-LOUIS LANET - Examinateur
Prof. CATALIN DIMA - Examinateur
Prof MARIE-LAURE POTET - Examinateur
Dr. MARIUS BOZGA - Co-directeur
Dr. ABDELLATIF TAKOUA - Co-encadreur
