• GLO-3004 Spécification formelle et vérification de logiciels
• Cours enseignés antérieurement :
  • IFT-2002 Informatique théorique
  • IFT-3000 Langages de programmation
  • IFT-65186 Analyse statique de code
  • GLO-3004 Spécification formelle et vérification de logiciels

J’ai commencé mes recherches en analyse statique de code dans le cadre de compilateurs parallélisant. J’étais ensuite attirée par le domaine d’analyse de code pour sa vérification. Les enjeux importants en sécurité informatique m’ont poussé vers ce domaine. Mon objectif ultime c’est d’avoir des applications informatiques fiables. Ma devise en recherche est que les problématiques de recherche doivent être inspirées par des problèmes réels et les résoudre doit être basé sur des fondements scientifiques et mathématiques solides.

Activités actuelles

• Application des politiques de sécurité et notamment celles empêchant des données confidentielles d’atteindre d’être divulguées à des cibles non désirées par l’usager principal.
• Regroupement des courriels indésirables en campagnes.

Activités antérieures

• Explorer la combinaison d'analyse statique et dynamique, moniteurs et instrumentation, de code pour la détection de code malicieux.
• Compilation certifiée. Ce travail porte sur la conception et l'implantation d'un compilateur certifié pour ANSI C.  Ce travail a été effectué dans le contexte du projet Malicots pour le RDDC Valcartier.
• Analyse dynamique de code par moniteurs et ses limitations dans un contexte à ressources limitées.  Dans ce travail, nous avons caractérisé les propriétés qu'il est possible d'appliquer dans un contexte où les ressources mémoire sont limitées. L'idée clé est de les comparer à une classe de langages formels, les langages localement vérifiables.
• Compilation efficace et sécurité de Java. Amélioration de la performance de la KVM (Kilo Virtual Machine, une machine virtuelle pour Java dans un contexte de ressources limitées). Ce travail a été réalisé dans le cadre d’un projet avec le centre de recherche de Panasonic.
• Compilation Certifiée de Java. Dans le cadre d'une collaboration avec le RDDC (Recherche et Développement pour la Défense Canada) de Valcartier  nous avons conçu et développé JACC un compilateur certifiant de Java. 
• Vérification de protocoles cryptographiques
• Dans le cadre du GIE (Groupement d'intérêt économique) Dyade nous avons collaboré (en tant que groupe du centre de recherche Bull) avec un groupe de l'INRIA Rhone-Alpes. Le résultat de cette collaboration est l'application de la vérification formelle à un cas industrielle taille réelle. C'est la vérification du protocole d'arbitrage du bus de la machine PowerScale.   
• Parallélisation automatique. Dans le cadre de ma thèse de doctorat et sous la direction du professeur  Paul Feautrier, j'ai travaillé sur la parallélisation automatique de code et son exécution efficace sur une machine multi-processeurs à mémoire partagée. J'ai également travaillé sur ce thème au centre de recherche de Bull. 

1. Andrew Bedford, Stephen Chong, Josée Desharnais, Elisavet Kozyri,  Nadia Tawbi: A progress-sensitive flow-sensitive inlined information-flow control monitor (extended version). Computers & Security, 2017, Vol 71, 114--131. PDF (local version). Bibtex. 
2. Andrew Bedford, Stephen Chong, Josée Desharnais,   Nadia Tawbi: 
   A Progress-Sensitive Flow-Sensitive Inlined Information-Flow Control Monitor. IFIP SEC 2016: 352-366. PDF . Bibtex. 
3. Andrew Bedford, Sébastien Garvin, Josée Desharnais, Nadia Tawbi, Hana Ajakan, Frédéric Audet, Bernard Lebel: Andrana: Quick and Accurate Malware Detection for Android. FPS-2016: 20-35. PDF.  Bibtex. 
4. Mina Sheikhalishahi, Mohamed Mejri, Nadia Tawbi, Fabio Martinelli: Privacy-Aware Data Sharing in a Tree-Based Categorical Clustering Algorithm. FPS-2016: 161-178. PDF. Bibtex.
5. Mina Sheikhalishahi, Mohamed Mejri, Nadia Tawbi: On the Abstraction of a Categorical Clustering Algorithm. MLDM 2016: 659-675. PDF. Bibtex.  
6. Mina SheikhAlishahi, Andrea , Mohamed Mejri, Nadia Tawbi, Fabio Martinelli: Digital Waste Sorting: A Goal-Based, Self-Learning Approach to Label Spam Email Campaigns. STM 2015: 3-19. PDF. Bibtex.
7. Mina Sheikhalishahi, Mohamed Mejri, Nadia Tawbi:Clustering Spam Emails into Campaigns.
8. ICISSP 2015: 90-97. PDF. Bibtex. 
9. Mina Sheikhalishahi, Andrea Saracino, Mohamed Mejri, Nadia Tawbi, Fabio Martinelli:
10. Fast and Effective Clustering of Spam Emails Based on Structural Similarity.Foundations and Practice of Security, FPS 2015 : 195-211, PDF. Bibtex.
11. Raphaël Khoury and Nadia Tawbi: Equivalence-preserving corrective enforcement of security properties. 
12. International Journal of  Information and Computer Security Volume 7, number 2/3/4: 113-139 (2015), PDF. Bibtex.  
13. A. Bedford, J. Desharnais, T. G. Godonou and N. Tawbi. Enforcing information flow by combining static and dynamic analysis,  International Symposim on Foundations & Practice of Security (FPS'2013). PDF . bibtex .
14. J. Desharnais, E. P. Kanyabwero and N. Tawbi. Enforcing information flow policies by a three-valued analysis,  International Conference "Mathematical Methods, Models and Architectures for Computer Network Security" (MMM-ACNS 2012). Full version with proofs . bibtex .
15. R. Khoury, and N. Tawbi. Corrective Enforcement: A new Paradigm of Security Policy Enforcement by Monitors.   ACM Transactions on Information and System Security (2012). PDF . bibtex .
16. R. Khoury, and N. Tawbi. Which security policies are enforceable by runtime monitors? A survey. Computer Science Review 6 (2012) pp 27-45. PDF , bibtex .
17. F. Lemay, R. Khoury and N. Tawbi. Optimized Inlining of Runtime Monitors. NordSec 2011. PDF , bibtex .
18. H.  Chabot, R. Khoury, and N. Tawbi. Extending the Enforcement Power of Truncation Monitors Using Static Analysis. Computers & Security (2011). PDF , bibtex .
19. R. Khoury, and N. Tawbi. Corrective Enforcement of Security Policies. In Proceedings of the The 7th International Workshop on Formal Aspects of Security & Trust. September 2010. PDF , bibtex .
20. R. Khoury, and N. Tawbi. Using Equivalence Relations for Corrective Enforcement of Security Policies . In Proceedings of the  5th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2010, Lecture Notes in Computer Science, volume 6258. September 2010. PDF , bibtex .
21. H.  Chabot, R. Khoury, and N. Tawbi. Generating in-line monitors for Rabin automata . In Proceedings of The 14th Nordic Conference on Secure IT  Systems. October 2009. PDF , bibtex .
22. N. Tawbi C. Talhi and M. Debbabi. Execution monitoring enforcement under memory-limitations constraints. Information and Computation, 2008. PDF , bibtex .

Suite

• Membre de l’Ordre des ingénieurs du Québec (OIQ)

Futurs étudiants

Vous êtes motivé pour la recherche, vous aimez mon travail relaté dans mes publications (voir ma page de publications),  contactez-moi pour faire une maîtrise ou un doctorat.

Étudiants actuels

• Ashraf Heni (PhD)
• Montes Monforte Aldo (PhD)
• Théophane Gloria Godonou (MSc)
• Andrew Bedford (MSc)
• Jean-Claude Simo (MSc)
• Kamel Laliam (MSc)

Étudiants diplômés

• Raphaël Khoury (PhD)
• Chamseddine Talhi (PhD)
• Hamdi Yahyaoui (PhD)
• Emna Menif (PhD)
• Lamia Ketari (MSc)
• Erwanne P. Kanyabwero (MSc)
• Frédérick Lemay (MSc)
• Véronique Briard (MSc)
• Frédéric Samson (MSc)
• Dani Nassour (MSc)
• Frédéric Michaud (MSc)
• Jean-François Rodrigue (MSc)
• Mohamed Mejri (MSc)
• Azzam Mourad (MSc)
• Sami Zhioua (MSc)
• Robert Cantave
• Imed Yahmadi (MSc)
• Alikacem Elhachemi (MSc)
• Martin salois (MSc)
• Elie Isber (MSc)

J’ai fait mon doctorat en France à l’Université Pierre et Marie Curie, Paris, France. J’ai travaillé dans le centre de recherche Bull SA, France avant de venir à Québec pour un poste de professeur à l’Université Laval.

Les énormes enjeux en sécurité informatique m’ont poussé à m’intéresser à ce domaine et notamment à ce qu’on appelle « language based security ».  Plus d’informations sur mes recherches se trouvent dans la section Recherche.
 

• Diplôme d’ingénieur  en Informatique (CNAM, Conservatoire national des arts et métiers, Paris, France, 1985)
• Diplôme d’études approfondies (DEA), Université Pierre et Marie Curie, Paris, France,1986
• Ph.D. - Informatique (Université Pierre et Marie Curie, Paris, France, 1991)