LTL Model Checking of Self Modifying Code

TL;DR

This paper presents a novel approach for LTL model checking of self-modifying code using self-modifying pushdown systems, enabling detection of malware that traditional antivirus tools often miss.

Contribution

We introduce a new formal model and reduction technique for LTL model checking of self-modifying code, along with a tool that detects previously undetectable malware.

Findings

Successfully detected several self-modifying malware samples.

Outperformed well-known antivirus solutions in malware detection.

Validated the effectiveness of the proposed model and tool.

Abstract

Self modifying code is code that can modify its own instructions during the execution of the program. It is extensively used by malware writers to obfuscate their malicious code. Thus, analysing self modifying code is nowadays a big challenge. In this paper, we consider the LTL model-checking problem of self modifying code. We model such programs using self-modifying pushdown systems (SM-PDS), an extension of pushdown systems that can modify its own set of transitions during execution. We reduce the LTL model-checking problem to the emptiness problem of self-modifying B\"uchi pushdown systems (SM-BPDS). We implemented our techniques in a tool that we successfully applied for the detection of several self-modifying malware. Our tool was also able to detect several malwares that well-known antiviruses such as BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec failed to detect.