Journée: AFSEC "méthodes formelles pour la sécurité" 21 juin 2017

Quand: Le 21 juin 2017
Lieu: ECE Paris — Ecole d’ingénieurs
Campus Eiffel 1   10 rue Sextius Michel – 75015 Paris
Métro ligne 6 (stations Bir-hakeim ou Duplex), RER C (station Champ de Mars)

Du fait des restrictions budgétaires, l’action prendra en charge les pauses café et le repas de midi sera à la charge de chacun. L’inscription (gratuite) au plus tard le 20 mai 2017 est nécessaire en envoyant un email à claire.pagetti@onera.fr ; objet : “Inscription AFSEC 21 juin” (cliquer sur le lien) - préciser : Nom et Affiliation.

Programme :

• 9h15-9h30: accueil
• 9h30-9h45: Mot d’accueil ECE
• 9h45-11h0  La sécurite des systèmes embarqués : quelques cas d’études (Vincent Nicomette, LAAS)
  • Résumé: Les systèmes informatiques d’aujourd’hui ne sont plus des simples PC de bureau classiques. L’informatique est partout et elle est notamment de plus en plus embarquée, dans les moyens de transport par exemple mais aussi dans les objets connectés qui envahissent chaque jour d’avantage notre quotidien. Par ailleurs, l’utilisation massive du réseau Internet a facilité la propagation de logiciels malveillants, qui peuvent aujourd’hui cibler tous ces types d’équipements informatiques. Alors qu’il existe déjà des normes permettant d’évaluer la sécurité d’équipements informatiques “classiques”, leur application aux équipements embarqués est encore limitée. La présence et la criticité des vulnérabilités qui peuvent affecter ces équipements sont encore mal connues car pas suffisamment étudiées.
    Cet exposé présente des travaux de recherche qui ont été menés au LAAS depuis plusieurs années sur le thème de la sécurité des systèmes embarqués. Deux exemples seront présentés sur différents types d’équipements. La première étude
    présente une analyse de vulnérabilités d’un système embarqué critique avionique, réalisé dans la cadre d’une collaboration avec Airbus. La seconde étude concerne une analyse de vulnérabilités de systèmes embarqués dans deux types d’équipements connectés : les box ADSL et les téléviseurs connectés. Cette étude a été réalisée dans le cadre d’une collaboration avec Thalès. La présentation de ces cas d’études sera précédée d’une introduction générale à la sécurité informatique et aux propriétés associées.
  • Bio: Vincent Nicomette est professeur à l’INSA de Toulouse et chercheur dans l’équipe Tolérance aux Fautes et Sûreté de Fonctionnement Informatique du LAAS-CNRS. Il est diplômé de l’ENSEEIHT option Informatique
    en 1992, a obtenu son doctorat de l’TNP de Toulouse en 1996 et son HDR de l’INP de Toulouse en 2009. Ses principaux thèmes de recherche concernent la sécurité dans les systèmes répartis, la sécurité des systèmes d’exploitation et des systèmes embarqués.
• 11h-12h Sécurité des applications : quels outils ? quelles techniques ? (Marie-Laure Potet, Verimag)
  • Résumé: L’analyse de code pour chercher des vulnérabilités ou évaluer leur robustesse vis-à-vis d’attaques pose des problèmes différents de la vérification ou la recherche de bugs pour la sûreté. Dans un premier temps nous illustrerons ceci à travers des exemples et montrerons les outils adaptés pour ces analyses. Un premier type d’analyse de vulnérabilités sera ensuite illustré par l’approche Gueb, développée dans le cadre du projet ANR BinSec, qui combine analyses statique et concolique pour la détection de use-after-free. Nous nous intéresserons ensuite à l’analyse de la robustesse de code contre l’injection de fautes. Nous présenterons FISCC, la première collection publique de code durci contre l’injection de fautes ainsi que des métriques d’évaluation de la robustesse à l’injection de fautes. Ces derniers travaux sont développés dans le cadre du projet DGA-ANR Sertif.
  • Bio: Marie-Laure Potet est Professeur à l’Ensimag, école de Grenoble INP, et chercheur au laboratoire Verimag. Elle a travaillé dans le domaine des méthodes formelles (approche correction par construction) pour la validation de systèmes sûrs et la certification Critères Communs. Depuis 8 ans elle anime une équipe à Vérimag sur l’analyse de code pour la sécurité et l’analyse de vulnérabilités à partir de modèles. Elle est impliquée dans de nombreux projets collaboratifs en sécurité.
• 13h-14h Vérification automatique de propriétés d’équivalence (Vincent Cheval, LORIA)
  • Résumé: La conception et l’analyse des protocoles de sécurité sont connues pour être difficiles puisqu’elles demandent de considérer toutes les actions malicieuses d’un attaquant sur le protocole. Les modèles symboliques ont été utilisées avec succès pour prouver la sécurité de protocoles et pour découvrir de nouvelles failles de sécurité. Pourtant, prouver à la main la sécurité des protocoles cryptographiques est difficile et souvent source d’erreurs. C’est pourquoi une grande variété d’outils de vérification automatiques a été développée afin de prouver ou découvrir des attaques sur les protocoles. Je présenterai dans un premier temps un aperçu des outils existants puis je parlerai plus précisément des techniques de vérification automatique développées au sein de l’équipe PESTO pour vérifier différentes notions d’équivalence de processus. Ces notions étant particulièrement importantes pour exprimer de nombreuses propriétés de sécurité (ex: l’anonymat, la confidentialité du vote, la non-traçabilité).
  • Bio: Vincent Cheval est  chargé de recherche à Inria Nancy au sein du LORIA. Ses thèmes de recherche concernent l’analyse et la vérification de protocoles cryptographiques au sein de modèles formels, développement d’outils et la vérification de programmes.
• 14h-15h Formal Methods and the Dark Side of the Force (Jean-Louis Lanet, Université de Rennes)
  • Résumé: Formal methods have been used in the industry for a long time with some noticeable successes. Unfortunately any technology can have a dual use, and in particular, attackers can use rigorous technologies for discovering weaknesses in a product or hidding a code inside another one.
  • Bio: Jean-Louis Lanet joined INRIA- Rennes Bretagne Atlantique in September 2014 to be involved into the High Security Labs (LHS) for a four years period. He has been Professor at the University of Limoges (2007-2014) at the Computer Science department, where he lead the team SSD (Smart Secure Device). He was also associate professor of the University of Sherbrooke and was in charge of the Security and Cryptology course of the USTH Master (Hanoi). His research interests included the security of small systems like smart cards, but also software engineering. Prior to that, he was senior researcher at Gemplus Research Labs (1996-2007) the smart card manufacturer. During this period he spent two years at INRIA (2003-2004) as an engineer at DirDRI (Direction des Relations Industrielles) and senior research associate in the Everest team at INRIA Sophia-Antipolis. He got my Habilitation à Diriger des Recherches (HdR) during the first INRIA period. He was researcher at the Advanced Studies Labs of Elecma, Electronic division of the Snecma, now part of the Safran group where he worked on hard real time techniques for jet engine control (1984-1995).
• 15h15-16h15 Model Based Safety and Security Analyses of Avionics Systems (Pierre Bieber et Julien Brunel, ONERA)
  • Résumé: We aim at developing common models and tools to assess safety and security. In this talk we propose adaptations of models devised for safety assessment of avionics platforms in order to analyse their security. We describe  a security modelling and analysis approach based on the AltaRica and Alloy languages and their associated tools. The approach is illustrated by avionics case-studies. We report lessons learnt about the convergence and divergence points between security and safety with respect to modelling and analysis techniques.
  • Bio: Pierre Bieber et Julien Brunel sont ingénieurs de recherche à l’ONERA Toulouse, ils travaillent sur les méthodes d’analyse de la sécurité des systèmes aéronautiques.
• 16h15-17h15 Opacité probabiliste (Béatrice Bérard, LIP6)
  • Résumé: L’opacité est un cadre générique qui permet de décrire formellement certaines propriétés de sécurité liées aux fuites d’information. Elle prend comme paramètres les exécutions d’un système, dont
    certaines sont considérées comme secrètes, et une fonction d’observation fournissant une vue partielle des exécutions à un agent extérieur qui connaît la structure du système. Le secret est opaque si pour toute exécution secrète, il en existe une non secrète avec la même observation. Après un bref panorama des résultats obtenus, je présenterai des extensions probabilistes de la notion d’opacité, avec pour but de mesurer la résistance d’un système aux fuites d’information et d’en comparer plusieurs réalisations. (travaux communs avec Serge Haddad, Olga Kouchnarenko, Engel Lefaucheux, John Mullins et Mathieu Sassolas).
  • Bio: Béatrice Bérard est professeur à l’Université P. et M. Curie et chercheur au LIP6, en délégation Inria au LSV pour 2016/2017. Ses thèmes de recherche concernent les questions d’expressivité et de vérification pour des modèles quantitatifs (temporisés ou probabilistes), avec des applications à la sécurité et aux systèmes de transport automatisés.

Journée AFSEC organisée par Pierre Bieber, Julien Brunel et Claire Pagetti.
Organisée avec le soutien du GDR GPL.
Organisation locale: Xiaoting Li, Sebti Mouelhi ECE