Jeudi 18 Juin

Heure:	14:30 - 15:30
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Model-checking for efficient malware detection
Description:	Tayssir Touili The number of malware is growing extraordinarily fast. Therefore, it is important to have efficient malware detectors. Malware writers try to obfuscate their code by different techniques. Many of these well-known obfuscation techniques rely on operations on the stack such as inserting dead code by adding useless push and pop instructions, or hiding calls to the operating system, etc. Thus, it is important for malware detectors to be able to deal with the program's stack. In this talk I will show a new model-checking approach for malware detection that takes into account the behavior of the stack. Our approach consists in : (1) Modeling the program using a Pushdown System (PDS). (2) Introducing new logics, called SCTPL and SLTPL, to represent the malicious behavior. SCTPL (resp. SLTPL) can be seen as an extension of the branching-time temporal logic CTL (resp. the linear-time temporal logic 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 show how our new logics can be used to precisely express malicious behaviors that could not be specified by existing specification formalisms. We then consider the model-checking problem of PDSs against SCTPL/SLTPL specifications. We provide efficient algorithms to solve these problems. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee.