Using algebraic models of programs for detecting metamorphic malwares

R. I. Podlovchenko ; N. N. Kuzyurin ; V. S. Shcherbina ; V. A. Zakharov

Fundamentalʹnaâ i prikladnaâ matematika, Tome 15 (2009) no. 5, pp. 181-198.

Résumé

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 antivirus 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.

Bibliographie

[1] Godlevskii A. B., “Nekotorye spetsialnye sluchai problemy ostanovki i funktsionalnoi ekvivalentnosti avtomatov”, Kibernetika, 1973, no. 4, 90–97 | MR | Zbl

[2] Godlevskii A. B., “Ob odnom razreshimom sluchae spetsialnoi problemy funktsionalnoi ekvivalentnosti diskretnykh preobrazovatelei”, Kibernetika, 1974, no. 3, 32–36 | MR

[3] Zakharov V. A., “Avtomatnye modeli programm”, DAN SSSR, 309:1 (1989), 24–27 | MR

[4] Zakharov V. A., “Ob odnom kriterii sravnimosti operatornykh formalnykh modelei programm”, Programmirovanie, 1993, no. 4, 12–25 | MR | Zbl

[5] Letichevskii A. A., “Ekvivalentnost avtomatov otnositelno svobodnoi polugruppy s pravym nulëm”, Dokl. AN USSR, 182:5 (1968), 248–252

[6] Letichevskii A. A., “Ekvivalentnost avtomatov otnositelno polugrupp”, Teor. kibernetika, 1970, no. 6, 3–71 | MR

[7] Letichevskii A. A., Smikun L. B., “O klassakh grupp s razreshimoi problemoi ekvivalentnosti avtomatov”, DAN SSSR, 17:2 (1976), 341–344

[8] Petrosyan G. N., “Ob odnom bazise operatorov i predikatov s nerazreshimoi problemoi pustoty”, Kibernetika, 1974, no. 5, 23–28 | Zbl

[9] Podlovchenko R. I., “Ierarkhiya modelei programm”, Programmirovanie, 1981, no. 2, 3–14 | MR | Zbl

[10] Podlovchenko R. I., “Polugruppovye modeli programm”, Programmirovanie, 1981, no. 4, 3–13 | MR | Zbl

[11] Podlovchenko R. I., “Ekvivalentnye preobrazovaniya skhem programm dlya “zaputyvaniya” samikh programm”, Programmirovanie, 28:2 (2002), 106–116 | MR | Zbl

[12] Podlovchenko R. I., “O skhemakh programm s perestanovochnymi i monotonnymi operatorami”, Programmirovanie, 29:5 (2003), 270–276 | MR | Zbl

[13] Podlovchenko R. I., Zakharov V. A., “Polinomialnyi po slozhnosti algoritm, raspoznayuschii kommutativnuyu ekvivalentnost skhem programm”, Dokl. RAN, 362:6 (1998), 744–747 | MR | Zbl

[14] Barak B., Goldreich O., Impagliazzo R., Rudich S., Sahai A., Vedhan S., Yang K., “On the (im)possibility of obfuscating programs”, CRYPTO' 01 – Advances in Cryptology, Lect. Notes Comput. Sci., 2139, Springer, 2001, 1–18 | DOI | MR | Zbl

[15] Chess D., White S., “An undetectable computer virus”, Proc. of the 2000 Virus Bulletin Conference, 2000

[16] Chow S., Gu Y., Johnson H., Zakharov V. A., “An approach to the obfuscation of control-flow of sequential computer programs”, 6th Inf. Security Conf., Lect. Notes Comput. Sci., 2200, Springer, 2001, 144–155 | DOI | Zbl

[17] Christodorescu M., Jha S., “Static analysis of executables to detect malicious patterns”, Proc. of the 12th USENIX Security Symposium (Security' 03), 2003, 169–186

[18] Christodorescu M., Jha S., “Testing malware detectors”, Proc. of the Int. Symp. on Software Testing and Analysis (ISSTA 2004), 2004

[19] Christodorescu M., Jha S., Seshia S. A., Song D., Bryant R. E., “Semantics-aware malware detection”, Proc. of the 2005 IEEE Symp. on Security and Privacy (Oakland 2005), 2005, 32–46 | DOI | MR

[20] Collberg C., Thomborson C., Low D., A taxonomy of obfuscating transformations, Tech. Report No 148, Univ. of Auckland, 1997

[21] Collberg C., Thomborson C., Low D., “Manufacturing cheap, resilient and stealthy opaque constructs”, Symp. on Principles of Programming Languages, 1998, 184–196

[22] Cousot P., Cousot R., “An abstract interpretation-based framework for software watermarking”, Conf. Record of the 31st ACM SIGACT-SIGMOD-SIGART Symp. on Principles of Programming Languages, 2004, 173–185

[23] Dalla Preda M., Giacobazzi R., “Semantic-based code obfuscation by abstract interpretation”, Automata, Languages and Programming, Lect. Notes Comput. Sci., 3580, Springer, 2005, 1325–1336 | DOI | MR | Zbl

[24] Dalla Preda M., Giacobazzi R., Madou M., de Bosschere B., “Opaque predicate detection by means of abstract interpretations”, Proc. of 11th Int. Conf. on Algebraic Methodology and Software Technology (AMAST06), Lect. Notes Comput. Sci., 4019, Springer, 2006, 81–95 | DOI | Zbl

[25] Harju T., Karhumaki J., “The equivalence of multi-tape finite automata”, Theor. Comput. Sci., 78 (1991), 347–355 | DOI | MR | Zbl

[26] Hopcroft J. E., Karp R. M., A linear algorithm for testing equivalence of finite automata, Technical Report TR 71-114, Cornell Univ., Comput. Sci. Dep., 1971

[27] Ianov Iu. I., “On the equivalence and transformation of program schemes”, Comm. ACM, 1:10 (1958), 8–12 | DOI

[28] Ivanov K. S., Zakharov V. A., “Program obfuscation as obstruction of program static analysis”, Proc. of the Inst. for System Programming, 6, 2004, 141–161

[29] Kaspersky E., Virus List Encyclopedia, Kaspersky Lab., 2002

[30] Marx A., “A guideline to anti-malware-software testing”, Proc. of the 9th Ann. European Institute for Computer Antivirus Research Conference (EICAR' 00), 2000

[31] McGrow G., Morriset G., “Attacking malicious code: report to the Infosec research council”, IEEE Software, 17:5 (2000), 33–41 | DOI

[32] Nachenberg C., Understanding and managing polymorphic viruses, The Symantec Enterprise Papers, 30, 1996

[33] Nachenberg C., “Computer virus-antivirus coevolution”, Comm. ACM, 40:1 (1997), 46–51 | DOI

[34] Podlovchenko R. I., Rusakov D., Zakharov V., “On the equivalence problem for programs with mode switching”, Conf. on the Implementation and Application of Automata, Lect. Notes Comput. Sci., 3845, Springer, 2006, 351–352 | DOI | Zbl

[35] Rutledge J. D., “On Ianov's program schemata”, J. ACM, 11:1 (1964), 1–9 | DOI | MR | Zbl

[36] Sampson T., “A virus in info-space: the open network and its enemies”, J. Media Culture, 7:3 (2004)

[37] Spinellis D., “Reliable identification of bounded-length viruses is NP-complete”, IEEE Trans. Inform. Theory, 49:1 (2003), 280–284 | DOI | MR | Zbl

[38] Szor P., Ferrie P., “Hunting for metamorphic”, Proc. of the 2001 Virus Bulletin Conference, 2001, 123–144

[39] Varnovsky N. P., Zakharov V. A., “On the possibility of probably secure obfuscating programs”, 5th Conf. “Perspectives of System Informatics”, Lect. Notes Comput. Sci., 2890, Springer, 2004, 91–102 | DOI

[40] Zakharov V. A., “An efficient and unified approach to the decidability of equivalence of propositional program schemes”, Automata, Languages, and Programming, Proc. of ICALP' 98 (Aalborg, Denmark, July 13–17, 1998), Lect. Notes Comput. Sci., 1443, Springer, 1998, 247–258 | DOI | MR

[41] Zakharov V. A., “On the decidability of the equivalence problem for monadic recursive programs”, Theor. Inform. Appl., 34:2 (2000), 157–171 | DOI | MR | Zbl

[42] Zakharov V. A., “The equivalence problem for computational models: decidable and undecidable cases”, Machines, Computations, and Universality, Lect. Notes Comput. Sci., 2055, Springer, 2001, 133–153 | DOI | MR

[43] Zakharov V. A., Zakharyaschev I. M., “On the equivalence checking problem for a model of programs related with multi-tape automata”, Conf. on Implementation and Application of Automata, Lect. Notes Comput. Sci., 3317, Springer, 2005, 293–305 | DOI | MR | Zbl