Recherche
Financement des activités
Le financement de mes activités de recherche au Canada est ou bien a été effectué par:
Le financement de mes activités de recherche en France a été effectué par:
Activités en cours
Explorer la combinaison d'analyse statique et dynamique, moniteurs et instrumentation, de code pour la détection de code malicieux. Ce travail est accompli avec mes étudiants gradués: Hugues Chabot, Raphaël Khoury et Frédérick Lemay. Une autre activité est liée au Cyber Forensics et elle est menée conjointement avec des collègues de l'université Concordia, les professeurs Mourad Debbabi et R. Dssouli.
Détection de code malicieux
Compilation certifiée:
Travail accompli en collaboration avec le Professeur Mourad Debbabi et d'anciens étudiants gradués Emmanuel Giasson, Bechir Ktari et Frédéric Michaud. 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.
Analyse statique:
Travail accompli en collaboration avec les Professeurs Mourad Debbabi, Jules Desharnais et Jean Bergeron avec des étudiants gradués Mourad Erhioui and Marc Lavoie. Il porte sur la définition d'une suite de technoques basées sur l'analyse statique pour la détection de comportements malicieux dans les codes binaires. Le produit de cette recherche est un prototyoe appelé SamCots qui fonctionne sur des binaires Win32.
Analyse dynamique
Dans le cadre d'une collaboration avec le professeur Mourad Debbabi et mon ancien étudiant gradué Dr. C. Talhi nous avons exploré l'analyse dynamique 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:
KVM (Kilo Virtual Machine, une machine virtuelle pour Java dans un contexte de ressources limitées)
Ce travail a été effectué dans le cadre d'une collaboration avec le professeur Mourad Debbabi et le laboratoire de recherche de Panasonic. Le produit de ce travail est l'implantation d'un compilateur juste à temps (E-Bunny) et une suite de méchanismes d'optimisations et leur intégration à la KVM.
Compilation Certifiée de Java:
Une collaboration avec les professeurs M. Debbabi et J. Desharnais et d'étudiants gradués M. Fourati, E. Menif et F. Painchaud. Dans le cadre d'une collaboration avec le RDDC (Recherche et Développement pour la Défense Canada) de Valcartier avec R. Charpentier, nous avons conçu et développé JACC un compilateur certifiant de Java.
Sémantique dynamique de Java
Avec mon collègue M. Debbabi et notre ancien étudiant gradué H. Yahyaoui nous avons élaboré une sémantique dynamique opérationnelle pour Java. Nous avons également élaboré un modèle sémantique pour Java supportant le parallélisme et le non déterminisme.
Vérification de protocoles cryptographiques
Avec mon collègue M. Debbabi et nos anciens étudiants M. Mejri et I. Yahmadi nous avons travaillé sur la vérification formelle de protocoles cryptographiques. Une méthode formelle et complètement automatique a été conçue et développée, le logiciel Dymna.
Vérification formelle
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 :
Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS.
Parallelisation 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 avec mes collègues B. Dehbonei, F. Hassaïne, P. Jouvelot et Catherine Laurent. Nous avons développé Pmacs un compilateur basé sur la détection de parallélisme par une méthode développée par le professeur Paul Feautrier. Cette méthode est basée sur un algorithme effectuant la résolution d'équations et inéquations linéaires dans les entiers de façon paramétrée.