Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 2/2022

14-02-2023

LTL model checking of self modifying code

Authors: Tayssir Touili, Xin Ye

Published in: Formal Methods in System Design | Issue 2/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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, 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üchi pushdown systems. 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.
previous article Control strategies for off-line testing of timed systems
next article Functional synthesis via input–output separation

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
2
Self-modifying instructions are embedded into these programs.
 
Literature
1.
Touili T, Ye X (2017) Reachability analysis of self modifying code. In: 2017 22nd international conference on engineering of complex computer systems (ICECCS). IEEE, pp. 120–127
2.
Bouajjani A, Esparza J, Maler O (1997) reachability analysis of pushdown automata: application to model checking. In: International conference on concurrency theory (CONCUR). Springer, pp 135–150
3.
Esparza J, Hansel D, Rossmanith P, Schwoon S (2000) Efficient algorithms for model checking pushdown systems. In: International conference on computer aided verification (CAV). Springer, pp 232–247
4.
Touili T, Ye X (2019) LTL model checking of self modifying code. In: 2019 24th international conference on engineering of complex computer systems (ICECCS). IEEE, pp 1–10
5.
Bergeron J, Debbabi M et al (2001) Static detection of malicious code in executable programs. Int J Req Eng 79:184–189
6.
Balakrishnan G, Reps T, Kidd N, Lal A, Lim J et al (2005) Model checking x86 executables with codesurfer/x86 and WPDS++. In: International conference on computer aided verification (CAV). Springer, pp 158–163
7.
Singh P, Lakhotia A (2003) Static verification of worm and virus behavior in binary executables using model checking. In: IEEE systems, man and cybernetics societyinformation assurance workshop, 2003. IEEE, pp. 298–300
8.
Kinder J, Katzenbeisser S, Schallhart C, Veith H (2005) Detecting malicious code by model checking. In: International conference on detection of intrusions and malware, and vulnerability assessment. Springer, pp. 174–187
9.
Song F, Touili T (2012) Efficient malware detection using model-checking. In: International symposium on formal methods. Springer, pp 418–433
10.
Beaucamps P, Gnaedig I, Marion J (2010) Behavior abstraction in malware analysis. In: International conference on runtime verification. Springer, pp 168–182
11.
Song F, Touili T (2013) LTL model-checking for malware detection. In: International conference on tools and algorithms for the construction and analysis of systems (TACAS). Springer, pp 416–431
12.
Nguyen H, Touili T (2017) CARET model checking for malware detection. In: Proceedings of the 24th ACM SIGSOFT international SPIN symposium on model checking of software
13.
Dam K, Touili T (2018) Learning malware using generalized graph kernels. In: Proceedings of the 13th international conference on availability, reliability and security, pp 1–6
14.
Dam K, Touili T (2018) Precise extraction of malicious behaviors. In: 42nd annual computer software and applications conference (COMPSAC), vol 1. IEEE, pp 229–234
15.
Dam K, Touili T (2017) Malware detection based on graph classification. In: ICISSP, 2017
16.
Cai H, Shao Z, Vaynberg A Certified self-modifying code. In: ACM SIGPLAN notices, vol 42 no. 6
17.
Debray S, Coogan K, Townsend G On the semantics of self-unpacking malware code. Technical report University of Arizona, Computer Science
18.
Bonfante G, Marion J, Reynaud-Plantey D (2009) A computability perspective on self-modifying programs. In: International conference on software engineering and formal methods (SEFM). IEEE, pp 231–239
19.
Bertrand A, Matias M, Koen D (2006) A model for self-modifying code. In: International workshop on information hiding, Springer, pp 232–248
20.
Blazy S, Laporte V, Pichardie D (2016) Verified abstract interpretation techniques for disassembling low-level self-modifying code. J Autom Reason 56(3):283–308MathSciNetCrossRefMATH
21.
Roundy K, Miller B (2010) Hybrid analysis and control of malware. In: International workshop on recent advances in intrusion detection. Springer, pp 317–338
22.
Coogan K, Debray S, Kaochar T, Townsend G (2009) Automatic static unpacking of malware binaries. In: 2009 16th working conference on reverse engineering. IEEE, pp 167–176
23.
Gyung K et al (2007) Renovo: a hidden code extractor for packed executables. In: Proceedings of the 2007 ACM workshop on recurring malcode, pp 46–53
24.
Royal P, Halpin M et al (2006) Polyunpack: automating the hidden-code extraction of unpack-executing malware. In: 22nd annual computer security applications conference (ACSAC’06). IEEE, pp 289–300
25.
Schwoon S (2002) Model-checking pushdown systems. Ph.D. thesis, Technische Universität München, Universitätsbibliothek
26.
Kinder HJ (2008) Jakstab: a static analysis platform for binaries. In: International conference on computer aided verification (CAV). Springer
27.
Vardi M, Wolper P Reasoning about infinite computations. Inf Comput 115(1)
28.
Gastin P, Oddoux D (2001) Fast LTL to büchi automata translation. In: International conference on computer aided verification (CAV). Springer
29.
30.
31.
32.
33.
Pang C, Yu R, Chen Y, Koskinen E, Portokalidis G, Mao B, Xu J (2021) Sok: all you ever wanted to know about x86, x64 binary disassembly but were afraid to ask. In: IEEE symposium on security and privacy (SP). IEEE, pp 833–851
Metadata
Title
LTL model checking of self modifying code
Authors
Tayssir Touili
Xin Ye
Publication date
14-02-2023
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 2/2022
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-022-00394-8

Other articles of this Issue 2/2022

Formal Methods in System Design 2/2022 Go to the issue

OriginalPaper

Functional synthesis via input–output separation

OriginalPaper

Control strategies for off-line testing of timed systems

OriginalPaper

Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

Correction

Correction: Parameterized verification of leader/follower systems via first-order temporal logic

OriginalPaper

Assumption-based Runtime Verification

OriginalPaper

Specifiable robustness in reactive synthesis

Premium Partner

    Image Credits