Analyse de Code pour la Sûreté, la Compilation et la Sécurité - 4MMACSCS

Objectif(s)

Ce cours introduit les méthodes formelles d'analyse de code (vérification déductive, interprétation abstraite, exécution symbolique) et leurs applications en sûreté de fonctionnement, optimisation de code à la compilation (à middle-end), et sécurité du logiciel (en incluant les techniques de test et de reverse). Plusieurs TPs accompagnent ce cours (preuves de programme, attaques et techniques de sécurisation du code, reverse et attaque par buffer overflow) avec la prise en main d'outils de l'état de l'art (plugins WP et EVA de Frama-C, Klee, Ghidra, etc). L'originalité du cours est de présenter un cadre théorique unifié pour la vérification et l'analyse de programmes.

Responsable(s)

Sylvain BOULME

Contenu(s)

• Sémantique comparée de langages de programmation (C, Java, Rust, etc).
• Formalisation de la sémantique axiomatique et de la vérification déductive de programmes (logique de Floyd-Hoare-Dijkstra).
• Théorie des techniques d'interprétations abstraites et d'analyses flot de donnée.
• Exemples des analyses de valeurs, de variables vivantes, de bonne initialisation et d'analyses de teintes.
• Application à la sûreté de fonctionnement des systèmes critiques
• Application aux optimisations de compilation middle-end (e.g. propagation de constantes, éliminations de code inutile)
• Sécurité des applications : attaques, exploitabilité et protections
• Outils pour le pentest (tests de pénétration).

• connaissance du C et d'un assembleur.
• théorie des langages (langages réguliers, grammaires hors-contextes, grammaires attribuées).
• notions de calculabilité (théorème de l'arrêt, théorème de Rice).
• notions en compilation (analyse syntaxique, arbres de syntaxe abstraite, traduction dirigée par la syntaxe).
• implémentation (partielle) d'un compilateur (e.g. en "projet GL").
• notions en logique des prédicats du 1er ordre (notions de modèle et de système d'inférence).
• la connaissance de Java et de Rust est un plus - mais ne sont pas des pré-requis.

Contrôle des connaissances

Evaluation : Examen écrit (2h)

Rattrapage : Examen écrit (2h)

Examens écrits de 2h.
Documents autorisés: 1 feuille A4 recto-verso (manuscrite ou non)

Calendrier

Le cours est programmé dans ces filières :

• Cursus ingénieur - Tronc Commun - Semestre 8

Informations complémentaires

Code de l'enseignement : 4MMACSCS
Langue(s) d'enseignement :

Vous pouvez retrouver ce cours dans la liste de tous les cours.