Logiciels, Prototypes et Démonstrateurs

• SMOF (Safety Monitoring Framework) J. Guiochet, H. Waeselynck, 2018: https://www.laas.fr/projects/smof
• YOUCAN (Hazard model-based analysis with HAZOP-UML.) J. Guiochet, 2018: https://www.laas.fr/projects/HAZOPUML
• Osmosis (Open Source Material fOr Safety assessment of Intelligent Systems), J. Guiochet, H. Waeselynck, 201X: https://osmosis.gitlab.io/index.html
• NFLib est une bibliothèque conçue afin d'optimiser les performances calculatoires des opérations arithmétiques effectuées entre polynômes, M.-O. Killijian, C. Aguilar Melchor et al.: https://github.com/quarkslab/NFLIb
• XPIR (Private Information Retrieval for Everyone), M.-O. Killijian, C. Aguilar Melchor et al., 201X: https://github.com/XPIR-team/XPIR
  bibliothèque dédiée à la contruction de protocoles PIR
• MIRAGE, V. Nicomette, R. Cayre et al., 2019, https://homepages.laas.fr/rcayre/mirage-documentation/
  un framework pour l'analyse de vulnérabilités et l'audit de sécurité d'objets connectés
• GEPETO (GEoPrivacy-Enhancing TOolkit), M.-O. Killijian, M. Nunez del Prado Cortez, S. Gambs (Univ. Rennes), 2014 (Diffusion par GIT. License CeCILL-B)
  GEPETO est un logiciel flexible qui peut être utilisé pour visualiser, assainir, effectuer des attaques d’inférence et mesurer l'utilité d'un ensemble de données géolocalisées. L'objectif principal de GEPETO est de permettre à un conservateur de données (par exemple, une entreprise, un organisme gouvernemental ou une autorité de protection des données) de concevoir, configurer, expérimenter et évaluer divers algorithmes d'assainissement des données et différentes d'attaques d’inférence. Il permet également de visualiser les résultats correspondants et d'évaluer les compromis résultants entre la vie privée et l'utilité des données.
• MARACAS (CBSE Middleware for adaptive fault tolerance), J. C. Fabre, M. Roy, M. Stoicescu, 2014 (Diffusion restreinte)
  Ce logiciel permet de montrer comment des mécanismes de tolérance aux fautes peuvent être adaptés et combinés en ligne. Des critères de ressources, d'évolution des applications, de changement de modèle de faute en vie opérationnelle, peuvent être à l'origine de la reconfiguration dynamique des mécanismes de tolérance aux fautes. Un ensemble de mécanismes a été développé pour montrer les capacités de l'approche à composant sur un support d’exécution réflexif pour réaliser des systèmes sûrs de fonctionnement agiles. Il s'agit d'une preuve de concepts, les principes techniques qu'il démontre sont applicables à de très nombreux domaines d'application.
• ARINC 653 Simulator, M. Cronel, J. C. Fabre, G. Bustamente, R. Palustran, M. Roy: https://github.com/makrin/ARINC653-simulator (Licenses MIT et CeCILL-B, Diffusion par GIT)
  Un simulateur du standard d’exécution ARINC 653 pour l’IMA a été développé sur Unix. Il permet d’émuler les concepts associés de partitionnement d’espace et de temps, ainsi que les mécanismes de communication inter-partitions.
• IronHIDE (outil d’analyse des attaques par entrées-sorties), E. Alata, Y. Deswarte, F. Lone Sang, V. Nicomette, (Diffusion restreinte)
  IronHIDE est un contrôleur d’entrées-sorties utilisant la technologie FPGA, qui est dédié à l’analyse de vulnérabilités à l’interface entre les composants logiciels et matériels. Ce contrôleur a l’avantage de s’interfacer avec les bus PCI-Express et permet de générer des requêtes valides et invalides sur ces bus pour identifier des attaques par entrées-sorties.
• MINOTOR (Monitoring tool for timing and behavioral analysis), O. Baldellon, J. C. Fabre, M. Roy
  Cet outil basé sur une extension de Réseaux de Petri permet la surveillance et l’analyse en ligne de propriétés temporelles et comportementales de systèmes répartis. L’outil est conçu pour fonctionner dans des environnements distribués dans lesquels l’observation peut être imparfaite.
• SOUK (Social Observation of hUman Kinetics), E. Alata, R. Akrout, Y. Bachy, A. Dessiatnikoff, M. Kaâniche, V. Nicomette, 2012 (Diffusion restreinte)
  L'objectif de ce logiciel est d'identifier de façon automatique les vulnérabilités d'une application web. L’approche est basée sur un parcours combinatoire du site et l’exploitation réelle des vulnérabilités. Des requêtes spécifiques aux vulnérabilités recherchées sont générées à partir d’une grammaire et les réponses sont analysées par des techniques de clustering. Cette approche présente deux avantages. Le premier avantage est la capacité de poursuivre l’analyse après l'exploitation d'une vulnérabilité. En particulier, les pages accessibles après l'exploitation de la vulnérabilité peuvent être traitées automatiquement. Le second avantage est sa capacité à identifier des vulnérabilités qui sont activées uniquement après avoir réalisé une séquence d'actions particulières sur le site.
• WASAPY (Web Applications Security Assessment in Python), E. Alata, R. Akrout, Y. Bachy, A. Dessiatnikoff, M. Kaâniche, V. Nicomette, 2012 (Diffusion restreinte)
  L'objectif de ce logiciel est d'identifier de manière automatisée les vulnérabilités des applications web. Pour ce faire, WASAPY effectue une analyse combinée du site web et de l'exploitation des vulnérabilités. Des requêtes spécialement conçues à partir d'une grammaire sont soumises à l'application, et les réponses correspondantes sont analysées à l'aide de techniques de regroupement. Cette approche présente deux avantages. Le premier est la capacité du logiciel à poursuivre son analyse après l'exploitation d'une vulnérabilité. En particulier, les pages accessibles après l'exploitation de la vulnérabilité peuvent être traitées automatiquement. Le second avantage est sa capacité à identifier les vulnérabilités qui ne sont activées qu'après l'exécution d'une séquence d'action particulière sur le site.
• HAZOP-UML (Risk analysis for the identification and validation of safety requirements), Q.A. Do Hoang, D. Martin-Guillerez, J. Guiochet, D.Powell, 2011 (Diffusion restreinte)
  HAZOP-UML est un outil d'analyse de risque basée modèle. Cet outil permet de modéliser des diagrammes UML (Unified Modeling Language) de séquence et de cas d'utilisation, utilisés pour générer des tables de déviations en appliquant la technique HAZOP (HAZard OPerability).
• STELAE (Systems TEst LAnguage Environment), R. Guduvan, H. Waeselynck, V Wiels (ONERA), G. Durrieu (ONERA), Y. Fusero (Cassidian), M. Schieber (Cassidian), 2010 (Diffusion restreinte)
  STELAE est un environnement d'ingénierie dirigée par les modèles, pour le développement de tests de systèmes avioniques. Il inclut des éditeurs personnalisables (graphiques et textuels) pour les modèles de tests abstraits, des vérifications sur ces modèles, et enfin des transformations de modèles basées sur des templates, permettant de générer du code exécutable sur une plate-forme de test industrielle (la plate-forme U-Test de Cassidian Test & Services). Le coeur de STELAE est constitué d'un méta-modèle intégrant un ensemble riche de concepts spécifiques au domaine du test dans l'avionique.
• STANCE (Structural ANalysis of Counter Examples), T. Bochot (ONERA & Airbus), K. Cabrera, P. Virelizier (Airbus), H. Waeselynck, V. Wiels (ONERA)
  STANCE vise à faciliter la mise au point de modèles Simulink, en exploitant les contre-exemples retournés par un outil de vérification formelle (« model checker »). Il effectue une analyse structurelle des chemins du modèle activés par le contre exemple et extrait les informations pertinentes pour expliquer la violation de propriété observée. STANCE peut également être utilisé pour guider le model checker dans la recherche de contre-exemples différents, présentant de nouveaux scénarios d'activation de chemins et donc de nouvelles façons de violer la propriété.
• TERMOS (TEst Requirement language for MObile Setting), P. André, Z. Micskei (BUTE), M.D. Nguyen, N. Rivière, H. Waeselynck, 2009 (Diffusion restreinte)
  TERMOS est un langage formel basé sur les diagrammes de séquence UML, utilisé pour le test d'applications mobiles. L'outil support est intégré à la technologie UML et comprend : (1) un profil UML pour l'édition de scénarios à vérifier (exigences positives et négatives, objectifs de test) avec des vues spatiales et événementielles, (2) un plugin Eclipse pour la vérification automatique de traces de test par rapport aux scénarios spécifiés. La vérification d'une trace de test combine des algorithmes d'appariement de graphes et de calculs d'ordres partiels d'événements. La partie d'appariement de graphes recherche les occurrences de la séquence des configurations spatiales du scénario. L'analyse de l'ordre des événements d'interaction repose sur une sémantique des diagrammes de séquence donnée par la construction d'un automate.
• MASS (Multi Agent Simulator Software), J.H. Collet, 2007 (Diffusion restreinte)
  MASS est un simulateur d'agents mobiles en 2 ou 3 dimensions. Les agents sont activés de façon asynchrone par un scheduler, et chacun exécute un automate d'états. Le logiciel tourne sous Windows. Il a été parallélisé pour tirer parti des processeurs multicoeurs.