Faster resolution based metamorphic virus detection using ATP control strategy

Ruo Ando, Nguyen Anh Quynh, Yoshiyasu Takefuji

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


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
Issue number2
Publication statusPublished - 2006 Feb
Externally publishedYes


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

ASJC Scopus subject areas

  • Information Systems
  • Computer Science Applications


Dive into the research topics of 'Faster resolution based metamorphic virus detection using ATP control strategy'. Together they form a unique fingerprint.

Cite this