Ent?te

Logo du LIFL

Depuis le 1er janvier 2015 le LIFL et le LAGIS forment le laboratoire CRIStAL

  1. News

Thesis of

Dorina Ghindici

Thursday 4 December 2008
Bâtiment des thèses - Université de Lille1

Analyse de flot d'information pour les systèmes embarqués : aspects pratiques et théoriques

Directeur de Thèse: Isabelle Simplot-Ryl, Professeur, Université de Lille I
Rapporteurs :
Yves Bertot, DR INRIA, INRIA de Nice Sophia-Antipolis
Nadia Tawbi, Professeur, Université Laval Canada Québec
Membres:
Bertil Folliot, Professeur, Université de Paris VI
David Pichardie, Maître de Conférences, INRIA de Rennes-Bretagne Atlantique
Gilles Grimaud, Maître de Conférences, Université de Lille I
Mireille Clerbout, Professeur, Université de Lille I

Nos travaux ont pour but de fournir une solution aux problèmes de confidentialité dans les systèmes multi-applicatifs: assurer la sécurité des applications dédiées aux systèmes portables et autonomes en vérifiant des propriétés de sécurité en termes de flot d'information au moment du chargement des applications, contrairement aux travaux existants qui ne sont ni modulaires ni dynamiques. Afin de fournir une solution complète, nous avons traité les aspects à la fois pratiques et théoriques du problème. Dans un premier temps, nous proposons un modèle et un outil adaptés aux contraintes inhérentes aux systèmes embarqués. Notre approche est modulaire et supporte l'héritage et la surcharge. La vérification est donc incrémentale et s'effectue sur le système cible, le seul endroit ou la sécurité peut être garantie. Il s'agit, à notre connaissance, du premier vérifieur embarqué pour l'analyse de flot d'information. Afin de prouver l'utilité pratique de notre modèle, nous avons mené des expérimentations et nous avons testé l'outil dans des contextes différents. Dans un deuxième temps, nous traitons les aspects théoriques: nous proposons un modèle formel basé sur des graphes de l'abstraction de la mémoire. Un graphe de l'abstraction de la mémoire est un graphe « points-to » prolongé par des noeuds de type primitif et par des liens issus de flots implicites. Notre construction est prouvée correcte par un théorème de non-interférence. De plus, les politiques de sécurité ne nécessitent pas d'être connues pendant l'analyse : le flot d'information est vérifié a posteriori en étiquetant le graphe de l'abstraction de la mémoire avec des niveaux de sécurité.

Ours

UMR 8022 - Laboratoire d'Informatique Fondamentale de Lille - Copyright © 2012 Sophie TISON - Crédits & Mentions légales

Page respectant XHTML et CSS.

Pour tout commentaire / Comments and remarks : webmaster