CTL Model Checking of Concurrent Self Modifying Code

Analysing programs without actually executing them is crucial for binary analysis but poses many challenges especially if we consider programs with the ability to spawn parallel processes (concurrency) and to modify their own instructions (self-modification). Modern malware uses this complexity to obfuscate the virus programs and make them hard to analyse. This paper proposes an efficient model checking approach for handling such type of programs. A natural abstraction of concurrent and self-modifying programs is SelfModifying Dynamic Pushdown Network (SM-DPN). It is a set of Pushdown Systems, each with the ability to spawn new processes and modify its own set of rules. We consider single indexed CTL model checking of these processes. A single indexed CTL formula represents a conjunction of CTL formulas, each corresponding to a single process. The problem is not trivial because a process may or may not be spawned, which affects the result. Our approach is to construct finite automata that accept process configurations satisfying the corresponding formula. Then, we iteratively exclude configurations that spawn violating processes. We implemented the algorithm and conducted practical experiments showing promising results. In particular, our tool was able to detect several self-modifying concurrent malware.