PoMMaDe: pushdown model-checking for malware detection

Abstract

We present PoMMaDe, a Pushd own Model-checking based M alware D etector. In PoMMaDe, a binary program is modeled as a pushdown system (PDS) which allows to track the stack of the program, and malicious behaviors are specified in SCTPL or SLTPL, where SCTPL (resp. SLTPL) is an extension of CTL (resp. LTL) with variables, quantifiers, and predicates over the stack (needed for malware specification). The malware detection problem is reduced to SCTPL/SLTPL model-checking for PDSs. PoMMaDe allows us to detect 600 real malwares, 200 new malwares generated by two malware generators NGVCK and VCL32, and prove benign programs are benign. In particular, PoMMaDe was able to detect several malwares that could not be detected by well-known anti-viruses such as Avira, Avast, Kaspersky, McAfee, AVG, BitDefender, Eset Nod32, F-Secure, Norton, Panda, Trend Micro and Qihoo 360.

BibTeX

@inproceedings{Song-Touili:FSE13,
  author    = {Fu Song and
               Tayssir Touili},
  title     = {{PoMMaDe:} pushdown model-checking for malware detection},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {607--610},
  publisher = {{ACM}},
  year      = {2013},
}

PoMMaDe: pushdown model-checking for malware detection

Abstract

Related papers