Bourse de doctorat en informatique à Paris : Model Checking pour la détection de logiciels malveillants (virus)

Vérification du modèle pour la détection des logiciels malveillants (virus) :

Le nombre de malwares ayant généré des incidents en 2010 est supérieur à 1,5 milliard. Un malware peut causer de graves dommages, par exemple le ver MyDoom a ralenti l’accès à Internet mondial de dix pour cent en 2004. Les autorités enquêtant sur le crash du vol Spanair 5022 en 2008 ont découvert qu’un système informatique central utilisé pour surveiller les problèmes techniques de l’avion était infecté par un malware. Il est donc crucial de disposer de détecteurs de virus efficaces et à jour. Les systèmes antivirus existants utilisent diverses techniques de détection pour identifier les virus, telles que (1) l’émulation de code où le virus est exécuté dans un environnement virtuel pour être détecté ; ou (2) la détection de signature, où une signature est un modèle de code de programme qui caractérise le virus. Un fichier est déclaré comme virus s’il contient une séquence d’instructions de code binaire qui correspond à l’une des signatures connues. Chaque variante de virus a sa signature correspondante. Ces techniques ont certaines limites. En effet, les techniques basées sur l’émulation ne peuvent vérifier le comportement du programme que dans un intervalle de temps limité. Elles ne peuvent pas vérifier ce qui se passe après le délai d’expiration. Ainsi, ils risquent de ne pas détecter le comportement viral s’il se produit après cet intervalle de temps. Quant aux systèmes basés sur les signatures, il est très facile pour les développeurs de virus de les contourner. Il suffit d’appliquer des techniques d’obfuscation pour modifier la structure du code tout en gardant les mêmes fonctionnalités, de sorte que la nouvelle version ne corresponde pas aux signatures connues. Les techniques d’obfuscation peuvent consister à insérer du code mort, à remplacer des instructions par des instructions équivalentes, etc. Les auteurs de virus mettent fréquemment à jour leurs virus pour les rendre indétectables par ces systèmes antivirus.

Pour contourner ces limitations, au lieu d’exécuter le programme ou de procéder à une vérification syntaxique, les détecteurs de virus doivent utiliser des techniques d’analyse qui vérifient le comportement (et non la syntaxe) du programme de manière statique, c’est-à-dire sans l’exécuter. Dans ce but, nous proposons d’utiliser le model-checking pour la détection de virus.

Le model-checking est un formalisme mathématique qui permet de vérifier si un système satisfait une propriété donnée. Il consiste à représenter le système à l’aide d’un modèle mathématique M, la propriété à l’aide d’une formule F dans une logique donnée, puis à vérifier si le modèle M satisfait la formule F. Le model-checking a déjà été appliqué à la détection de malwares. Cependant, les travaux existants présentent certaines limites.

En effet, les langages de spécification qu’ils utilisent n’ont été appliqués que pour spécifier et détecter un ensemble particulier de comportements malveillants. Ils ne peuvent pas être utilisés pour détecter tous les comportements des virus. Ainsi, l’un des principaux défis de la détection des logiciels malveillants est de proposer des formalismes de spécification et des techniques de détection capables de spécifier et de détecter un ensemble plus large de virus.

L’objectif de cette thèse est donc de :

1- Définir des logiques expressives qui peuvent être utilisées pour exprimer de manière compacte des comportements malveillants. Notre objectif est de pouvoir – exprimer un large ensemble de comportements malveillants qui n’étaient pas considérés auparavant.

2- Définir des algorithmes de model-checking efficaces pour ces logiques.

3- Réduire le problème de détection des malwares au problème de model-checking de ces logiques.

4- Implémenter ces techniques dans un outil de détection de malwares et appliquer cet outil pour détecter plusieurs malwares.

L’objectif ultime est de construire un détecteur de malware plus précis que les antivirus commerciaux existants.

Qu’est-ce qui est financé

Un doctorat en informatique

Durée

3 ans

Admissibilité

Étudiant titulaire d’un diplôme de master en informatique.