Master Mathématiques Informatique, 2e année - voie recherche
Descriptif de Projets - Année 2005/2006

93 -   Architecture de sécurité Java : Modèles et vérifications du contrôle d\'accès



Laboratoire(s) : LSR

Sujet proposé par : Marie-Laure Potet et Nicolas Stouls

Specialite(s): Intelligence Interaction Information, Systemes et Logiciels

Mots clefs : méthodes formelles, politiques de contrôle, raffinement et preuve, sécurité des systèmes

Résumé :

Le sujet de recherche s'inscrit dans le cadre de la maîtrise de la sécurité des systèmes logiciels, domaine en pleine expansion. En effet la sécurité devient un aspect incontournable et nécessite d'être prise en compte dès les phases amont de la conception. L'architecture sécurisée de l'environnement Java repose sur différents mécanismes qui prennent en compte certaines propriétés soit de manière statique soit de manière dynamique. Ces mécanismes sont les chargeurs de classes, le vérificateur de byte-code et le security manager. A partir de Java 2.0 la sécurité est basée sur la description de politiques de sécurité, description qui permet au développeur de préciser les accès contrôlés et autorisés. Etablir les propriétés globales d'une telle architecture est un problème complexe car ceci nécessite de prendre en compte les différents mécanismes concernés, ainsi que les propriétés issues des vérifications statique et dynamique.

Description :
Le but du travail sera d'étudier précisément les politiques de contrôle d'accès admises et, à partir de cette étude, de proposer un modélisation formelle de ces politiques en vue de garantir le respect de ces politiques. La solution classique consiste à " monitorer " à l'exécution chaque accès ce qui ralentit les exécutions. Pour une application donnée le but sera de déterminer ce qui peut être garanti statiquement et ce qui demande effectivement une vérification à l'exécution. Finalement les exigences de sécurité sont généralement exprimées de manière plus abstraite qu'une politique de contrôle d'accès. Le but sera d'étudier le lien formel entre des propriétés de haut niveau et des politiques de sécurité. Ce travail poursuit un travail de Master sur la modélisation et la vérification de politiques de sécurité de type niveaux de sécurité. Il donnera lieu à un outil permettant de spécifier et vérifier les politiques de sécurité de Java. Ce sujet s'inscrit dans le cadre de différents projets dans lesquels l'équipe Vasco est impliquée : l'ACI sécurité GECCOO (Génération de Code Certifié Orienté Objet), l'ACI POTESTAT (POlitiques de sécurité : TEST et Analyse par le Test de systèmes en réseau ouvert) et le projet IMAG MODESTE (Modélisation pour la Sécurité : test et raffinement en vue d'un processus de certification). D'autre part des collaborations industrielles sur ce thème sont en cours de montage. Références : Access Control : Policies, Models, and Mechanisms P. Samarati and S. Capitani di Vemercati Foundations of Security Analysis and Design Inside Java 2 Platform security Architecture, API Design, and Implementation. Li Gong, Gary Ellison, Mary Dageforde. Addison Wesley Professional, 2nd Edition, may 2003
Résultats théoriques attendus
- Modèle formel des politiques de sécurité admises à partir de Java 2.0 et de la notion de conformité d'une application à ces politiques. - utilisation de la méthode B pour déterminer les vérifications nécessaires à l'exécution. - études de propriétés de haut niveau et de leur implémentation en terme de politiques de sécurité Java.

Résultats pratiques attendus
Un outil de spécification et de vérification de politiques de sécurité (développement Java)





en cas de problème, merci de bien vouloir contacter Contact sujets

retour à la page d'accueil