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 2018  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, 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.

 10 sept. 2018 
2   

Algèbres de processus : Calculus for Communicating Systems (CCS)

 17 sept. 2018 
3   

Calculus for Communicating Systems (CCS) (suite)

 24 sept. 2018 
4   

Formalismes Logiques : mu calcul modal

 01 oct. 2018 
5   

Semaine d'études.

 08 oct. 2018 
6   

Examen intra.

 15 oct. 2018 
7   

mu calcul modal (suite)

 22 oct. 2018 
8   
  • Linear Temporal Logic (LTL)
  • Évaluation de modèles
  • Automates de Büchi
 29 oct. 2018 
9   
  • Linear Temporal Logic (LTL) (suite)
  • Évaluation de modèles
  • Automates de Büchi
 05 nov. 2018 
10   

Renforcement de politiques de sécurité : approche algebrique.

 12 nov. 2018 
11   

Systèmes de réécriture.

 19 nov. 2018 
12   

Renforcement de politiques de sécurité par réécriture.

 26 nov. 2018 
13   

Présentation des projets.

 03 déc. 2018 
14   
  • Présentation des projets.
  • Révision pour l'examen final.
 10 déc. 2018 
15   

Examen final.

 17 déc. 2018 
6. Évaluation du cours :
  • Examen de mi-session : 30 %
  • Examen final : 40 %
  • Projet de session : 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