Programmé en UVF2RMRIR404
Présentation :
Responsable : Thomas Jensen (jensen@irisa.fr)
Équipe pédagogique : Éric Filiol, Thomas Jensen, David Pichardie
L'objectif du cours est d'enseigner les notions fondamentales de l'analyse statique de programmes (sémantique opérationnelle, interprétation abstraite, systèmes de types) et de montrer comment ces techniques sont utilisées pour améliorer la sécurité des logiciels embarqués (byte code Java, C, etc.). À la fin du cours, l'étudiant sera capable d'écrire une sémantique opérationnelle d'un langage de programmation et de définir un système de types et des analyses statiques pour ce langage d'une manière systématique, en s'appuyant sur la théorie de l'interprétation abstraite. La deuxième partie du cours sera dédiée à l'utilisation d'analyse statique pour sécuriser les programmes byte code Java (vérification de type du byte code, analyse de flux d'information) ainsi qu'à la détection de virus et à la virologie informatique.
Pré-requis :
Cours de compilation, connaissances souhaitables en sémantique opérationnelle.
Liens :
http://master.irisa.fr/master/live/modules/p3m3_fr.html
Volume horaire :
20h
Contenu détaillé :
-- Sémantique opérationnelle (2h)
sémantique opérationnelle à petit pas et sémantique naturelle pour un simple langage impératif et pour le lambda calcul ; équivalence sémantique ; sémantique du byte code Java.
-- Interprétation abstraite (6h)
analyse de flot de données (variables vivantes, expressions disponibles) ; théorie de treillis (connexions de Galois, calcul de points fixes) ; conception d’interprétations abstraites pour un langage impératif ; analyse relationnelle (polyèdres, octogones) ; analyse inter-procédurale ; analyse d’alias.
-- Systèmes de types (2h)
lambda calcul simplement typé ; polymorphisme ; invariance et correction par typage, inférence de type ; unification.
-- Sécurité logicielle (10h)
vérification du byte code Java ; analyse de flux d’information et canaux cachés ; attaques basées sur l’obfuscation de types ; détection de virus et virologie informatique
Année 2019/2020
Dernière mise à jour le 11-JAN-19
Validation par le responsable de programme le
| 
