Using algebraic models of programs for detecting metamorphic malwares
Polymorphic and metamorphic viruses are the most sophisticated malicious programs that give a lot of trouble to virus scanners. Each time when these viruses infect new executables or replicate themselves they completely modify (obfuscate) their signature to avoid being detected. This contrivance poses a serious threat to anti-virus software which relies on classical virus-detection techniques: such viruses do not have any stable specific sequence of instructions to be looked for. In the ultimate case the only characteristic which remains invariable for all generations of the same virus is their functionality (semantics). To all appearance, the only way to detect for sure a metamorphic malicious code is to look for a pattern which has the same semantics as (i.e. equivalent to) some representative sample of the virus. Thus, metamorphic virus detection is closely related to the equivalence-checking problem for programs. In this paper we outline some new automata-theoretic framework for the designing of virus detectors. Our approach is based on the equivalence-checking techniques in algebraic models of sequential programs. An algebraic model of programs is an abstract model of computation where programs are viewed as finite automata operating on Kripke structures. Models of this kind make it possible to focus on those properties of program instructions that are widely used in obfuscating transformations. We give a survey (including the latest results) on the complexity of equivalence-checking problem in various algebraic models of programs and estimate thus a resilience of some obfuscating transformation commonly employed by metamorphic viruses.
Proceedings of the Institute for System Programming, vol. 12 (in Russian), 2007, Стр. 77-94.
ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).