SAMOVAR UMR 5157

  • Accueil
  • Accueil
  • Accueil
  • Accueil

CNRS

Rechercher




Accueil > Équipes > METHODES > Bilan scientifique 2008-2013 > Axes de recherche

Méthodes formelles pour le test et la vérification

  • Enseignants-chercheurs : Ana Rosa CAVALLI, John Paul GIBSON, Stéphane MAAG, Amel MAMMAR
    • Thèses soutenues : 11
    • Thèses en cours : 8

Test passif

Le test passif ou monitorage est une approche permettant de tester si un système est conforme à son cahier des charges. De nombreuses techniques dites passives (car elles n’impactent pas le fonctionnement du système) ne considèrent que la partie contrôle des messages utilisés par les protocoles de communication. Les parties données sont alors négligées car elles sont considérées comme non pertinentes dans le test de conformité et sont difficiles à analyser en temps acceptable. Nous avons alors proposé d’étudier de nouvelles approches permettant de rendre symboliques les variables et les données de tels systèmes. L’objectif est de définir les propriétés fonctionnelles mais également les attaques éventuelles dans un réseau de communications en termes de systèmes symboliques. L’intérêt étant de vérifier l’absence ou la présence d’une propriété notamment de vulnérabilité dans un ensemble de traces d’exécution. L’utilisation de valeurs symboliques permet alors d’étudier plusieurs scénarios contenant éventuellement un nombre infini de valeurs réelles instanciées. Les parties contrôle et données des protocoles sont alors prises en considération pour tester des aspects comportementaux ou de sécurité. Notre technique de test passif a été outillée et appliquée dans une architecture IMS (IP multimedia subsystem) et Bluetooth. Elle est également aujourd’hui utilisée en collaboration avec des industriels dans le cadre d’un projet européen ITEA DIAMONDS. Nos travaux ont également été soutenus par le projet STIC AmSud SCAN. Les résultats sont aujourd’hui très prometteurs et permettent de considérer des volumes de données très importants. Plusieurs articles ont par ailleurs été publiés [434, 581, 532, 659].

L’équipe étudie également les problématiques du test de conformité et d’interopérabilité des services IMS. Contrairement aux réseaux MANET dans lesquels les interfaces des entités et couches protocolaires à tester sont très souvent disponibles, ce n’est plus le cas pour les services IMS qui font appel à des services externes dans des architectures distribuées. Les premiers résultats basés sur la définition syntaxique et sémantique d’invariants ont permis de vérifier de nombreuses propriétés (notamment sur le protocole SIP) sur de grandes traces d’exécution. Cela a par ailleurs soulevé de nouvelles difficultés aujourd’hui traitées par la prise en considération des données dans les paquets échangés par les entités communicantes. Pour cela, la logique de Horn est utilisée. Ces techniques ont été étudiées dans le cadre du projet EXOTICUS du pôle Systematic et sont aujourd’hui en cours d’adaptation dans le cadre le projet Stic Amsud CUDEN. Un prototype est mis à disposition sous licence GPL et permet l’analyse par monitorage de trace réelle d’exécution. Ces travaux ont mené à plusieurs publications [491, 503, 504, 622, 436, 429, 454, 623, 453, 591, 509, 480, 588, 506, 474, 475]. Un article [329] a notamment été publié dans ACM/IEEE Transactions on Networking.

Un effort de recherche important a porté sur le test des services web. Nous nous sommes particulièrement intéressés à l’étude d’algorithmes pour le test de la composition de services web en tenant compte aussi bien de la qualité de service que de la qualité d’expérience, et en intégrant des contraintes temporelles. Des résultats sont presentés dans les publications [613, 621, 470, 514, 484, 429, 541, 542, 555, 554, 447, 578]. Nos activités sur le test des services web ont été soutenues par le projet COFECUB ROBUSTWEB.

L’équipe poursuit également ses travaux sur le test de la sécurité. Elle s’est attelée à la conception de techniques pour le test et le monitorage des propriétés de sécurité, la détection d’intrusion et de vulnérabilités.

Nous avons travaillé sur la validation des politiques de sécurité d’organisations et de leur interopérabilité. Nous avons notamment modélisé la notion de confiance (trust) dans un contexte d’interopérabilité d’organisations possédant des politiques de sécurité différentes. Nous avons ainsi développé un modèle formel de la confiance et
défini une extension du langage de contrôle d’accès ORBAC qui intègre ce nouveau concept.

En plus de la détection d’intrusions dans le contexte des réseaux (évoquée plus haut), l’équipe a étudié la détection de vulnérabilités dans le cas des langages de programmation. En se basant sur une modélisation graphique des vulnérabilités, nous avons proposé un langage formel permettant d’associer une description formelle précise et non ambigüe à chaque VCG (graphe des causes de vulnérabilité) en traduisant ses différentes causes en prédicats logiques sur lesquels il devient possible de raisonner. L’obtention d’une telle description formelle a rendu possible la détection de vulnérabilités par le test passif sur des traces d’exécution. Nos travaux ont été publiés dans plusieurs conférences et plusieurs journaux dont par exemple [339, 343, 340, 388, 342]. Plusieurs projets ont aidé à la réalisation de ces travaux, notamment les 2 projets européens FP7 SHIELDS et INTER-TRUST, les 2 projets ANR PIMI et WEBMOV, le projet DGA ISER et le projet CELTIC IPNQSIS.

Test actif

Les aspects mobilité, topologie et connectivité dans les réseaux sans fil mobiles ad-hoc ont ouvert de nouvelles perspectives de recherche tant au niveau génération/exécution des tests de conformité mais également envers la modélisation formelle des fonctionnalités de ces systèmes. Les langages de modélisation, de spécification et de description formels utilisés pour les réseaux filaires ne sont plus adaptés aux contraintes intrinsèques de ces nouveaux systèmes et les architectures de test notamment standardisées par l’ISO sont difficilement applicables aux topologies de ces réseaux qui peuvent être en nombre exponential.

Nous avons donc, dans un premier temps, étudié la modélisation des noeuds dans de tels systèmes en établissant un algorithme d’auto-similarité permettant de réduire le nombre de nœuds à spécifier. Tout en conservant l’observation des cas de test dans la spécification du système, la génération automatisée des séquences de test de conformité a pu être effectuée. Ces méthodes ont ensuite été adaptées au test des protocoles de routage dans les réseaux véhiculaires dans le cadre du projet STIC-Asie MAMI.

Nos travaux ont évolué vers le test d’interopérabilité. En effet, même si certaines propriétés distribuées permettent de tester l’interopérabilité de ces systèmes, il n’existait pas d’architectures de test dédiées à de tels systèmes. Nous avons donc proposé plusieurs modèles qui ont été appliqués sur des implantations réelles intégrées à des testbeds en laboratoire. Ces travaux ont été présentés dans le cadre de conférences internationales [529, 544, 645, 468, 442]. Plusieurs articles de revues ont également été publiés sur le sujet [357, 367, 383] dont un dans ACM computing surveys.

Vérification et modélisation

L’équipe s’intéresse à la définition d’un environnement formel pour le développement sûr d’applications systèmes d’information. Pour ce faire, une modélisation graphique du système à développer est réalisée en UML puis traduite dans le language B pour preuve et validation. Le langage graphique UML ne permettant malheureusement
pas d’exprimer diverses contraintes, nous proposons une approche formelle qui permet de calculer les préconditions additionnelles à ajouter à chaque opération B afin que celle-ci respecte toutes les contraintes de la spécification. L’approche est basée sur la définition d’un ensemble de règles de normalisation et de simplification. Ce travail a donné lieu à plusieurs publications dont [343].

L’équipe s’est également penchée sur la modélisation et la vérification des propriétés dynamiques dont la vérification dépend de plusieurs états pris à des instants différents de l’évolution du système. Nous avons particulièrement étudié la propriété d’atteignabilité [444], de non-interférence[415] et d’absence [416].

Nous avons également mené des recherches sur la détection de la vulnérabilité par la preuve. En effet, l’approche par test passif peut produire des faux positifs car la détection est plutôt syntaxique et les valeurs des variables ne sont pas prises en compte. L’approche que nous proposons se base sur l’utilisation du langage formel B vers lequel des règles de mapping d’un programme C ont été définies. Puis une activité de preuve et de model checking est menée sur la spécification B ainsi obtenue pour affirmer ou détecter l’absence ou la présence de vulnérabilités. Ces travaux ont été publiés dans [445, 443].

Une partie de l’équipe travaille sur le génie logiciel formel, et notamment sur la modélisation des interactions de services et de leur composition [625, 361, 359, 458]. Nous avons également mené des recherches sur la modélisation formelle du vote électronique. Notre principale contribution de recherche était de démontrer qu’il était possible de formaliser certains besoins fonctionnels (voter à un bureau de vote de son choix et la possibilité de revoter), et d’analyser, à travers la simulation de modèles formels, les qualités des services offerts par différentes architectures pour les systèmes distribués de vote électronique. Quelques exemples de nos publications traitant du vote électronique sont [539, 538, 483, 361, 593, 586, 570]. Ces travaux ont été réalisés dans le cadre du projet ANR SAVE.