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) : LSRSujet proposé par : Marie-Laure Potet et Nicolas Stouls
Specialite(s): Intelligence Interaction Information, Systemes et LogicielsMots 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