Analyse de Code pour la Sûreté et la Sécurité - ISI 2A - 2025-2026

Actualités

• 30 Apr corrigé du TD5 (Analyse d’intervalles)
• 1 Apr fixe une typo dans diapo 34 du CM3: les “live-out” sur les lignes 2 à 4 étaient décalés.
• 26 Mar En complément du TD6, voir cette introduction aux scripts shell sécurisés qui présente aussi l’outil ShellCheck.
• Tony Hoare — l’inventeur de la logique à son nom qui est étudiée dans ce cours — est décédé le 5 mars dernier, à Cambridge (UK), à l’âge de 92 ans.
• 13 Mar corrigé du TD4 (Analyse des pointeurs nuls)
• 27 Fév pour préparer le TP Frama-C, corrigé du TD3 (Preuve formelle)
• 26 Fév plusieurs corrections de typo dans les diapos sur logique de Hoare et Frama-C (concepts de base) 1up|4up|animations

Intervenants

• Responsable: Sylvain Boulmé
• CM: Sylvain Boulmé et Marie-Laure Potet
• TD G1: Damien Couroussé
• TD G2: Xavier Nicollin
• TD G3: Sylvain Boulmé
• Grand architecte: Marie-Laure Potet (2018-2025).

Plan des séances

• semaine 1:
  • demi-CM introduction à ACSS 1up|4up|animations
  • avec démo RTE sur signed_binary_search
  • demi-CM logique de Hoare et Frama-C (concepts de base) 1up|4up|animations
  • TD Sémantiques des langages de prog
• semaine 2:
  • CM logique de Hoare et Frama-C (commandes gardées jusqu’à la règle du while)
  • TD Preuve d’absence de RTE
• semaine 3:
  • CM logique de Hoare et Frama-C (fin)
  • avec démo WP Frama-C sur spec complète de signed_binary_search
  • TD Preuve formelle
• semaine 4:
  • TP Frama-C (3h): instructions du TP et fichiers fournis.
  • Un complément pas indispensable, utile seulement si vous n’êtes pas à l’aise: tutoriel informel (mais en anglais) au plugin WP de Frama-C.
• semaine 5:
  • CM interprétation abstraite et analyse flot de données (jusqu’à théorie des treillis incluse) 1up|4up|animations
  • TD Analyse des pointeurs nuls
• semaine 6:
  • CM interprétation abstraite et analyse flot de données (fin)
  • avec démos EVA sur binary_search et pointeurs_eva.
  • TD Analyse d’intervalles
• semaine 7:
  • CM écrire du code sécurisé avec les diapos du RTE-free X.509 parser
  • TD Failles de sécurité
• semaine 8:
  • TP intro à la sécurisation du code C (3h): sujet et sources fournies
  • TD analyse de liveness, d’initialisation, et élimination de code inutile
• semaine 9:
  • CM désassemblage et reverse: reverse, un exemple crakme, exécution symbolique.
  • TP Reverse et exploitation d’un buffer overflow (1h30): sujet et sources fournies
• semaine 10:
  • CM sécurité et langages de programmation: Propriétés de langages de programmation et Java une plateforme sécurisée.
  • TP Recherche de vulnérabilités avec KLEE (1h30): sujet et sources fournies avec les diapos sur les outils pour tester du code
• semaine 11 :
  • TD propriété des langages pour la sûreté et la sécurité

Annales des examens

Voir la page du cours sur Chamilo.

Quelques autres outils d’analyse statique open-source pour sécuriser votre code

• ShellCheck pour la sécurisation des scripts bash/sh. L’analyseur est écrit principalement en Haskell.
• Pyre et Pysa pour la sécurisation des scripts Python, notamment les serveurs web - via de l’analyse de teinte. Principalement écrit en OCaml.
• MOPSA un analyseur encore expérimental, basé sur de l’interprétation abstraite, pour analyser des programmes combinant du C et du Python. Principalement écrit en OCaml.