Title: Model-Checking for Malware Detection

Speaker: Fu Song (East China Normal University, Shanghai, China)

Time: 15:00, 19th March 2014

Venue: Lecture Room (334), 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

In this presentation, I will introduce 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 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.

Bio:

Dr. Fu Song obtained his PhD. degree from LIAFA, Paris 7, France in 2013. His research interests include model checking, program verification, malware analysis and detection. His work has been published in prestigious international conferences and journals, including ETAPS/TACAS, CONCUR, FM, STTT, ESEC/FSE, and ASE. He won the ETAPS/TACAS best paper award in 2012.

More information can be found in his homepage: http://www.liafa.univ-paris-diderot.fr/~song/