Model checking self modifying code
Vérification de code auto-modifiant
par Xin YE sous la direction de Tayssir TOUILI et de Jifeng HE
Thèse de doctorat en Informatique
ED 386 Sciences Mathematiques de Paris Centre

Soutenue le lundi 30 septembre 2019 à Université Paris Cité , East China normal university (Shanghai)

Sujets
  • Logique temporelle
  • Vérification de modèles (informatique)
  • Virus informatiques

Les thèses de doctorat soutenues à Université Paris Cité sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

TEL (Version intégrale de la thèse (pdf))

Description en anglais
Description en français
Mots clés
Code auto-modifiant, Détection de malware, Pushdown system, Analyse de l'accessibilité, Code binaire, LTL (Logique Temporelle Linéaire), CTL (Logique temporelle arborescente)
Resumé
Le code auto-modifiant est un code qui modifie ses propres instructions pendant le temps d'exécution. Il est aujourd'hui largement utilisé, notamment dans les logiciels malveillants pour rendre le code difficile à analyser et à été détecté par les anti-virus. Ainsi, l'analyse de tels programmes d'auto-modifiant est un grand défi. Pushdown System(PDSs) est un modèle naturel qui est largement utilisé pour l'analyse des programmes séquentiels car il permet de modéliser précisément les appels de procédures et de simuler la pile du programme. Dans cette thèse, nous proposons d'étendre le modèle du PDS avec des règles auto-modifiantes. Nous appelons le nouveau modèle Self-Modifying PushDown System (SM- PDS). Un SM-PDS est un PDS qui peut modifier l'ensemble des règles de transitions pendant l'exécution. Tout d'abord, nous montrons comment les SM-PDS peuvent être utilisés pour représenter des programmes auto- et nous fournissons des algorithmes efficaces pour calculer les configurations précédentes et suivantes des SM-PDS accessibles. Ensuite, nous résolvons les problèmes sur la vérification de propriétés LTL et CTL pour le code auto-modifiant. Nous implémentons nos techniques dans un outil appelé SMODIC. Nous avons obtenu des résultats encourageants. En particulier, notre outil est capable de détecter plusieurs logiciels malveillants auto-modifiants ; il peut même détecter plusieurs logiciels malveillants que les autres logiciels anti-virus bien connus comme McAfee, Norman, BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast et Symantec n'ont pas pu détecter.