Pushdown model checking for malware detection

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 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 study, we propose 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 a new logic, called stack computation tree predicate logic (SCTPL), to represent the malicious behavior. SCTPL can be seen as an extension of the branching-time temporal logic CTL with variables, quantifiers, and predicates over the stack. (3) Reducing the malware detection problem to the model-checking problem of PDSs against SCTPL formulas. We show how our new logic 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 specifications. We reduce this problem to emptiness checking in Symbolic Alternating Buchi Pushdown Systems, and we provide an algorithm to solve this problem. We implemented our techniques in a tool and applied it to detect several viruses. Our results are encouraging.