Analyse avancée de la sécurité et preuve de programmes

📋 Plan du Cours

1. Analyse de liveness et élimination de code mort (DCE)
2. Analyse d'initialisation des variables en Java et méthodes en avant et en arrière
3. Analyse avancée DCE avec graphes de contrôle de flux (CFG) et itérations
4. Interprétation abstraite du domaine des pointeurs et gestion des assertions nullité
5. Preuve de programmes avec WP et spécifications ACSL en C
6. Vulnérabilités classiques en C : débordements, comportements indéfinis et corrections
7. Principales injections (commande, SQL, XSS, SMTP, path traversal) et leurs protections
8. Attaques par débordement de buffer et protections de la pile (canari, ASLR, DEP, shadow stack)
9. Use-after-free, variables non initialisées et principe de moindre privilège
10. Utilisation des plugins Frama-C EVA et WP pour analyse statique et preuve
11. Points clés pour l'examen 2025 : exercices types, pièges fréquents et bonnes pratiques
12. TP sécurité C et WP Frama-C : exercices pratiques et méthodologie

📖 1. Analyse de liveness et élimination de code mort (DCE)

🔑 Notions clés & Définitions

• Invariant : Un invariant est un ensemble stable obtenu par itérations successives dans l'analyse de liveness d'une boucle, représentant les variables live à chaque point du corps de la boucle.
• Affectation morte : Si x ∉ Lo : `L

📝 Points essentiels