Skip to Main content Skip to Navigation
Theses

Model checking self modifying code

Abstract : A Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown Systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because it allows to accurately model procedure calls and mimic the program’s stack. In this thesis, we propose to extend the PushDown System model with self-modifying rules. We call the new model Self-Modifying PushDown System (SM-PDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. First, we show how SM-PDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SM-PDSs. Then, we consider the LTL model-checking problem of self-modifying code. We reduce this problem to the emptiness problem of Self-modifying Büchi Pushdown Systems (SM-BPDSs). We also consider the CTL model-checking problem of self-modifying code. We reduce this problem to the emptiness problem of Self-modifying Alternating Büchi Pushdown Systems (SM-ABPDSs). We implement our techniques in a tool called SMODIC. We obtained encouraging results. In particular, our tool was able to detect several self-modifying malwares; it could even detect several malwares that well-known anti-viruses such as McAfee, Norman, BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast and Symantec failed to detect.
Document type :
Theses
Complete list of metadatas

Cited literature [63 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-02972592
Contributor : Abes Star :  Contact
Submitted on : Tuesday, October 20, 2020 - 3:05:25 PM
Last modification on : Thursday, October 22, 2020 - 3:27:20 AM

File

YE_Xin_va2.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02972592, version 1

Collections

Citation

Xin Ye. Model checking self modifying code. Logic in Computer Science [cs.LO]. Université de Paris; East China normal university (Shanghai), 2019. English. ⟨NNT : 2019UNIP7010⟩. ⟨tel-02972592⟩

Share

Metrics

Record views

48

Files downloads

20