Interventions invitées
Delphine Longuet est ingénieure de recherche en méthodes formelles au sein de Thales cortAIx Labs. Elle a obtenu son doctorat à l’Université d’Évry-Val-d’Essonne en 2007. Elle a ensuite été maîtresse de conférences à l’Université Paris-Sud pendant neuf ans, avant de rejoindre Thales en 2018. Ses travaux de recherche portent sur les méthodes formelles appliquées à la validation et à la vérification des logiciels. Chez Thales, elle a codirigé deux projets consacrés à la génération automatique de tests, l’un pour le langage Ada en partenariat avec AdaCore, et l’autre pour le langage C en partenariat avec OCamlPro. Ces projets visent à favoriser l’adoption industrielle de ces techniques et de ces outils.
Vers l’adoption industrielle des techniques automatisées de génération de tests avec SeaCoral
Les méthodes formelles ont permis de développer avec succès des techniques avancées de génération automatique de tests et de détection de vulnérabilités. Toutefois, leur adoption dans les pratiques industrielles demeure encore fragmentée. Dans cette présentation, je présenterai SeaCoral, une nouvelle boîte à outils open source dédiée au test de programmes C, dont l’objectif est de faciliter l’application industrielle de divers outils de test et d’analyse en les intégrant au sein d’un cadre unifié et en les faisant collaborer. Je présenterai les différents outils intégrés et expliquerai comment SeaCoral les fait travailler conjointement sur un même code afin de générer des tests maximisant un critère donné de couverture de code. Au-delà de la génération de tests de couverture, une attention particulière est portée à la détection des erreurs à l’exécution (runtime errors), considérées comme des sources potentielles de vulnérabilités, ainsi qu’à leur reproductibilité.
Langue : Anglais (sous-titré en français)
Antoine Delignat-Lavaud est chercheur en sécurité au sein de l'équipe Confidential Computing d'Azure Research. Il conçoit des protocoles, des services de plateforme et des architectures matérielles permettant de bâtir un cloud garantissant la confidentialité et l'intégrité des données sensibles tout au long de leur cycle de vie. Il pilote notamment le développement d'offres d'IA confidentielle assurant la confidentialité vérifiable des modèles, des prompts et des réponses.
Les défis concrets du passage à l'échelle de l'informatique confidentielle dans Azure
L'exploitation de services d'informatique confidentielle soulève des défis qui dépassent la sécurité traditionnelle du cloud. Les clients doivent pouvoir vérifier non seulement l'identité d'un service, mais aussi son implémentation attestée. À grande échelle, la gestion des preuves d'attestation, des mises à jour et des dépendances entre services complexifie la chaîne de confiance. De plus, l'attestation doit être complétée par des garanties sur la construction des logiciels, tandis que les attaques par canaux auxiliaires rappellent les limites des environnements d'exécution de confiance (TEE). Cette présentation montrera les protocoles, les services et l'architecture développés par Azure pour rendre l'informatique confidentielle utilisable à grande échelle dans des environnements réels.
Langue : Anglais (sous-titré en français)