Nom du Projet : POLITESS

Intitulé du Projet : POLItiques de sécurité pour des systèmes d’information en réseau : modélisation, déploiement, TESt et Surveillance

Type de projet : Exploratoire

Durée : 30 mois

Priorité thématique : Sécurité

Nous proposons tout d’abord de définir une méthodologie descendante qui, partant de l’expression d’une politique de sécurité globale d’une organisation, permet de raffiner cette politique jusqu’à atteindre les règles de configuration des différents composants de sécurité mettant en œuvre cette politique. Cette méthodologie doit assurer par construction la validité, la complétude et la cohérence de l’ensemble des règles de configuration. Cette démarche descendante est bien adaptée à la conception d’infrastructure sécurisée de systèmes d’information centralisés pour lesquels il s’agit de définir des règles de configuration des différents composants de sécurité de cette infrastructure. Cette méthodologie doit permettre de déployer une politique de sécurité globale de manière à engendrer, pour chaque composant, un ensemble de règles de configuration à la fois :

   valide dans le sens où toutes les règles sont nécessaires à la mise en œuvre de la politique de sécurité globale,

   complet dans le sens où la réunion des règles doit permettre de réaliser les activités autorisées dans la politique de sécurité globale,

   et globalement cohérent.

Dans le cas d’une infrastructure de sécurité existante, la méthodologie définie dans POLITESS est complétée par une démarche ascendante destinée à confirmer la mise en œuvre correcte de la politique de sécurité dans cette infrastructure. Plus précisément, cette approche visera à évaluer l’ensemble des règles utilisées pour configurer les différents composants de sécurité de cette infrastructure. Cette démarche, basée sur des techniques de test, doit permettre d’analyser la compatibilité des politiques de sécurité mises en œuvre localement dans les différents composants de sécurité. Elle doit aussi permettre de détecter d’éventuelles erreurs de mise en œuvre d’une politique de sécurité dans une infrastructure de sécurité existante et de détecter la présence d’agents malveillants actifs qui exploiteraient ces erreurs. Enfin, les travaux entrepris dans POLITESS seront étendus à des environnements décentralisés ; l’objectif étant alors d’assurer l’interopérabilité entre différentes infrastructures ayant chacune leur propre politique de sécurité. Dans ce cas, les interactions doivent respecter la politique de sécurité de chaque composant. Pour cela, il s’agira d’étudier les problèmes de négociations de politiques de sécurité. Ces aspects de maintien de la politique locale de sécurité lors d’interaction avec d’autres systèmes munis de leurs propres politiques de sécurité doivent également être validés. L’objectif ultime (au-delà des études du projet) est que les responsables de sécurité puissent disposer d’outils, permettant :

   de modéliser les flux d’informations, les éléments du réseau (protocoles utilisés, types de nœud et type de sécurité associée etc.), afin de pouvoir décrire plus formellement la politique de sécurité,

   de dériver automatiquement les configurations des éléments de sécurité sur les différents nœuds du système,

   d’automatiser des procédures de test des systèmes pour vérifier si la politique de sécurité effectivement mise en œuvre correspond bien à celle déclarée.

Nous détaillons ci-dessous les objectifs de ces sous-projets.

SP1 - Modélisation

Modélisation des politiques et des propriétés de sécurité ; définition de formalismes, pour guider le déploiement ou le test des mécanismes de sécurité sur les éléments du réseau.

SP2 - Déploiement

Définition d’outils pour le déploiement de politiques de sécurité dans un environnement complexe ; Définition d’outils pour la décomposition de politiques de sécurité en fonction de la topologie et des capacités des composants devant participer à l’implantation de la politique. Définition d’outils pour la négociation de politique de sécurité.

SP3 - Test

Définition d’une « théorie du test » pour le test de politiques de sécurité sur des systèmes d’information en réseau : conformité d’un système par rapport à une politique, testabilité d’une politique donnée. Génération d’une suite de tests à partir de descriptions formelles de la politique de sécurité et d’éléments du réseau.

SP4 - Techniques de surveillance (observation et réaction)

Définition de techniques et d’outils de surveillance afin de détecter différentes infractions (anomalies, dysfonctionnements, attaques) dans les implantations des politiques de sécurité proposés par le projet.

SP5 - Etudes de cas

Fournir des contextes applicatifs complets, identifier les besoins correspondants, et expérimenter les méthodes et techniques du projet.

France Télécom - R&D

France Télécom est un opérateur de télécommunications majeur en Europe, offrant une large gamme de services domestiques et professionnels. France Télécom - R&D est la division de France Télécom en charge de la recherche et de l’innovation pour le groupe. Le laboratoire NSS (Network and Services Security) de France Télécom - R&D regroupe une soixantaine d’ingénieurs permanents travaillant sur la sécurité des réseaux et des systèmes d’information, pour le compte du groupe et de ses filiales. Il travaille dans trois domaines de recherche en sécurité, la cryptologie, la sécurité opérationnelle des réseaux, et les techniques formelles pour la sécurité.

Dans le domaine des web services, France Télécom est particulièrement actif sur le projet Liberty, et déploie régulièrement ces technologies dans des environnements sécurisés. Nous avons donc une bonne connaissance des standards et des outils utilisés dans ce domaine.

Leirios Technologies

Leirios Technologies est une société de technologie innovante (labellisée JEI) créée en mai 2003 pour industrialiser et commercialiser des solutions de génération automatique de tests à partir de spécifications. L’offre est structurée autour d’une gamme de produits LEIRIOS Test Generator (LTG) prenant en entrée des modèles en UML (Diagrammes de classes, Objet et Etat-Transitions annotés en OCL) et en notation par machine abstraite B. LTG automatise la traçabilité des exigences vers les tests générés et produit des scripts permettant d’exécuter les tests générés dans les environnements d’exécution cibles. L’outil LTG prend en charge la génération et l’exécution automatique des tests pour la validation fonctionnelle de systèmes, sous-systèmes ou de composants. Le cœur de l’innovation est basé sur des technologies d’évaluation symbolique du modèle et sur la mise en œuvre de stratégies de génération de tests permettant d’optimiser le ratio nombre de tests / couverture du modèle.

Leirios Technologies compte à mi-2005 16 salariés dont 10 en R&D produit. L’outil LTG fait partie des offres industrielles les plus matures au niveau européen dans le domaine de la génération automatique de tests fonctionnels.

L’offre LEIRIOS s’adresse en particulier au marché du logiciel embarqué à fort besoin de validation. La technologie LTG est actuellement mise en œuvre chez différents acteurs industriels : Parkeon, Axalto, Giesecke&Devrient, Sagem, Renault, Agence Spatiale Européenne (ESA/ESTEC), France Télécom - R&D, IRSN, ERG Transport Systems ...

Silicomp-AQL

Silicomp-AQL est une « Société de Service en Ingénierie Informatique » forte de plus de 650 collaborateurs (dont une très large majorité d’ingénieurs), et est une entité de Groupe Silicomp, une société technologique spécialisée dans les réseaux haut débit, les applications temps réel et les produits industriels (Groupe Silicomp compte environ 1000 employés en France et à l’étranger). Silicomp-AQL se développe au sein de la technopole Rennes Atalante, qui regroupe industriels, centres de recherches et universités, spécialisés dans les domaines des télécommunications, des réseaux et du multimédia. Silicomp-AQL propose ses services dans le domaine des technologies de l’information, en s’appuyant essentiellement sur ses compétences dans quatre domaines : l’ingénierie logicielle technique, l’ingénierie des systèmes d’information, la gestion de projets et de la qualité, la sécurité des systèmes d’information.

Silicomp-AQL est certifiée ISO 9001 pour le développement logiciel depuis 1992 et est l’une des premières sociétés françaises à avoir obtenu l’agrément ISO 9001-2000. Silicomp-AQL est par ailleurs renommée pour son Centre d’Evaluation de la Sécurité des Systèmes d’Information (CESTI) qui s’appuie sur des compétences en sécurité des technologies de l’information : consulting (ISO17799), expertise (test, architecture), évaluation sur la base des Critères Communs. Le laboratoire de la sécurité de Silicomp-AQL est officiellement agréé par les autorités françaises.

Silicomp-AQL entretient depuis plusieurs années une activité sur le thème des méthodes formelles et semi-formelles et plus particulièrement de leur utilisation dans un cadre industriel. Silicomp-AQL a, entre autres projets, participé à la validation de la preuve formelle du modèle B du projet METEOR ainsi qu’à la validation technique des modèles B pour le compte de Matra-Transport International. Plus récemment, Silicomp-AQL a participé à un projet européen (SATURN) et est impliqué dans plusieurs projets liés à la modélisation de la sécurité et de la génération de test à partir de spécification formelle ou semi-formelle (RNRT VERBATIM, RNTL COTE et CASTLES). Dans le cadre du projet ITEA SATURN, l’approche adoptée a consisté à compléter et à élargir le travail qui a été mené en Europe sur la sécurité (projet ITEA TESI ou le projet Médéa+ Cryptosoc). Ce projet a été l’occasion pour Silicomp-AQL d’analyser les techniques existantes de modélisation de systèmes complexes et de leur sécurité. Sur la base de cette étude, un environnement de modélisation de système a été proposé. Cet environnement s’appuie entre autre sur des outils existants et sur leur adaptation au domaine de la sécurité (outil d’ingénierie des exigences et outils de méta modélisation).

A titre d’exemple de projet récent, le projet RNTL CASTLES (2003-2006) dont l’objet est la « Conception d’Analyses Statiques et de Tests pour le Logiciel Embarqué Sécurisé » vise à définir un environnement pour l’automatisation de la certification de plate-forme et des applications JavaCard et d’évaluer cet environnement dans le contexte de la certification industrielle selon les Critères Communs. Silicomp-AQL a aussi participé à plusieurs Programmes d’Etudes Amont pour le compte de la DGA :
  le PEA CASTOR (terminé) dont le sujet est la modélisation de la sécurité des systèmes d’information,
  le PEA « Alerte & Réaction » (2003-2006), est un Programme d’Etude Amont financé par le ministère de la Défense dont le but est de réaliser un état de l’art et de définir les outils de Veille/Alerte/Réponse permettant de faire face aux menaces cybernétiques pesant sur les réseaux, systèmes et applications de la Défense, ainsi que de réaliser une plate-forme

SAP Research

Fondée en 1972, SAP est le premier fournisseur mondial de solutions business collaboratives pour toutes les industries et pour tous les marchés majeurs. Basée à Walldorf, en Allemagne, SAP est le premier fournisseur mondial de logiciels inter-entreprises, et le troisième fournisseur mondial de logiciels. SAP emploie plus de 30000 personnes dans plus de 50 pays, dont environ 500 en France. Les activités de SAP en France sont distribuées entre Paris et Sophia Antipolis et incluent aussi bien des activités de Recherche, que de Développement, de Production, de Vente et de Support Client.

SAP Research est le département de recherche technologique de SAP.

Ayant pour but de supporter la stratégie de SAP sur le long terme et d’établir SAP comme le leader dans le domaine des technologies de l’information émergentes, SAP Research observe les tendances actuelles et à venir des TIC, détermine la valeur des nouvelles technologies pour SAP et en introduit de nouvelles ainsi que les concepts pour les futures solutions qui seront d’une importance stratégique pour SAP et ses clients. SAP Research a identifié des programmes de recherche pour le long-terme (incluant entre autres Smart Items, Security & Trust, et Business Process Modelling and Management). SAP Research agit, si nécessaire, en fonction de la tendance et des changements imminents dans les TIC ou du marché. Le programme Security and Trust est un des programmes de recherche pour le long terme. Une douzaine de chercheurs travaille à temps plein au sein de SAP Labs France à Sophia-Antipolis sur différents projets liés à la sécurité, dont certains sont financés par l’Union Européenne. L’équipe de recherche impliquée dans le projet POLITESS est située au sein de SAP Labs France, à Sophia-Antipolis. Les principaux domaines d’expertise de l’équipe font partie du domaine appelé Sécurité d’Application. Ils incluent la Gestion d’Accès, les Règles de Contrôle d’Accès, les Modèles Formels de Sécurité, le Contrôle d’Organisation, la Sécurité des Logiciels, et les Méthodes Formelles. L’équipe est actuellement engagée dans 3 projets européens FP6 liés à la sécurité :

  eJustice : Le but est de développer les éléments d’une sécurité globale et un framework pour la Justice. http://www.ejustice.eu.com/

  Trustcom : Le but est de développer un framework permettant des processus métier collaboratifs sécurisés dans des organisations virtuelles créées à la demande, autogérées, capables de grandir et hautement dynamiques. http://www.eu-trustcom.com/

  Mosquito : Le but est de permettre la sécurisation d’applications métier pour les travailleurs mobiles dans des environnements ubiquitaires. http://www.mosquito-online.org/

GET

ENSTB

Deux écoles du GET, l’ENST Bretagne et Télécom INT, participent à POLITESS. La recherche en SSI est conduite par l’équipe SERES (« Sécurité des Réseaux et des Applications Réparties »). Cette équipe est composée de 10 personnes (4 enseignants-chercheurs et 6 doctorants). Elle a une expérience de projets de recherches : PEA, RNTL, RNRT et actions incitatives ACI. Elle a développé des partenariats industriels, en particulier avec France Télécom - R&D, EADS, Silicomp-AQL, ExaProtect or Netasq. Ses actions de recherche s’inscrivent dans quatre domaines principaux de la sécurité informatique : (1) Modèles d’accès, d’usage et de contrôle de flots, (2) Conception de mécanismes de sécurité pour les réseaux et les systèmes d’information, (3) Détection d’intrusions et analyse de vulnérabilités, (4) Validation et vérification de la sécurité. L’équipe du GET/INT impliquée dans ce projet fait partie également du laboratoire CNRS SAMOVAR. Ses domaines de recherche portent sur la conception et spécification de protocoles de communication et de services, la conception et mise en œuvre des techniques de surveillance, la conception des méthodes et des architectures pour le test de conformité ainsi que le développement des plates-formes de validation (en particulier ils ont développé la plate-forme PLATONIS, dans le cadre d’un projet RNRT). Par ailleurs, l’équipe du GET/INT a participé et participe toujours à de nombreux projets nationaux, internationaux et européens. Parmi ceux qui sont arrivés à terme récemment nous pouvons nommer : les projets RNRT CASTOR, RNTL TELEM, européens ASK-IT et E_LANE. L’équipe est également impliquée dans des actions de collaboration au sein de ses tutelles : projet RAS (Routage Ad hoc Sécurisé) du GET et responsabilité de l’AS « Techniques de spécification et de test pour les composants logiciels de communication » du CNRS.

Enfin, le réseau Marie-Curie RTN TAROT, dont l’équipe GET/INT est le leader, regroupe les acteurs européens majeurs du domaine du test, et vise à regrouper, améliorer et diffuser les techniques de test de partenaires académiques.

INPG/IMAG

L’Institut National Polytechnique de Grenoble est une université constituée du regroupement de 9 écoles d’ingénieurs grenobloises (et de l’ESISAR à Valence). Les laboratoires de la fédération IMAG sont associés à l’INPG, ainsi qu’à l’Université Joseph Fourier et au CNRS. Au sein du projet POLITESS, ce sont deux équipes associées dans le projet IMAG MODESTE (MODElisation pour la SécuriTE) qui contribueront : l’équipe Vasco (Validation, Spécification et Construction de logiciels) du LSR et l’équipe DCS (Systèmes Distribués et Complexes) de Vérimag. L’équipe Vasco a développé des méthodes et des outils de production de tests à partir de spécifications formelles, en particulier Lutess autour du formalisme Lustre pour le test de systèmes synchrones (appliqué aussi bien à des systèmes de contrôle-commandes, qu’à l’analyse des interactions de services téléphoniques - projet RNRT Valiserv), et Tobias, pour produire des tests à partir de programmes Java et de spécifications B (utilisé en particulier pour le test de cartes à puces). Dans le domaine des politiques de sécurité, Meca (modèles de contrôles d’accès) est un outil en cours de développement et permet de modéliser en B différentes formes de contrôles d’accès (discrétionnaire, obligatoire, RBAC). A terme il devrait permettre de produire de manière systématique les vérifications statiques liées à une application ou son monitoring à l’exécution. L’équipe développe aussi une large compétence sur la modélisation et la vérification de propriétés de sécurité, en vue de certifications haut niveau ou de génération de tests de conformité à une politique de sécurité (ACI Potestat et Geccoo et projet grenoblois MODESTE). Au cours des dernières années, l’équipe Vasco a participé à plusieurs projets RNTL ou RNRT dans le domaine du test ou du développement formel (BOM, COTE, INKA, VALISERV, DANOCOPS, VERBATIM), à trois projets de l’ACI Sécurité Informatique (Potestat, Edemoi, Geccoo) ainsi qu’à deux Actions Spécifiques du CNRS portant sur le test à partir de spécifications et sur la testabilité. L’équipe participe également au réseau européen TAROT (Training And Research On Testing) dans le cadre du programme Marie Curie Research Training Network (MCRTN).

Vérimag a des compétences reconnues dans la définition de langages de spécification, dans la vérification, la validation et le test basés sur des méthodes formelles et dans la modélisation des systèmes temps-réel et hybrides. Les outils produits par VERIMAG sont régulièrement transférés vers l’industrie. Le laboratoire est coordinateur du réseau d’excellence européen ARTIST et du réseau national ARTIST SECC du CNRS.

L’équipe DCS « Systèmes Distribués et Complexes » de Vérimag, vise le développement de formalismes, de méthodes et d’outils pour la conception et la validation de systèmes distribués et complexes (applications temps-réel, protocoles de sécurité, ainsi que les applications distribuées en général). L’équipe a contribué activement au développement de méthodes de test, basées sur les modèles. En particulier, l’équipe a développé la plate-forme IF, à laquelle sont connectés le générateur de tests TGV (développé en collaboration avec l’IRISA), l’outil d’exécution de tests Spider (développé par IBM Haifa) ainsi qu’une chaîne d’outils pour le test de propriétés et le test de robustesse.

Au sein du projet MODESTE et de l’ACI POTESTAT, les équipes DCS et Vasco ont élaboré des modèles pour analyser la conformité de systèmes à des politiques de sécurité.

IRISA

Deux équipes de l’Irisa participent au projet POLITESS : l’équipe Vertecs et l’équipe Distribcom.

L’équipe Vertecs conçoit des techniques et des outils de génération automatique de tests de conformité pour des systèmes réactifs non-déterministes, fondées sur des modèles formels et des techniques de vérification. D’une part elle a développé des techniques de génération de tests à la volée, basées sur une exploration paresseuse de graphes d’états guidée par des objectifs de test [JJ04]. Ces techniques ont été implémentées dans l’outil TGV en collaboration avec Vérimag. Depuis 5 ans, l’équipe Vertecs s’intéresse à la génération symbolique de tests de conformité pour des modèles de spécifications de type automates étendus, en évitant l’énumération des données a priori non bornées [RdBJ00], [JJRZ05]. La génération de tests symbolique consiste alors à générer un programme de test en utilisant des transformations syntaxiques du modèle de spécification, s’appuyant sur une analyse sémantique approchée par interprétation abstraite permettant d’affiner la sélection des tests. L’exécution des tests se base ensuite en partie sur des techniques de résolution de contraintes. Ces techniques sont implémentées dans l’outil STG qui utilise l’outil NBAC pour l’analyse par interprétation abstraite.

En dehors du test, l’équipe Vertecs possède une solide compétence dans diverses techniques de vérification (model-checking, interprétation abstraite, preuve de programmes), en synthèse de contrôleurs, en diagnostic et monitoring.

L’équipe Distribcom travaille depuis deux ans dans le domaine de la sécurité, et plus particulièrement autour des propriétés de confinement d’information et de non-interférence. Récemment, une nouvelle approche pour la détection de canaux cachés à l’aide de la théorie des jeux a été proposée [HZJ03], [HZD04],. Un stage de Master sur le sujet est également en cours. Outre la caractérisation logique de ces propriétés de sécurité, nous nous attachons à quantifier les flots d’information, à l’aide d’outils tels que l’algèbre (max, +) [H04] et la théorie de l’information. Par ailleurs, l’équipe Distribcom étudie des techniques de monitoring dans des réseaux, qui pourraient être utilisées pour la détection d’attaques distribuées.