Programme
Les actes d'AFADL 2020 sont disponibles
ici.
Les actes d'AFADL 2021 sont disponibles
ici.
Dans le programme ci-dessous, vous trouverez des pointeurs vers tous les
articles AFADL présentés cette année.
16 juin 2021
Session 1 — Session commune avec le GT LVP
Président de session : Julien Signoles
17 juin 2021
Session 2
Président de session : Yves Ledru
- 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.
Session 3 — Session commune avec le GT MTV2
Président de session : Antoine Rollet
- 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
18 juin 2021
Session 4
Présidente de session : Sandrine Blazy
- 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.
Session 5
Président de session : David Monniaux
- 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