Vérification de modèles — VER (campus UBS, Vannes)

Model checking

Description

Les objectifs du module sont (1) d'apprendre à utiliser les automates comme représentation mathématique d'un système ou d'une propriété, (2) d'introduire les méthodes de vérification formelles qui utilisent la théorie des automates, (3) d'utiliser des outils qui implémentent ces méthodes.

Mots-clés

Vérification de modèles (Model checking), Propriétés de cybersécurité

Pré-requis

Des connaissances des mathématiques de base, principalement de l'algèbre, de la logique Booléenne et de la théorie des automates à états finis, mots finis et infinis

Références biblio pour obtenir les pré-requis

von J.E. Hopcroft, R. Motwani, .J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison Wesley.

Modules allant naturellement avec ce cours

ARC, SEC, SES

Contenu

Partie 1: Modélisation d'un système informatique au moyen d'un système de transitions.
- Introduction à la concurrence et à sa modélisation par des contraintes sur des automates.
- Présentation d'algorithmes qui utilisent la théorie des automates pour la vérification formelle de propriétés décrites en LTL.
- Application à la vérification de propriétés de sécurité, plus particulièrement à la vérification de propriétés de sécurité de protocoles cryptographiques,
Partie 2: Introduction à l'analyse symbolique par SAT-solvers.
- Utilisation des logiciels Klee et American fuzzy lop pour la détection de vulnérabilités.

Compétences acquises

Savoir :
- Modélisation de logiciel au moyen de représentation mathématique.
- Bases de la vérification formelle par le model checking.
Savoir-faire :
- Mise en pratique des algorithmes fondamentaux du model checking.
- La mise en application d'outils de vérification par le model checking.
- Le lien entre le model checking et la validation de propriétés liées à la cybersécurité.

Références

JP. Katoen, C. Baier, Principles of Model Checking, MIT Press.
P. Bieber, J. Cazin, P. Girard, J-L. Lanet, V. Wiels, G. Zanon, Checking Secure Interactions of Smart Card Applets, extended version, Journal of Computer Security, Vol. 10, N°4, 2002, pp. 369-398.
E. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press.
P. Wolper, Introduction à la calculabilité, Dunod.

Notions ou résultats marquants du cours

Vérification des propriétés de cybersécurité au moyen du model checking

Modalité d'évaluation

Contrôle continu (activités pratiques et exercices de recherche, présentations d'articles et devoirs)

Enseignant

Axel Legay