Faster resolution based metamorphic virus detection using ATP control strategy

Ruo Ando, Nguyen Anh Quynh, Yoshiyasu Takefuji

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

In this paper we propose a resolution based detection method for detecting metamorphic computer virus. Our method is the application of formal verification using theorem proving, which deduce parts of viral code from the large number of obfuscated operations and re-assemble those in order to reveal the signature of virus. While previously many kinds of the symbolic emulation based methods have been applied for metamorphic virus, no resolution strategy based method is proposed. It is showed that the complexity of metamorphic virus can be solved if the obfuscated viral code is canonicalized and simplified using resolution based state pruning and generation. To make our detection method more feasible and effective, redundancy-control strategies are applied for the resolution process. In this paper the strategies of demodulation and subsumption are applied for eliminating the redundant path of resolution. Experiment shows that without these strategies, resolving metamorphic code into several simplified operations is almost impossible, at least is not feasible in reasonable computing time. The statistics of reasoning process in detecting obfuscated API call is also presented. We divide obfuscated API call into four modules according to the types of metamorphic techniques and compare the conventional resolution with our method applying redundancy-control strategy.

Original languageEnglish
Pages (from-to)260-266
Number of pages7
JournalWSEAS Transactions on Information Science and Applications
Volume3
Issue number2
Publication statusPublished - 2006 Feb

Fingerprint

Adenosinetriphosphate
Application programming interfaces (API)
Virus
Redundancy
Control Strategy
Computer viruses
Theorem proving
Demodulation
Statistics
Computer Virus
Theorem Proving
Emulation
Experiments
Formal Verification
Pruning
Divides
Deduce
Signature
Reasoning
Module

Keywords

  • First-order logic
  • Metamorphic virus
  • Obfuscated APl call
  • Redundancy control strategy
  • Resolution based detection
  • Theorem proving

ASJC Scopus subject areas

  • Computer Science (miscellaneous)
  • Computational Mathematics

Cite this

Faster resolution based metamorphic virus detection using ATP control strategy. / Ando, Ruo; Anh Quynh, Nguyen; Takefuji, Yoshiyasu.

In: WSEAS Transactions on Information Science and Applications, Vol. 3, No. 2, 02.2006, p. 260-266.

Research output: Contribution to journalArticle

@article{443897d4b913460182ffea06de29e127,
title = "Faster resolution based metamorphic virus detection using ATP control strategy",
abstract = "In this paper we propose a resolution based detection method for detecting metamorphic computer virus. Our method is the application of formal verification using theorem proving, which deduce parts of viral code from the large number of obfuscated operations and re-assemble those in order to reveal the signature of virus. While previously many kinds of the symbolic emulation based methods have been applied for metamorphic virus, no resolution strategy based method is proposed. It is showed that the complexity of metamorphic virus can be solved if the obfuscated viral code is canonicalized and simplified using resolution based state pruning and generation. To make our detection method more feasible and effective, redundancy-control strategies are applied for the resolution process. In this paper the strategies of demodulation and subsumption are applied for eliminating the redundant path of resolution. Experiment shows that without these strategies, resolving metamorphic code into several simplified operations is almost impossible, at least is not feasible in reasonable computing time. The statistics of reasoning process in detecting obfuscated API call is also presented. We divide obfuscated API call into four modules according to the types of metamorphic techniques and compare the conventional resolution with our method applying redundancy-control strategy.",
keywords = "First-order logic, Metamorphic virus, Obfuscated APl call, Redundancy control strategy, Resolution based detection, Theorem proving",
author = "Ruo Ando and {Anh Quynh}, Nguyen and Yoshiyasu Takefuji",
year = "2006",
month = "2",
language = "English",
volume = "3",
pages = "260--266",
journal = "WSEAS Transactions on Information Science and Applications",
issn = "1790-0832",
publisher = "World Scientific and Engineering Academy and Society",
number = "2",

}

TY - JOUR

T1 - Faster resolution based metamorphic virus detection using ATP control strategy

AU - Ando, Ruo

AU - Anh Quynh, Nguyen

AU - Takefuji, Yoshiyasu

PY - 2006/2

Y1 - 2006/2

N2 - In this paper we propose a resolution based detection method for detecting metamorphic computer virus. Our method is the application of formal verification using theorem proving, which deduce parts of viral code from the large number of obfuscated operations and re-assemble those in order to reveal the signature of virus. While previously many kinds of the symbolic emulation based methods have been applied for metamorphic virus, no resolution strategy based method is proposed. It is showed that the complexity of metamorphic virus can be solved if the obfuscated viral code is canonicalized and simplified using resolution based state pruning and generation. To make our detection method more feasible and effective, redundancy-control strategies are applied for the resolution process. In this paper the strategies of demodulation and subsumption are applied for eliminating the redundant path of resolution. Experiment shows that without these strategies, resolving metamorphic code into several simplified operations is almost impossible, at least is not feasible in reasonable computing time. The statistics of reasoning process in detecting obfuscated API call is also presented. We divide obfuscated API call into four modules according to the types of metamorphic techniques and compare the conventional resolution with our method applying redundancy-control strategy.

AB - In this paper we propose a resolution based detection method for detecting metamorphic computer virus. Our method is the application of formal verification using theorem proving, which deduce parts of viral code from the large number of obfuscated operations and re-assemble those in order to reveal the signature of virus. While previously many kinds of the symbolic emulation based methods have been applied for metamorphic virus, no resolution strategy based method is proposed. It is showed that the complexity of metamorphic virus can be solved if the obfuscated viral code is canonicalized and simplified using resolution based state pruning and generation. To make our detection method more feasible and effective, redundancy-control strategies are applied for the resolution process. In this paper the strategies of demodulation and subsumption are applied for eliminating the redundant path of resolution. Experiment shows that without these strategies, resolving metamorphic code into several simplified operations is almost impossible, at least is not feasible in reasonable computing time. The statistics of reasoning process in detecting obfuscated API call is also presented. We divide obfuscated API call into four modules according to the types of metamorphic techniques and compare the conventional resolution with our method applying redundancy-control strategy.

KW - First-order logic

KW - Metamorphic virus

KW - Obfuscated APl call

KW - Redundancy control strategy

KW - Resolution based detection

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=30144437354&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=30144437354&partnerID=8YFLogxK

M3 - Article

VL - 3

SP - 260

EP - 266

JO - WSEAS Transactions on Information Science and Applications

JF - WSEAS Transactions on Information Science and Applications

SN - 1790-0832

IS - 2

ER -