Comme un automate à piles, Tayssir Touili déborde d'énergie. Grande passionnée de mathématiques, elle s'est jetée corps et âme dans une grande aventure, celle de contrer les malware. Amatrice de sports d'extérieurs, elle sera également heureuse de vous rencontrer autour d'une partie d'échec. Rencontre avec Tayssir Touili, nouvelle directrice de recherche à l'IRIF.

“Ce qu'il nous faut, c'est une technique qui va analyser le comportement du programme et non pas sa syntaxe, comme la signature matching et sans l'exécuter puisqu'il ne peut pas l'être indéfiniment. C’est justement ce que permet de faire le model checking, une technique qui analyse les comportements des systèmes. Mon idée a donc été de dire, appliquons le model cheking pour la détection de malware. C'est ce sur quoi porte mon travail aujourd'hui.” Tayssir Touili, directrice de recherche | Pôle Automates, structures et vérification - Équipe Modélisation et vérification.

Dès le lycée, je n'avais qu'une obsession, faire des maths. J'ai donc naturellement poursuivi ma scolarité par une classe préparatoire en Tunisie, qui m'a conduit à intégrer l'école Polytechnique de Tunisie où j'ai été major de promo. Je suis ensuite venue à Paris pour faire un DEA en algorithmique à l'université Paris VII, puis, toujours dans la même université, j'ai continué par une thèse avec Ahmed Bouajjani. Enfin, j'ai terminé avec un post-doctorat, pendant un an, à l'université Carnegie Mellon, à Pittsburgh, aux États-Unis, avec Edmund M. Clarke qui est le fondateur du model checking.
A mon retour, j'ai été prise comme chargée de recherche au CNRS au LIAFA où je suis restée pendant 10 ans. Puis, je suis devenue directrice de recherche au LIPN jusqu'en début 2024 et j'ai récemment demandé une mutation pour travailler à l'IRIF.

Au début de ma carrière, je travaillais sur la vérification des systèmes infinis, c'est à dire des systèmes qui ont un nombre infini d'états, de configurations. Mon travail de thèse consistait à faire ce qu'on appelle du regular model cheking c'est à dire, représenter les ensembles infinis de configurations par des automates finis, donc travailler sur ces automates et réduire les problèmes de la vérification aux problèmes d'accessibilités.

Depuis, j’ai changé, je travaille maintenant sur la détection des virus, les malware. La détection des virus est un problème très important de nos jours, crucial même, comme en témoignent la quantité très importante de cyberattaques.
Le problème est que les techniques qui existent aujourd'hui ne sont pas assez robustes, les antivirus dont on dispose sur nos ordinateurs ne sont pas assez efficaces. Leurs techniques sont essentiellement basées sur deux approches:

1. la première est ce qu'on appelle la signature matching, où chaque malware a une signature, c'est à dire une séquence de bits, et chaque antivirus a une database, une base de données de signatures. D'ailleurs, l'antivirus demande assez fréquemment de faire des mises à jour, pour réactualiser les signatures qu'il a enregistré. Pour savoir si un programme que l'on télécharge est un virus ou non, l'antivirus va chercher si syntaxiquement, le code de ce nouveau programme va matcher une des signatures qu'il a dans sa base de données ou pas. Le problème est que ces techniques sont très simples à contourner, parce qu'il suffit de prendre un virus, de changer légèrement son code pour obtenir une deuxième version du virus, donc un autre bout de code qui a exactement le même comportement que le virus initial mais qui a une signature différente. Il ne sera donc pas détecté par l'antivirus, puisque sa signature ne sera pas dans la base de données de l'antivirus. Les personnes qui écrivent les virus le savent et c'est pour cela qu'elles mettent à jour fréquemment leurs malware. Pour un seul malware, on peut donc obtenir des millions de variantes. Dès l'instant où la signature d'un malware est connue, l'écrivain qui l'a créé, va changer une partie de son code.
2. L'autre technique, c'est ce qu'on appelle l’émulation de code, c'est à dire que l'antivirus va essayer d'exécuter le programme dans un environnement virtuel. Il va essayer de le simuler, et si un comportement malveillant est rencontré, il va prévenir que c'est un virus. Dans le cas contraire, il dira que c'est un bon programme. Mais, le problème c'est que l'antivirus ne peut pas exécuter le programme à l'infini. Le comportement malveillant peut donc arriver après un certain temps, sans que l'antivirus ne puisse le détecter.

Par conséquent, ces deux techniques-là, qui existent dans les antivirus que nous utilisons sur nos ordinateurs par exemple, ne sont pas assez robustes. Ce qu'il nous faut, c'est une technique qui va analyser le comportement du programme et non pas sa syntaxe, comme la signature matching et sans l'exécuter puisqu'il ne peut pas l'être indéfiniment. C’est justement ce que permet de faire le model checking, une technique qui analyse les comportements des systèmes. Mon idée a donc été de dire, appliquons le model cheking pour la détection de malware. C'est ce sur quoi porte mon travail aujourd'hui.

Les principaux concepts de ma recherche sont donc la détection de malware grâce au model cheking.

Je travaille aussi beaucoup avec les automates à piles parce qu'ils me permettent justement de modéliser ces programmes.
Pour préciser un peu ce qu'est le model checking, c'est en fait une approche générale qui permet de savoir de manière complètement automatique si un système satisfait une propriété ou pas. Pour faire appliquer le model checking à la détection de malware, l'idée est de représenter un programme par un modèle mathématique, et de spécifier les comportements malveillants par une formule dans une logique.
Les comportements malveillants sont donc spécifiés par une formule dans une logique temporelle. On va donc réduire le problème de savoir si un programme est malveillant ou pas, au problème de savoir si un modèle mathématique satisfait ou non une certaine formule. Cette dernière va représenter le comportement malveillant tandis que le modèle mathématique va représenter le programme en question. Et moi, comme modèle mathématique, j'utilise beaucoup les automates à piles, ainsi que des variantes et extensions de ceux-ci, tout simplement parce qu'ils permettent de représenter de manière précise les programmes. Les automates à piles sont un modèle qui a de bonnes propriétés d’accessibilité et de décidabilité. Ils permettent de modéliser de manière assez précise les comportements des programmes.

Nous avons entamé notre travail sur un antivirus qui arrive déjà à détecter des malware que des antivirus commerciaux existants n'arrivent pas à détecter. Le tableau de comparaison de notre antivirus avec d'autres antivirus disponibles sur le marché était impressionnant. Ça fait même très peur. Pour faire ce test, on ne pouvait pas comparer notre antivirus avec les antivirus existants en utilisant les malware déjà connus. En effet, les bases de données des antivirus existants contiennent déjà les signatures des malware déjà connus.. C'est pour cela qu'on a utilisé un générateur de malware automatique pour en créer 200 nouveaux ; on voulait voir comment les antivirus existants réagissaient en leur envoyant de nouveaux malware et comment notre programme réagirait également. Certains antivirus n'ont même pas pu détecter un seul malware que nous avions créé. Mais pour le moment, aucun programme n'arrive à détecter tous les malware ; il y a encore beaucoup de cas, de programmes, de particularités que, à ce stade-là, nous n'avons pas encore traités. J'espère que dans les 10 prochaines années, nous arriverons à traiter plus de comportements, et que l'on arrivera à faire un vrai antivirus, qui concurrencera grandement les antivirus existants, et que l'on pourra, pourquoi pas, valoriser et proposer aux entreprises.

Concernant la détection de malware, c'est en voyant toutes les cyberattaques de ces dernières années, plusieurs ministères ont été attaqués par des hackeurs pro-russe, il y eu la CAF, le crédit agricole également, Microsoft (outlook) qui ont été hackés, que j’ai voulu me rendre utile à la société. C'est en fait la protection de nos données qui est en jeu, et de nos jours, c'est un problème qui est réellement important.

Pour ce qui est de l'informatique en générale, lorsque l'on aime les maths comme je les aimais au lycée, ce qui vient naturellement après, c’est de faire une classe préparatoire puis ensuite d'aller dans une école d’ingénieure. Et c'est à ce moment-là que je me suis passionnée pour les automates, qui sont en fait des modèles mathématiques.

Pour moi, l'IRIF m’offre un cadre de recherche exceptionnel et j’aimerais en profiter pour développer mon projet : réussir à faire un vrai antivirus qui va concurrencer les antivirus existants en contrant une grande majorité de virus, si ce n'est la totalité. C'est vraiment mon but, c'est une vraie obsession désormais.

Un vrai problème mathématique est de savoir si P=NP ou pas. C'est un problème ouvert.
Dès que je suis arrivée en thèse, j’ai dit à mon directeur de thèse que j'avais une preuve que P était bien égale à NP. En moins de 15 minutes, tout en prenant la chose tout à fait au sérieux, et en ayant la gentillesse de ne pas me rappeler que de grands chercheurs plus expérimentés que moi n'avaient toujours pas trouvé la réponse, il m'a rapidement prouvé pourquoi ma preuve était fausse.

Je suis très sportive, j'adore faire du footing, de la randonnée, et par exemple j’adore faire la traversée de Paris.
Je fais du luth, quand j'étais jeune j'en faisais beaucoup, j'ai moins de temps aujourd'hui mais quand j'ai l'occasion, j'aime en rejouer.
J’aime aussi beaucoup jouer aux échecs, et la première chose que j'ai remarqué quand je suis arrivée à l'IRIF, c'est l'échiquier du 4ème étage.

2024 : Arrivée à l'IRIF en tant que directrice de recherche
2014-2024 : Directrice de recherche au LIPN
2004-2014 : Chargée de recherche au CNRS au LIAFA
2003-2004 : Post-doctorat à la Carnegie Mellon University à Pittsburgh (États-Unis) avec Edmund M. Clarke
2000-2003 : Thèse à l'Université Paris VII (aujourd'hui Université Paris Cité) avec Ahmed Bouajjani