LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
La conception de systèmes de communications sûrs est un défi. Il est possible de monter de véritables attaques en exploitant uniquement les faiblesses des protocoles. Ces attaques échappent souvent aux concepteurs à cause de la difficulté à prévoir a priori les différentes manières possibles pour un environnement malicieux d?interférer avec les differents agents. Ceci montre l?importance de disposer d?outils puissants capable d?analyser le flot d?information distribué entre les différents agents communicants. Les algèbres de processus et les techniques de réécritures associées offrent des modèles bien adaptés pour de telles analyses. Par exemple, elles peuvent exploiter des critères d?observation adéquats pour vérifier la confidentialité ou l?authentification pour les protocoles cryptographiques ; mais elles conviennent également à d?autres applications telles que la répartition à grande échelle de politiques de contrôle d?accès dynamiques sur des OS sécurisés. D?intéressants résultats ont été obtenus récemment par ces approches, cependant leur application effective à des problèmes de type industriel nécessite de résoudre des questions fondamentales telles que : procédures de décision plus efficaces et approximations plus précises, prise en compte de l?incidence du temps, modélisation adéquate des primitives cryptographiques imparfaites, de la notion du déni de service et étude formelle des attaques associées.
Les équipes du projet SATIN disposent de compétences complémentaires en sécurité et méthodes formelles ; notre objectif est de relever le défi de l?analyse et de la conception de systèmes distribués sûrs. Nous nous appuierons sur des avancées récentes en modélisation formelle, résolution de contraintes, automates d?arbre et critères d?observation pour systémes concurrents. L?interaction avec nos partenaires industriels CEA-DAM et France Telecom sera naturellement importante pour valider les résultats obtenus à chaque étape du projet.
Pierre COURTIEU
Gaétan HAINS
Pierre RETY
Université d'Orléans | INSA Centre Val de Loire