Dans le cadre de notre séminaire « La Cybersécurité sur un plateau » (Cybersecurity on a Plate), nous aurons 2 présentations le mardi 09 décembre prochain. Le séminaire CoaP aura lieu à 10h30 dans le bâtiment IMT/TP/TSP, en salle 3.A213.

Si vous venez participer pour la première fois, n'hésitez pas à contacter les organisateurs pour ne pas être bloqué à l'entrée.

Virgile Prevosto (CEA LIST): Preuve d'intégrité avec Frama-C/MetAcsl

Abstract: Frama-C est un outil d'analyse de programmes C, muni d'un langage de spécifications formelles ACSL, dans lequel l'utilisateur peut décrire les propriétés attendues du code, principalement sous la forme de contrats de fonction et d'assertions logiques. Ce type d'annotations est bien adapté pour décrire des propriétés fonctionnelles du programme, c'est à dire intuitivement que le programme calcule bien ce qu'on attend de lui. En revanche, d'autres classes de propriétés sont difficilement exprimables en ACSL, exigeant un encodage complexe et donc source potentielle d'erreur dans la spécification elle-même. C'est typiquement le cas pour des propriétés de sécurité comme l'intégrité ou la confidentialité du contenu de locations mémoire du programme, qui demanderaient en théorie d'ajouter des assertions pour chaque accès en écriture (respectivement en lecture), ce qui devient rapidement rédhibitoire, même sur un code de taille modeste.

Le greffon MetAcsl de Frama-C a été développé par Virgile Robles dans le cadre de sa thèse pour répondre à ce problème. Plus précisément, MetAcsl permet de définir dans un langage dédié des HILAREs (High-Level ACSL Requirements), propriétés destinées à être instanciées automatiquement en annotations ACSL à chaque point du programme correspondant au contexte de l'HILARE (par exemple chaque accès en écriture/en lecture). En outre, MetAcsl permet aussi dans certains cas de raisonner directement au niveau des HILAREs. Une telle étape de "méta-déduction" permet de valider une HILARE en fonction de celles précédemment prouvées, évitant ainsi de devoir prouver séparément toutes ses instances au niveau ACSL.

Dans cet exposé, nous présenterons les principales constructions des HILAREs ainsi que les mécanismes de validation, par preuve directe des annotations ACSL générées via le greffon WP et par méta-déduction au sein de MetAcsl, à travers une étude de cas visant à établir l'intégrité de l'automate qui supervise le déroulement du bootloader de WooKey, un prototype de clé USB sécurisée développée par l'ANSSI.

Bio: Virgile Prevosto est Ingénieur Chercheur au laboratoire de sûreté et sécurité des logiciels du CEA List, expert senior en méthodes formelles. Il est un des principaux développeurs de la plateforme d'analyse de programmes Frama-C.

Benoit NOUGNANKE: How Dataset Diversity Affects Generalization in ML-based NIDS

Abstract: Machine Learning-based Network Intrusion Detection Systems (ML-based NIDS) rely heavily on the quality of the datasets used for training and evaluation. However, widely used NIDS benchmarks often suffer from poor data diversity, which limits model generalization and undermines the reliability of evaluation protocols. While prior work has acknowledged this limitation, a systematic framework to quantify dataset diversity and analyze its relationship with performance is still missing. To address this gap, we introduce a structured approach for characterizing dataset diversity in ML-based NIDS, grounded in measurement theory. We distinguish three types of diversity—intra-class, inter-class, and domain-shift—and operationalize their measurement using established metrics such as the Vendi Score and the Jensen-Shannon divergence. Our empirical analysis on the CIC-IDS2018 dataset, spanning sixty diversity-controlled train–test experiments, provides new insights into the relationship between diversity and generalization and demonstrates the value of diversity-aware data sampling for improving evaluation reliability.