Université du Québec en Outaouais Département d'informatique et d'ingénierie
Sigle : INF6233  Gr. 01
Titre : Sécurité informatique et méthodes formelles
Session : Automne 2016  Horaire et local
Professeur : Adi, Kamel
1. Description du cours paraissant à l'annuaire :

Objectifs

Permettre aux étudiants de maîtriser les techniques formelles utilisées pour la sécurisation des systèmes et réseaux informatiques.

Contenu

Problèmes de la sécurité dans les logiciels et intergiciel. Formalismes algébriques et logiques pour la description des systèmes et des politiques de sécurité. Automates d’édition. Techniques formelles de renforcement de politiques de sécurité dans les systèmes. Renforcement par Monitorage. Renforcement par réécriture de programmes. Classes de propriétés de sécurités : sûreté, vivacité, « renewal », etc.
2. Objectifs spécifiques du cours :
Dans ce cours, nous présenterons les techniques formelles couramment utilisées pour assurer la sécurité des systèmes informatiques. En particulier, le cours aborde les formalismes de spécification et les techniques de vérification et de renforcement de politiques de sécurité dans les systèmes informatiques : algèbre de processus, CCS/CSP, logique temporelle, "model-checking", systèmes d'inférences, systèmes de réécriture, etc.
3. Stratégies pédagogiques :
Ce cours est donné principalement sous forme magistrale, parsemé d’exercices de compréhension.
4. Heures de disponibilité ou modalités pour rendez-vous :
Sur rendez-vous.
5. Plan détaillé du cours sur 15 semaines :
Semaine Thèmes Dates
1    Introduction aux méthodes formelles. 07 sept. 2016 
2    Analyse statique
  • Algèbres de processus.
  • Calculus for Communicating Systems (CCS).
 14 sept. 2016 
3    Analyse statique
  • Calculus for Communicating Systems (CCS).
 21 sept. 2016 
4    Analyse statique
  • Formalismes Logiques.
  • Mu calcul modal.
  • Linear Temporal Logic (LTL).
28 sept. 2016 
5    Analyse statique
  • Évaluation de modèles.
  • Automates de Büchi.
  • Edinburgh Concurrency Workbench.
 05 oct. 2016 
6    Semaine d'études. 12 oct. 2016 
7    Examen intra. 19 oct. 2016 
8    Analyse dynamique
  • Techniques de monitorages.
 26 oct. 2016 
9    Analyse dynamique
  • Automates d'édition.
 02 nov. 2016 
10    Systèmes de réécriture. 09 nov. 2016 
11    Renforcement de politiques de sécurité par réécriture. 16 nov. 2016 
12    Renforcement de politiques de sécurité par réécriture. 23 nov. 2016 
13    Présentation des projets. 30 nov. 2016 
14    Présentation des projets. Révision pour l'examen final. 07 déc. 2016 
15    Examen final. 14 déc. 2016 
6. Évaluation du cours :
  • Examen de mi-session : 30 %
  • Examen final : 40 %
  • Projet : 30%
7. Politiques départementales et institutionnelles :
8. Principales références :
  • Robin Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science, 1995, ISBN : 0131150073.
  • Colin Stirling. Modal and Temporal Properties of Processes. Springer, 2001, ISBN :0-387-98717-7
  • K. Adi. Thèse de doctorat
  • N. Sui, M. Mejri, H. Ben Sta. FASER (Formal and Automatic Security Enforcement by Rewriting): An algebraic approach. Computational Intelligence for Security and Defence Applications(CISDA), 2012 IEEE Symposium.
  • Hakima Ould-Slimane, Mohamed Mejri, Kamel Adi. Using Edit Automata for Rewriting-Based Security Enforcement. DBSec 2009: 175-190
  • K. Adi, M. Debbabi, and M. Mejri. A New Logic for Electronic Commerce Protocols .In the International Journal of Theoretical Computer Science, TCS, Volume/Issue291/3 pp. 223-283, Elsevier.
9. Page Web du cours :
moodle.uqo.ca