Événements

Programme

• 13:30 - 14:00 Olivier Nicole, Matthieu Lemerre, Sébastien Bardin et Xavier Rival. Pas de Pannes, Pas d'Exploits : Vérification Automatique de Noyaux Embarqués (Papier AFADL 2021) [Résumé PDF]
  Rejeu d'une publication acceptée à RTAS 2021.
• 14:00 - 14:30 Gilles Barthe, Benjamin Grégoire, Vincent Laporte et Swarn Priya. Modèle de fuite structurée & applications à la compilation sécurisée [Résumé]
• 14:30 - 15:00 Nicolas Magaud. Un prouveur automatique pour la géométrie projective et son intégration à Coq [Résumé]
• 15:00 - 15:30 Cyril Cohen. Unsolvability of the Quintic Formalized in Dependent Type Theory [Résumé]

• 9:00 - 9:30 Arthur Clavière, Eric Asselin, Christophe Garion et Claire Pagetti. Vérification formelle de la sûreté d'un système contrôlé par réseaux de neurones [Résumé PDF]
  Cet article est un résumé étendu de l'article "Safety Verification of Neural Network Controlled Systems", soumis à SSIV 2021 (7th International Workshop on Safety and Security of Intelligent Vehicles). Dans cet article, nous proposons une approche pour vérifier la sûreté d’une classe particulière de systèmes contrôlés par réseaux de neurones, combinant un système dynamique temps continu avec avec contrôleur temps discret, et où le contrôleur est un classificateur basé sur plusieurs réseaux de neurones. Nous définissons un modèle pour ce type de système, et la procédure d’analyse d’atteignabilité associée, permettant ainsi de calculer une sur-approximation des états atteignables par ce système. Cette méthode est illustrée à l'aide d’un cas d’étude aéronautique.
• 9:30 - 10:00 Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling et Pascale Le Gall. Méthodologie pour la validation d'exigences globales appliquée à la sécurité [Résumé PDF]
  La spécification et la vérification formelle d'exigences de haut niveau (telles que les propriétés de sécurité comme la confidentialité ou l'intégrité des données) sur un logiciel de grande taille est toujours un défi important pour l'industrie. Des travaux récents ont introduit une méthode basée sur le greffon de Frama-C MetAcsl permettant de spécifier des propriétés haut niveau appelées les HILARE sur des programmes C et de les transformer en assertions pouvant être vérifiées par des approches classiques. Cet article présente une méthodologie pour la spécification et la vérification d'un large éventail de propriétés de haut niveau et l'illustre sur plusieurs exemples. Le but est de donner aux utilisateurs des outils de vérifications des recommandations détaillées pour traiter des formes communes de propriétés afin de faciliter leur travail quotidien et d'éviter certains écueils. Cette méthodologie est illustrée sur des formes communes de propriétés et sur deux cas d'études. Le premier — sur le code réel du bootloader du projet de clé USB sécurisée Wookey — a été complètement vérifié en utilisant l'approche décrite, démontrant ainsi sa capacité à passer à l'échelle. L'autre cas d'étude — sur le le micronoyau d'un OS — a été ajouté pour illustrer d'autres propriétés courantes, et la description de son architecture a été volontairement laissée très générique.
• 10:00 - 10:30 Tithnara Nicolas Sun, Luka Le Roux, Ciprian Teodorov et Philippe Dhaussy. Exploration de Scénarios de Systèmes Cyber-Physiques pour l'Analyse de la Menace [Résumé PDF]
  La cybersécurité des systèmes est un besoin vital depuis que l'industrie se dirige vers l'automatisation, que ce soit dans les systèmes cyber-physiques ou dans "l'industrie du futur". Il est désormais nécessaire d'envisager la sécurité comme une problématique continue et accompagnant le système tout au long de son cycle de vie. Les méthodes de modélisation actuelles se focalisent généralement sur le système à un instant précis, que ce soit en conception ou en pentest. Cependant, ces analyses ne tiennent pas compte de l'évolution du système et ne garantissent donc pas de résultats pérennes. Dans cet article, nous proposons un environnement de modélisation et de simulation de scénarios d'attaque prenant en compte l'aspect opérationnel du système. Pour cela nous introduisons un langage de scénarios exécutable. Ce langage permet à la fois d'enrichir une modélisation statique du système d'une part et de modéliser le comportement de l'attaquant d'autre part. Nous illustrons notre approche sur une station de pompage. Nous montrons comment un expert peut capturer d'une manière abstraite sa compréhension du système afin de la confronter à une modélisation des capacités de l'attaquant. Ceci permet d'exhiber des analyses formelles de sécurité sur le système sous attaque.
• 10:30 - 11:00 Pierre-Alain Yvars and Laurent Zimmer. DEPS Studio : Un environnement intégré de modélisation et de résolution pour la synthèse de système [Résumé PDF]
  Nous présentons DEPS Studio, un environnement intégré de modélisation et de résolution conçu pour poser et résoudre des problèmes de synthèse de système. Cet environnement permet d'éditer, de compiler, de déboguer et de résoudre des problèmes exprimés dans le langage de modélisation DEPS. DEPS (Design Problem Specification) traite des problèmes de dimensionnement, de configuration, de déploiement de fonctions et plus généralement de génération ou de synthèse d'architecture rencontrés dans la conception de système. Les systèmes considérés peuvent être des systèmes physiques, des systèmes à forte composante logicielle ou des systèmes mixtes (embarqués, cyber-physiques). Ce langage combine des fonctionnalités de modélisation structurelle propres aux langages orientés objet avec des fonctionnalités de spécification de problème issues de la programmation par contraintes. Après quelques rappels sur le langage de modélisation, nous présentons les différents éléments qui composent l'environnement intégré. Nous détaillons notamment l'organisation de la chaîne de compilation depuis l'édition du modèle jusqu'à la génération du modèle de calcul ainsi que les principales fonctionnalités du solveur de programmation par contraintes mixte qui a été spécifiquement développé pour être intégré dans cet IDE.

• 13:30 - 14:00 Lesly-Ann Daniel, Sébastien Bardin et Tamara Rezk. Binsec/Rel : Exécution Symbolique Relationnelle Efficace pour Analyse de Binaire Constant-Time (Papier AFADL 2020) [Résumé PDF]
  Constant-time est une contre-mesure aux attaques temporelles qui interdit les branchements et les accès mémoires dépendants des secrets. Cette contre-mesure n'est généralement pas préservée par le compilateur et requiert donc de raisonner au niveau binaire. Or, les outils d’analyse dédiés à constant-time raisonnent actuellement à un plus haut niveau (C ou LLVM), approximent la sémantique du programme, ou ne passent pas à l’échelle. Nous concevons une technique d'analyse efficace au niveau binaire qui ne fait pas d’approximation sur la sémantique du programme, permettant à la fois de trouver des bugs ou de faire de la vérification bornée pour constant-time. Celle-ci s'appuie sur l'exécution symbolique relationnelle, à laquelle nous ajoutons des optimisations dédiées. Nous proposons un prototype, Binsec/Rel et réalisons des expériences sur un ensemble de 338 binaires cryptographiques, démontrant le passage à l'échelle de notre technique. De plus, en utilisant Binsec/Rel, nous avons automatisé et étendu une étude existante sur la préservation de constant-time par les compilateurs. Nous avons ainsi découvert des violations introduites par les compilateurs qui étaient hors de portée des outils d’analyse pour LLVM, soulignant l’importance de raisonner au niveau binaire.
• 14:00 - 14:25 Manh-Dung Nguyen. Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities (Papier AFADL 2020) [Résumé PDF]
  Directed fuzzing focuses on automatically testing specific parts of the code by taking advantage of additional information such as (partial) bug stack trace, patches or risky operations. Key applications include bug reproduction, patch testing and static analysis report verification. Although directed fuzzing has received a lot of attention recently, hard-to-detect vulnerabilities such as Use-Afer-Free (UAF) are still not well addressed, more especially at the binary level. We propose UAFuzz, the first (binary-level) directed greybox fuzzer dedicated to UAF bugs. The technique features a fuzzing engine tailored to UAF specifics, a lightweight code instrumentation and an efficient bug triage step. Experimental evaluation for bug reproduction on real cases demonstrates that UAFuzz significantly outperforms state-of-the-art directed fuzzers in terms of fault detection rate, time to exposure and bug triaging. UAFuzz has also been proven effective in patch testing, leading to the discovery of 20 new bugs in Perl, GPAC and GNU Patch (including a buggy patch) - all of them have been acknowledged and 14 have been fixed. Last but not least, we provide to the community the first fuzzing benchmark dedicated to UAF, built on both real codes and real bugs.
• 14:25 - 14:50 Thibault Martin, Nikolai Kosmatov, Virgile Prevosto et Matthieu Lemerre. Détection d’objectifs de test polluants pour les critères de flot de données (Papier AFADL 2021) [Résumé PDF]
  Dans ce travail, nous évaluons trois approches pour détecter les objectifs de test polluants pour les critères de flot de données, avec une analyse de flot de données simple, une analyse de valeurs, basée sur l'interprétation abstraite, et une analyse de plus faible précondition. Nous avons implanté ces approches dans LT EST, une boîte à outils open-source pour le test. Nous avons ensuite évalué et comparé ces techniques sur différentes études de cas et avons analysé leurs capacités à détecter les objectifs polluants et leurs limites. Nous nous sommes concentrés sur la partie clef des critères de flot de données : les paires def-use. Les capacités de détection que nous avons observées semblent être différentes de celles des expériences similaires faites précédemment pour d'autres critères.
  
  Cette soumission est un résumé long du papier "Detection of Polluting Test Objectives for Dataflow Criteria" paru à IFM 2020.
• 14:50 - 15:20 Frédéric Tamagnan. Identifying and Generating Missing Tests using Machine Learning on Execution Traces [Résumé]
  Testing IT systems has become a major bottleneck for many companies. Besides the growing complexity of such systems, shorter release cycles and increasing quality requirements have led to increased verification and validation costs. However, analysis of existing testing procedures reveals that not all artifacts are exploited to tame this cost increase. In particular, customer traces are usually ignored by validation engineers. In this paper, we use machine learning from execution traces (both customer traces and test execution traces) to identify test needs and to generate new tests in the context of web services and API testing. Log files of customer traces are split into smaller traces (user sessions) then encoded into Pandas DataFrames for data analysis and machine learning. Clustering algorithms are used to analyse the customer traces and compare them with existing system tests, and machine learning models are used to generate missing tests in the desired clusters. The tool-set is implemented in an open-source library called Agilkia.
• 15:20 - 15:30 Mot des responsables MTV2

• 9:00 - 9:30 Nicolas Nalpon, Celia Picard, Cyril Allignol et Sebastien Leriche. Vers la vérification de smala, un langage réactif-interactif (Papier AFADL 2020) [Résumé PDF]
  
  Smala est un langage réactif dédié à la programmation de systèmes à forte composante interactive. Pour pouvoir utiliser ce langage dans un contexte critique, il est nécessaire de pouvoir apporter des garanties. Ainsi, nous nous intéressons à la vérification formelle du compilateur de Smala, avec pour objectif de garantir la préservation de la sémantique du programme source à la compilation. Dans un premier temps, nous avons limité notre étude à un sous-ensemble de Smala. Dans cet article, nous présentons une version préliminaire de la sémantique opérationnelle de ce sous-ensemble.
  Cécile Marcon, Nicolas Nalpon, Cyril Allignol et Celia Picard. Représentation de programmes Smala grâce à la théorie des bigraphes (Papier AFADL 2021) [Résumé PDF]
  Dans le but de certifier le compilateur du langage réactif-interactif Smala,nous cherchons à représenter sa sémantique en instanciant la théorie des bigraphes. En nous limitant dans un premier temps à un sous-ensemble de ce langage, nous avons pu représenter ses différents acteurs comme des entités distribuées dans l'espace. Des règles de réaction sur les bigraphes permettent de mettre ces entités en mouvement et en relation les unes avec les autres afin de représenter l'exécution du programme en plus de sa structure.
• 9:30 - 10:00 Léo Gourdin. Formally verified postpass scheduling with peephole optimization for AArch64. [Résumé PDF]
  Compcert is a C compiler with a complete machine-checked proof of semantic preservation from C to assembly [Leroy 2009]. We present here an extension of Compcert for AArch64 processors, that optimizes the use of the pipeline in the processor (postpass scheduling) and performs instruction compaction (e.g. replaces pairs of simple load instructions, by single double load instructions), through a technique called peephole optimization. Our method is founded on a two-tier design, introducing an untrusted oracle performing the translation, and a formally-verified checker testing whether the code produced by the oracle simulates the original code. We reuse here the generic checker, based on symbolic execution with an hash-consing mechanism, of [Six et al. 2020]. The paper presents the proof schema for establishing the correctness of my optimizations, and experimental measurements of performance improvements. More generally, my thesis aims to explore how to apply and generalize such mechanisms of translation validation in order to extend Compcert with target-dependent optimizations.
• 10:00 - 10:30 Vincent Iampietro, David Andreu et David Delahaye. Vers la vérification d’une méthodologie pour la conception de circuits numériques critiques [Résumé PDF]
  La méthodologie HILECOP décrit un processus d'aide à la conception de systèmes numériques critiques. Dans HILECOP, les réseaux de Petri (RdP) servent, en tant que formalisme de haut-niveau, à la spécification du comportement des systèmes conçus. Du code VHDL est ensuite généré automatiquement depuis les modèles à réseaux de Petri; ce code permet la synthèse du système numérique sur carte programmable FPGA. Le but de notre travail est de formellement vérifier qu'à travers cette transformation modèle vers texte, le comportement décrit dans le modèle initial est préservé dans le code généré. La preuve de préservation sémantique sera conduite avec l'assistant à la preuve Coq. Nous présentons ici l'état d'avancement de ce travail; notamment, nous présentons nos efforts quant à la formalisation et l'implémentation des sémantiques des modèles de haut-niveau (RdP) et du langage cible (VHDL).
• 10:30 - 11:00 Abdelhak Khemiri, Aznam Yacoub et Maamar El Amine Hamri. Vérification formelle d'un réseau sur puce : Application de DEv-Promela [Résumé PDF]
  Dans ce papier, nous présentons une approche pour vérifier et valider des systèmes dynamiques complexes qui reposent à la fois sur une vérification formelle des propriétés temporelles exprimées et une simulation (tester un scénario, quantifier des variables ou aider à la prise de décision) de la dynamique du système modélisé. En effet, nous montrons qu'il est possible de combiner un vérificateur et une simulation pour tirer les avantages et combler mutuellement les inconvénients de chacun. Nous nous appuyons sur le langage DEv-PROMELA qui lui repose sur deux formalismes développés par deux communautés différentes : PROMELA pour vérifier formellement des systèmes asynchrones et DEVS pour modéliser et simuler des systèmes dynamiques. Enfin, une étude de cas décrivant un réseau sur une puce électronique est présentée et les résultats obtenus sont analysés et commentés.

• 13:30 - 14:00 Baptiste Pollien. Vérification d'une bibliothèque mathématique d'un autopilote avec Frama-C [Résumé PDF]
  Lors du développement de système critique, comme un autopilote de drone, il est essentiel de s'assurer que le programme est sûr, en utilisant par exemple des méthodes formelles. Pour faciliter la vérification, on se restreint généralement à une abstraction du système ou un sous-ensemble. Cet article présente la vérification d'une bibliothèque mathématique de l'autopilote Paparazzi, à l'aide de l'outil Frama-C, afin de garantir l'absence d'erreur à l'exécution et certaines propriétés fonctionnelles.
• 14:00 - 14:30 William Weens, Thibaud Vazquez-Gonzalez et Louise Ben Salem-Knapp. La double précision suffit-elle à l'exascale ? [Résumé PDF]
  La croissance des capacités de calcul des machines permet d'obtenir des résultats de simulation de plus en plus précis. Ces résultats sont souvent calculés en binary64 (double précision) avec l'idée que les erreurs d'arrondi ne sont pas significatives. Or, l'exascale permet d'augmenter le nombre d'opérations et des problèmes d'accumulation d'erreurs d'arrondi pourraient apparaître. Augmenter la précision des nombres flottants pour remédier à ce problème n'est pas envisageable car le surcoût en mémoire, en temps de calcul et en énergie ferait perdre une partie importante des performances des nouvelles machines. Il est donc important de mesurer la robustesse du binary64 en anticipant les ressources de calcul à venir afin d'assurer la pérennité de celle-ci dans les simulations numériques. C'est dans ce but que des expériences numériques ont été réalisées et sont présentées dans cet article. En montrant que les erreurs d'arrondi restent dominées par les erreurs du schéma, les résultats ont permis de valider le binary64 dans ces simulations.
• 14h30 - 15:00 Alexis Maffart et Xavier Thirioux. Taylor series revisited [Résumé PDF]
  We propose a renovated approach around the use of Taylor expansions to provide polynomial approximations. We introduce a coinductive type scheme and finely-tuned operations that altogether constitute an algebra, where our multivariate Taylor expansions are first-class objects. As for applications, beyond providing classical expansions of integro-differential and algebraic expressions mixed with elementary functions, we demonstrate that solving ODE and PDE in a direct way, without external solvers, is also possible. We also discuss the possibility of computing certifed errors within our scheme.
• 15:00 Mot de la fin des présidents de ces journées