On pushdown systems model checking : application to malware detection and software model-checking
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
In this thesis, we consider Pushdown Systems (PDSs) model-checking and its application to malware detection anc software model-checking. The main contribution of this thesis is a new model-checking approach for malware detection taking into account the behavior of the stack. Our approach consists in: (1) Modeling the program using a PDS. (2) Introducing two new logics, called SCTPL and SLTPL, to represent the malicious behaviors. SCTPL (resp. SLTPL) can be seen as an extension of the temporal logic CTL (resp. LTL) with variables, quantifiers, and predicates over the stack. (3) Reducing the malware detection problem to the model-checking problem of PDSs against SCTPL/SLTPL formulas. We present symbolic techniques to solve these model-checking problems and implement them in our tool POMMADE. POMMADE was able to detect 600 real malwares and 200 new malwares. Several well-known and widely used anti-viruses such as Avira, Avast, Kaspersky, McAfee or Norton were not able to detect several of these new malwares. POMMADE was also able to prove that 400 real benign programs are benign. We also consider in this thesis CTL model checking for PDSs. Finally, we consider Dynamic Pushdown Networks (DPNs) model-checking.
Abstract FR:
Dans cette thèse, nous considérons le problème de vérification des systèmes à pile (PDS) et son application à la détection de codes malveillants et à la vérification du logiciel. La principale contribution est une nouvelle approche de model-checking pour la détection des malwares en tenant compte du comportement de la pile. Notre approche consiste à: (1) la modélisation du programme à l'aide d'un PDS. (2) La définition de deux logiques nouvelles, appelées SCTPL et SLTPL, pour représenter les comportements malveillants. SCTPL (resp. SLTPL) peut être vue comme une extension de la logique temporelle CTL (resp. LTL) avec des variables, des quantificateurs, et des prédicats sur la pile. (3) La réduction du problème de détection de codes malveillants auproblème de model-checking de PDS contre des formules SCTPL / SLTPL. Nous présentons des techniques symboliques pour résoudre ces problèmes de model-checking. Nous avons mis en œuvre ces techniques dans notre outil POMMADE. POMMADE est capable de détecter 600 malwares réels et 200 nouveaux malwares. Plusieurs anti-virus bien connus et largement utilisés tels que Avira, Avast, Kaspersky, McAfee ou Norton ne sont pas en mesure de détecter plusieurs de ces nouveaux malwares. POMMADE a également été en mesure de prouver que 400 programmes bénins sont bénins. Nous considérons également dans cette thèse le problème de vérification de propriétés CTL pour les PDS. Enfin, nous considérons le problème de vérification de réseaux d'automates à piles.