La XXIX° édition des journées FAC aura lieu les 3 et 4 avril 2024 au LAAS-CNRS.

Inscriptions

La participation aux journées est gratuite.

Afin de pouvoir dimensionner correctement les pauses-café et les repas, il est demandé de s’inscrire au plus tard le 25 mars via le formulaire suivant.

https://www.laas.fr/registration/fac2024

Conférenciers invités

Cette année nos conférenciers invités sont:

• Caterina Urban (INRIA Paris, équipe ANTIQUE et ENS): Machine Learning Interpretability and Verification

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This brings forth important challenges related to safety, privacy, and non-discrimination. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is predominantly carried out in the ML community, while research in ML verification is almost exclusively carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by highlighting the synergies between interpretability and verification in ML software. We will survey our recent and ongoing work, and discuss research questions and avenues for future work in this context.

• Laurent Mounier (Vérimag, Univ. Grenoble): Vérification formelle pour la détection et l’analyse de vulnérabilités logicielles

La place prépondérante prise par les technologies du numérique dans notre quotidien s’accompagne d’une augmentation croissante - en nombre et en degré de sophistication - des cyberattaques auxquelles nous devons faire face. L’une des causes de ces attaques réside dans des erreurs de conception et/ou de développement des logiciels que nous utilisons, des systèmes d’exploitation aux logiciels applicatifs. Détecter et analyser la dangerosité de ces vulnérabilités est donc un enjeu majeur pour les développeurs/intégrateurs de logiciels, pour les organismes de certification et pour la mise en place de correctifs et mécanismes de protections adéquats.

Pour cela il est nécessaire de disposer d’outils permettant d’automatiser certaines analyses de code spécifiques à la sécurité. Nous présenterons comment l’utilisation de techniques de vérification formelle dédiées permet de répondre à ce besoin en l’illustrant notamment à travers deux exemples d’attaques “avancées”, les attaques par injection de fautes et les attaques dites adaptatives.

Programme

Programme disponible rapidement

Comité de programme

Jean-Paul Bodeveix, Julien Brunel, Silvano Dal Zilio, Mamoun Filali, Christophe Garion, Didier Le Botlan, Iulian Ober, Marc Pantel, Célia Picard, Philippe Quéinnec, Jean-Baptiste Raclet, Pierre Roux, Matthieu Roy, Pascal Sotin.