Skip to Main content Skip to Navigation
Journal articles

CTL Model Checking of Self Modifying Code

Abstract : Self-modifying code is extensively used to obfuscate malware and to make reverse engineering harder. It consists in code that can modify its own instructions during the execution. Being able to analyse such code is crucial nowadays. In this paper, we consider the CTL model-checking problem of self modifying code. To model such programs, we use Self Modifying Pushdown Systems (SM-PDS), an extension of pushdown systems whose set of rules can be modified during execution. We reduce the CTL model-checking problem to the emptiness problem of Self-Modifying Alternating Büchi pushdown systems (SM-ABPDS). We implemented our techniques in a tool. 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 antiviruses such as McAfee, Norman, BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast and Symantec, failed to detect.
Document type :
Journal articles
Complete list of metadata
Contributor : Tayssir Touili Connect in order to contact the contributor
Submitted on : Tuesday, December 1, 2020 - 3:51:07 PM
Last modification on : Wednesday, June 2, 2021 - 3:28:27 AM
Long-term archiving on: : Tuesday, March 2, 2021 - 7:49:48 PM


Files produced by the author(s)


  • HAL Id : hal-03034019, version 1


Tayssir Touili, Xin Ye. CTL Model Checking of Self Modifying Code. Proceedings of the 25th INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2020), 2020. ⟨hal-03034019⟩



Record views


Files downloads