SAFER: Safety and Security Analyses via Formal and Efficient veRification

Responsable : Kaïs Klai

Les systèmes développés de nos jours sont de plus en plus complexes et leur fonctionnement peut avoir des conséquences importantes sur leur environnement, voire irréversibles : systèmes avioniques, médicaux… Il est par conséquent indispensable de garantir des systèmes sûrs, dont le fonctionnement a pu être vérifié avant leur mise en oeuvre. L’écriture d’une spécification formelle permet non seulement une meilleure compréhension du système étudié, mais aussi de prouver formellement, par une vérification exhaustive, son bon fonctionnement, quelle que soit l’exécution du système.

Nos activités s’articulent autour de trois principales thématiques de recherche :

– Conception de spécifications formelles: Le développement des spécifications est une tâche délicate, et il est facile de faire des erreurs. Le cadre des spécifications formelles oblige à une meilleure précision, et est ici sous-jacent aux travaux qui choisissent une expression en diagrammes UML.

– Vérification paramétrée, modulaire et distribuée :
La conception de nouvelles techniques de vérification permettant de combattre le problème de l’explosion combinatoire constitue un axe majeur de nos recherches.

– Sûreté et sécurité logicielles :
L’analyse de programmes concurrents est encore balbutiante. Nous étudions différents formalismes pour modéliser les programmes récursifs parallèles, et des techniques d’analyse associées. Nous développons aussi différents modèles pour la détection de malware et la découverte de comportements malveillants.

Consulter le rapport d’équipe 2017-2022 pour des informations plus détaillées.