MTV2 2022
Journée MTV2 du 17 Mars 2022
Télécom SudParis à Palaiseau, Amphi 2
Adresse : 19 place Marguerite Perey, 91120 Palaiseau
Programme de la journée
Les exposés pourront se faire en français ou en anglais.
La durée d’un exposé régulier est de 20min+10min questions-réponses.
La durée d’un exposé invité est de 60min+15min questions-réponses.
10:00-10:30 Accueil, Café, Ouverture de la journée - Nikolai Kosmatov, Natalia Kushik, Pascale Le Gall, Antoine Rollet
10:30-12:00 Session 1.
10:30-11:00 Fine-Grained Coverage-Based Fuzzing - Bernard Nongpoh - CEA LIST
11:00-11:30 Modèles pour le test d'applications mobiles sensibles au contexte - Ioannis Parissis - INP-UGA
11:30-12:00 A small-step approach to multi-trace checking against interactions - Erwan Mahe - CEA LIST
12:00-14:00 Pause déjeuner
14:00-15:15 Session 2. Exposé invité.
14:00-15:15 Rétro-ingénierie de modèles par et pour le test - Roland Groz - Grenoble INP
15:15-15:45 Pause café
15:45-16:45 Session 3.
15:45-16:15 Verifying Redundant-Check Based Countermeasures: A Case Study - Thibault Martin - CEA LIST
16:15-16.45 Tests Aléatoires Automatisés pour les Types Contraints - Ghiles Ziat - IRIF
16.45-17:00 Annonces, discussions, fin de journée - Nikolai Kosmatov, Natalia Kushik, Pascale Le Gall, Antoine Rollet
Résumés
Rétro-ingénierie de modèles par et pour le test (Roland Groz - Grenoble INP) - Exposé invité
Les approches à base de modèles permettent d'automatiser des techniques de V&V avec un certain niveau de garantie sur la qualité de la validation. Mais les modèles sont rarement disponibles dans les développements logiciels, l'IDM restant confinée à certaines niches de développement (systèmes critiques, embarqués...).
Des modèles peuvent toutefois être reconstruits à partir de logiciels par des techniques d'apprentissage, lesquelles consistent à observer les réactions d'un système. Elles s'apparentent donc à des formes de test à des fins de reconstituer des modèles de comportement.
Cet exposé présentera des approches de rétro-conception de modèles par des techniques d'apprentissage, en particulier celles qui sont mises en œuvre dans des approches de V&V. Après une présentation globale, on s'intéressera plus particulièrement au problème de rétro-conception de modèle pour des systèmes qui ne peuvent être réinitialisés. On verra qu'il est possible d'inférer de façon assez efficace des modèles en repartant d'éléments classiques du test de conformité.
Enfin, on évoquera des recherches en cours pour relier la rétro-ingénierie active (on a accès au système et on peut le tester) et passive (utilisant des traces enregistrées de l'exploitation du logiciel).
Fine-Grained Coverage-Based Fuzzing (Bernard Nongpoh - CEA LIST)
Fuzzing is an effective software testing method that discovers bugs by feeding target applications with (usually a massive amount of) automatically generated inputs. Many state-of-art fuzzers use branch coverage as a feedback metric to guide the fuzzing process. The fuzzer retains inputs for further mutation only if branch coverage is increased. However, branch coverage only provides a shallow sampling of program behaviours and hence may discard inputs that might be interesting to mutate. This talk discusses our ongoing work aiming to take advantage of the large body of research over defining finer-grained code coverage metrics (such as mutation coverage) and use these metrics as better proxies to select interesting input for mutation. We propose to make coverage-based fuzzers support most fine-grained coverage metrics out of the box (i.e., without changing fuzzer internals). We achieve this by making the test objectives defined by these metrics (such as mutants to kill) explicit as new branches in the target program. Fuzzing such a modified target is equivalent to fuzzing the original target, but the fuzzer will also retain inputs covering the additional metrics objectives for mutation. Our preliminary experiment shows significantly positive results on one application of the LAVA-M benchmark suite and marginally negative ones on the three others.
Verifying Redundant-Check Based Countermeasures: A Case Study (Thibault Martin - CEA LIST)
To thwart fault injection based attacks on critical embedded systems, designers of sensitive software use redundancy based countermeasure schemes. In some of these schemes, critical checks (i.e. conditionals) in the code are duplicated to ensure that an attacker cannot bypass such a check by flipping its result in order to get to a protected point (corresponding e.g. to a successful authentication or code integrity verification). This talk presents a source-code-level verification technique of the correct implementation of such countermeasures. It is based on code instrumentation and deductive verification. The proposed technique was implemented in a tool prototype and evaluated on a real-life case study: the bootloader module of a secure USB storage device called WooKey, supposed to be resistant to fault injection attacks. We were able to prove the correctness of almost all redundant-check countermeasures in the module except two, and found an error in one of the unproven ones. This is a joint work with Nikolai Kosmatov and Virgile Prevosto.
Modèles pour le test d'applications mobiles sensibles au contexte (Ioannis Parissis - INP-UGA)
Équipés de capteurs sophistiqués et d'une énorme puissance de calcul, les appareils mobiles modernes, tels que les smartphones, sont désormais capables de détecter leur environnement. En conséquence, les applications mobiles intègrent de plus en plus de fonctionnalités dont le comportement dépend non seulement de la saisie explicite de l'utilisateur, mais également de l'état de l'environnement (ou contexte). Nous présentons nos travaux en cours sur le test des applications mobiles sensibles au contxete. Premièrement, nous présentons une approche pour générer automatiquement des cas de test dépendant du contexte à partir d'une combinaison de modèles comportementaux (machines d'états finis hiérarchiques) et contextuels écrits dans des langages spécifiques au domaine. Cette approche inclut également des critères de couverture du contexte par la suite de tests générés. Ces travaux ont fait l'objet du stage de Master d'Abdellah Adwan, soutenu en juin 2021. Ensuite, dans le cadre de la thèse en cours de Le Thi Thanh Binh, nous étudions une approche combinant deux autres modèles : un "Bigraphical Reaction System" et un "Dynamic feature Petri net" pour la génération automatique de cas de test. Ces travaux font l'objet d'une collaboration entre le laboratoire LCIS et l'université de Danang et bénéficient d'un soutien de l'IDEX UGA et de la Région Auvergne Rhône Alpes.
Tests Aléatoires Automatisés pour les Types Contraints (Ghiles Ziat - IRIF)
Il est fréquent de manipuler des valeurs numériques avec des contraintes non explicitées par leurs types. Par exemple, les intervalles d'entier sont des couples de nombres avec la contraintes que le premier (la borne inférieure) soit plus petit que le deuxième (borne supérieure). Nos travaux proposent de générer automatiquement des tests unitaires à partir de la définition de ce genre de types. Nous présenterons des exemples en OCaml. Pour générer des tests automatiquement à partir d'un type: nous dérivons les contraintes le concernant, calculons, à l'aide de programmation par contrainte, une représentation de l'espace des habitants de ce type et enfin, nous générons le code du test qui générera aléatoirement et uniformément des intervalles. Notre méthode est implémentée dans un prototype de pré-processeur pour OCaml appelé Testify. Nous étendons notre méthode aux types récursifs en mixant de la génération de structures de données inductive à l'aide de la méthode de Boltzmann et la génération en domaines finis uniformément distribué en utilisant des contraintes globales., notre cadre Nous utilisons clp(fd) de SICStus Prolog comme bibliothèque de contraintes et la bibliothèque Arbogen en tant que générateur aléatoire de structures arborescentes.
A small-step approach to multi-trace checking against interactions (Erwan Mahe - CEA LIST)
Interaction models describe the exchange of messages between the different components of distributed systems. This paper presents an approach for checking the validity of multi-traces against interaction models. A multi-trace is a collection of traces (sequences of emissions and receptions), each representing a local view of the same global execution of the distributed system. We formally prove our approach, study its complexity, and implement it in a prototype tool.