Stages proposés ( PDF)

SOA

  • Système d'exploitation orienté cloud, Stéphane Frénot détails
  • Outil de manipulation d'interfaces graphiques par le son , Stéphane Frénot Détails

    L'objectif du stage est d'intégrer un outil haute performance d'affichage graphique comme javaFX ou Flex à un outil de reconnaissance de la parole comme sphinx afin de piloter des interfaces graphiques de centres publiques d'affichage. Nous avons déjà développé un prototype permettant d'actionner à la parole telle ou telle type de fonctionnalité et nous souhaiterions l'étendre de manière générique afin de piloter efficacement panneaux d'information.

Formalisation de systèmes

  • Contrats architecturaux formels pour applications orientées services, Lionel Morel Détails
  • Proof carrying code for service oriented systems, Lionel Morel et Nicolas Stouls Détails
  • Encodage de propriétés dynamiques dans des assertions de logique du premier ordre, Nicolas Stouls Détails

    L'objectif de ce stage est dans un premier temps, d'étudier les différentes traductions proposées dans la littérature, avant de les comparer avec les choix effectués au sein de l'outil Aoraï. Ensuite, le candidat sera amené à proposer ses propres heuristiques et à les expérimenter manuellement sur différents exemples. Si ces tests sont concluants, alors il sera possible d'implanter ces propositions au sein de l'outil Aoraï avant la prochaine release de la plateforme FramaC. Une réflexion pourra également être menée sur les extensions possibles du langage de spécification ACSL, pour y inclure des primitives comportementales.

  • Assistance à la vérification automatique de propriétés dynamiques sur du code C, Nicolas Stouls Détails

    L'objectif de ce stage est d'ajouter de nouvelles fonctionnalités au logiciel Aoraï. Plusieurs ont déjà été demandées pour les utilisateurs potentiels et ce sera au stagiaire de choisir les points qu'il souhaite traiter en premier. Parmi les améliorations attendues, nous trouvons : mise à jour du langage de spécification, ajout d'une heuristique considérant des automates déterministes, amélioration de la lisibilité des spécifications générées, implémentation des variables ghost, etc.

    Dans un premier temps, le candidat manipulera l'outil Aoraï pour mieux comprendre son fonctionnement et les choix effectués. Ensuite, à partir du cahier des charges, le candidat sera amené à proposer ses propres solutions algorithmiques de mise à jour. Une réflexion pourra également être menée sur les extensions possibles du langage de spécification ACSL, pour y inclure des primitives comportementales.

  • Extraction et analyse de comportements en présence de contraintes temporelle dans des plate-formes à services dynamiques, Julien Ponge détails

Observation de systèmes

  • CryptPress gestion de logs applicatifs, Stéphane Frénot détails
  • Gestion de traces d'exécution, Stéphane Frénot détails
  • Observation et évaluation de performances de machines virtuelles embarquées , Guillaume Salagnac détails

Sécurité

  • Informatique de confiance en réseau ambiant, Nicolas Stouls et Lionel Morel Détails

    L'objectif de ce stage est d'étudier l'utilisation de l'informatique de confiance dans un réseau ambiant, dans lequel chaque noeud intégrerait un TPM. Le résultat attendu est d'une part un état de l'art des domaines cités, et d'autre part la proposition, soit d'une nouvelle méthode de gestion de la confiance dans les réseaux intégrant des TPM, soit d'un cahier des charges pour un TPM allégé, qui soit suffisant pour ce cas d'application. Dans tous les cas, il sera important de définir précisément les hypothèses effectuées et les propriétés vérifiées par l'approche proposée.

  • Extraction de métriques de sécurité par benchmarking de sécurité pour plates-formes Java, Stéphane Frénot et Pierre Parrend

    L'objectif scientifique est de déterminer un processus d'analyse de sécurité de plates-formes d'exécution type machine virtuelle basé sur des métriques, et de définir ces métriques. L'identification et le reporting de ces métriques formeront le cœur de la contribution scientifique du master. L'objectif technique est de développer un environnement de benchmarking de sécurité pour plates-formes Java dans l'environnement de développement Eclipse. Seront fournis: un ensemble de composants de test de sécurité et robustesse pour Java, et un cahier des charges précis afin de pallier aux difficultés de communications liées à l'encadrement à distance.

Stages Attribués

2009/2010

SOA

  • Felip Acevedo-Viera, 2010, Outil de manipulation graphique d'automates de comportements, Stéphane Frénot Détails

    L'objectif du stage est de réaliser un outil graphique de manipulation de graphes. Les graphes sont générés à partir de fichiers d'enregistrement de l'activité d'un système. Nous avons développé dans l'équipe Amazones une série d'outils algorithmiques permettant l'extraction d'automates de comportements à partir de l'analyse de fichiers d'enregistrement (logs). C'est automates de comportement sont présentés à l'utilisateur selon différents niveau de détails.

  • Sadeddine Menad, 2010, Déploiement automatique et orienté-utilisateur de services sur terminaux mobiles OSGi / Android, Frédéric Le Mouël Détails

    Au laboratoire CITI, nous avons défini AxSeL : A contextual Service Loader. Axsel est une architecture de chargement contextuel de services sur terminaux mobiles prenant en considération aussi bien les contraintes des plates-formes matérielles que les données liées au contexte. Elle se base sur une approche orientée graphe. Le but du stage de master est d'améliorer les algorithmes de coloriage de graphe de manière à y intégrer l'utilisateur. Ceci peut consister à définir un profil utilisateur avec des services requis ou préférés ou peut consister à inclure les statistiques d'utilisation des services avec un système de 'social ranking'.

  • Bertrand Chevalier, 2010, Unification des interfaces applicatives par une approche REST et application à la composition dans Google Android, Julien Ponge détails

Formalisation

  • Nguyen Manh Cuong, 2010, Étude énergétique de logiciels embarqués sur capteurs, Nicolas Stouls et Guillaume Salagnac Détails

    Ce stage s'insère dans la proposition de projet BQR « Méthode de conception pour l'optimisation énergétique de réseaux de capteurs » réalisé en partenariat avec les laboratoires CETHIL (Centre thermique de Lyon) et LIRIS (Laboratoire d'analyse en image et systèmes d'information).

    L'objectif de ce stage est d'étudier les méthodes d'évaluation du coût énergétique des logiciels et de croiser ces critères avec les informations récupérables sur les infrastructures matérielles de capteurs. Il existe des approches par simulation. Il serait intéressant d'étudier si d'autres approches permettant une analyse correcte de pire cas et de cas moyen existent. Le résultat attendu est une proposition théorique de méthode d'évaluation énergétique du coût d'un logiciel en fonction de la plateforme utilisée et du scénario d'utilisation.

  • Herman Mekontso Tchinda, 2010, Université de Yaoundé, Expression SOA en calcul des ambiants, Nicolas Stouls et Stéphane Frénot. détails
  • Fabien Cellier, 2009, Propositions théoriques et implantation d'optimisations fonctionnelles de l'outil d'analyse statique Aoraï, Nicolas Stouls

    L'objectif de ce stage est d'abord d'étudier, puis d'étendre l'outil Aoraï qui permet de vérifier, par la preuve, qu'un programme C respecte une propriété dynamique. Le travail commencera par une découverte de l'outil via la rédaction de différents jeux de test mettant en évidence des lacunes de l'outil. Le stagiaire devra ensuite proposer des solutions théoriques permettant de considérer les limitations observées, puis les implanter. Parmi les extensions possibles, le candidat pourra proposer l'utilisation en interne d'autres plugins de la plate forme Frama-C, tels que l'analyse de valeurs.

Observation

  • Fawaz Hassan, 2010, Modélisation et instrumentation de machines virtuelles pour l'observation, Antoine Fraboulet détails
  • Élise Chénot Étude de faisabilité: Réseaux de capteurs pour la localisation de troupeaux de bétail, Guillaume Salagnac Détails

Sécurité

  • Goichon Francois, 2010, Analyse de code de composants Java: Analyse de flux de données pour la détection de vulnérabilités, Stéphane Frénot et Pierre Parrend

    L'objectif scientifique est d'identifier la possibilité de passage à l'échelle de la découverte de vulnérabilités par analyse statique de code en fonction des catégories de bugs connues, dans le cas des langages objets: des vulnérabilités simples peuvent être identifiées avec un haut niveau d'abstraction, et d'autres nécessitent une modélisation très fine du programme, ce qui rend l'analyse d'applications de grande taille (>10^6 lignes de code) impossibles. L'objectif technique est le développement d'un ensemble de plugins Eclipse permettant aux développeurs de réaliser eux-mêmes des revues de code automatiques.

Thèses en cours

  • zheng hu, Thèse CIFRE avec France Télécom, Reconnaissance et Intégration d'équipements électriques, Co-encadrement Bernard Tourancheau, Stéphane Frénot
  • Andreea Chis, Thèse MENRT, Sensor Network Cross Layer Optimization, Co-encadrement Eric Fleury, Antoine Fraboulet
  • Riadh Ben Abdallah, Thèse en collaboration avec le CEA, Virtual Machine for Software Defined Radio, Co-encadrement Tanguy Risset, Antoine Fraboulet