Actualités du projet

  • Présentation au Colloque "Systèmes embarqués, Sûreté de fonctionnement, Sécurité", à Toulouse les 13 et 14 décembre 2010 par Thierry Lecomte et Dominique Méry du bilan du projet RIMEL. L'exposé est consultable.

  • Joris Rehm a reçu le Prix des Unversités de Lorraine le 4 octobre 2010 au cours de la cérémonie de rentrée des universités de Lorraine. Ce prix est attribué pour les travaux menés dans le cadre du projet RIMEL de l'ANR notamment pour l'intégration du temps dans les modèles Event B au cours du raffinement.

  • Présentation des patrons de développement prouvés pour les protocoles cryptologiques à la conférence CSR 2010 organisée du 16 juin au 21 juin 2010 à Kazan. Les travaux présentés concernent une partie de la thèse Nazim Benaissa.

  • ViSiDiA: Visualization and Simulation of Distributed Algorithms est maintenant sous une nouvelle version; B2VISIDIA sera très prochainement intégré.

  • Les quatre universités de Lorraine ont attribué le Prix IAEM à Joris Rehm pour son travail de thèse soutenue le 10 décembre 2009. Ce prix lui sera décerné en octobre 2010 lors de la remise des prix de thèse et de la cérémonie des docteurs honoris causa.
  • Le 28 mai 2010, Nazim benaissa a soutenu sa thèse intitulée: La composition des protocoles de sécurité avec la méthode B événementielle. Cette thèse a été préparée daqns le cadre du projet RIMEL et a été financée par une bourse du gouvernement algérien et par l'ANR RIMEL.
    Résumé: De nos jours, la présence de réseaux à grande échelle dans notre société bouleverse nos habitudes avec l'apparition de nouveaux services distants avec des besoins en matière de sécurité de plus en plus important. De nombreux mécanismes de sécurité sont mis en \oe uvre pour garantir les propriétés désirées, ainsi nous trouvons dans les réseaux informatiques des services d'authentification, d'autorisation, des pare-feux, des systèmes de détection d'intrusions, \ldots Nous avons abordé tout au long de cette thèse la problématique de la vérification de ces mécanismes de sécurité avec une approche compositionnelle. Nous nous sommes intéressé plus particulièrement aux protocoles cryptographiques ainsi qu'aux politiques de contrôle d'accès. Nous avons utilisé la méthode B événementielle et ses différentes techniques de composition de modèles formels. Composition et cryptographie : La première partie de la thèse est consacrée à la composition des protocoles cryptographiques ainsi que leurs intégration avec d'autres types de protocoles. Nous avons étudié aussi bien l'exécution parallèle des protocoles que leur composition pour obtenir des protocoles plus complexes. Nous avons notamment introduit la notion de mécanismes cryptographiques qui sont des protocoles simples qui peuvent être composés pour obtenir des protocoles plus complexes sous réserve de faire les preuves nécessaires. Nous avons utilisé dans nos travaux les différentes techniques de composition de modèles B événementiels. Un modèle B événementiel réutilisable de l'attaquant a également été proposé. Nous avons également élaboré une méthode pour la reconstitution d'éventuelles attaques. Déploiement des politiques des contrôle d'accès : La seconde partie de la thèse est consacrée au déploiement des politiques de contrôle d'accès par le raffinement, l'idée consiste à partir de politiques de sécurité abstraites et de les raffiner afin d'obtenir des politiques plus concrètes. Nous avons pour cela proposé un modèle général paramétrable en B événementielle pour les politiques de contrôle d'accès. Nous avons notamment appliqué cette méthode pour vérifier le déploiement d'une politique de contrôle d'accès dans un système où est implémentée une autre politique de contrôle d'accès. Nous proposons également de combiner la technique de raffinement avec la technique de composition pour répondre au problème de la complexité des politiques de contrôle d'accès que l'on souhaite déployer.
  • Le 10 décembre 2009, Joris Rehm a soutenu sa thèse intitulée: Gestion du temps par le raffinement. Cette thèse a été préparée daqns le cadre du projet RIMEL et a été financée par une allocation du MESR.

  • Organisation d'un tutorial BART d'une journée à l'occasion de ABZ 2010 par Thierry Lecomte.

  • Présentation de BART lors d'une journée industrielle organisée à Tokyo lors du Grace International Symposium on Advanced Software Engineering. par Thierry Lecomte.

  • Workshop on Recent Innovations and Applications in B [RIAB] est organisé par Thierry Lecomte dans le cadre de la conférence FM 2009 le 3 Novembre 2009 à Eindhoven.

  • BART est en cours de validation par les partenaires industriels de ClearSy. Cet outil de raffinage automatique est en lien avec l'Atelier B dont une nouvelle version est mise à disposition gracieuse.

  • Atelier B 4.0 est disponible sur le site de la société partenaire ClearSy. Il ne s'agit pas d'un résultat de RIMEL mais ce composant sera utile pour la suite.

  • Le projet ViSiDiA: Visualization and Simulation of Distributed Algorithms est développé au sein du projet RIMEL dans le cadre de l'axe Outils du projet; une action du projet vise à lier cet outil à la platefome RODIN.

  • The Event B Homepage at LORIA est un site qui donne les informations spécifiquement sur le langage Event B et les travaux menés au LORIA ou ailleurs. Cette page est référencée par l'éditeur Springer dans le cadre de l'ouvrage suivant: Logics of Specification Languages de la série Monographs in Theoretical Computer Science. An EATCS Series Bjorner, Dines; Henson, Martin C. (Eds.) . A chapter on Event B coécrit par Dominique Cansell et Dominique Méry.