LTL model checking of self modifying code

DOI10.1007/S10703-022-00394-8MaRDI QIDQ6102164zbMATH OpenFDO

Authors Tayssir Touili, Xin Ye

Publication date 8 May 2023

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1909.12635

zbMATH Keywords

model checkingautomatamalware detection

Mathematics Subject Classification ID

Computer science (68-XX)

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.

Recommendations

• LTL model-checking for malware detection
• Pushdown model checking for malware detection
• Modelling metamorphism by abstract interpretation
• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• Efficient malware detection using model-checking

Cites work

• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• Computer Aided Verification
• Efficient malware detection using model-checking
• LTL model-checking for malware detection
• Reachability analysis of pushdown automata: Application to model-checking
• Reasoning about infinite computations
• Verified abstract interpretation techniques for disassembling low-level self-modifying code

Cited in

(3)

• Reachability Analysis of Self Modifying Code
• Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking
• A Logic Approach for LTL System Modification

This page was built for publication: LTL model checking of self modifying code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6102164)