The Community for Technology Leaders
RSS Icon
Issue No.04 - October-December (2010 vol.7)
pp: 424-438
Stefan Katzenbeisser , Technische Universität Darmstadt, Darmstadt
Christian Schallhart , Technische Universität München, Garching
Helmut Veith , Technische Universität Darmstadt, Darmstadt
Although recent estimates are speaking of 200,000 different viruses, worms, and Trojan horses, the majority of them are variants of previously existing malware. As these variants mostly differ in their binary representation rather than their functionality, they can be recognized by analyzing the program behavior, even though they are not covered by the signature databases of current antivirus tools. Proactive malware detectors mitigate this risk by detection procedures that use a single signature to detect whole classes of functionally related malware without signature updates. It is evident that the quality of proactive detection procedures depends on their ability to analyze the semantics of the binary. In this paper, we propose the use of model checking—a well-established software verification technique—for proactive malware detection. We describe a tool that extracts an annotated control flow graph from the binary and automatically verifies it against a formal malware specification. To this end, we introduce the new specification language CTPL, which balances the high expressive power needed for malware signatures with efficient model checking algorithms. Our experiments demonstrate that our technique indeed is able to recognize variants of existing malware with a low risk of false positives.
Invasive software, model checking.
Stefan Katzenbeisser, Christian Schallhart, Helmut Veith, "Proactive Detection of Computer Worms Using Model Checking", IEEE Transactions on Dependable and Secure Computing, vol.7, no. 4, pp. 424-438, October-December 2010, doi:10.1109/TDSC.2008.74
[1] J. Kinder, S. Katzenbeisser, C. Schallhart, and H. Veith, "Detecting Malicious Code by Model Checking," Proc. Second Int'l Conf. Detection of Intrusions and Malware and Vulnerability Assessment (DIMVA '05), pp. 174-187, 2005.
[2] mi2g Ltd., MyDoom Causes $3 Billion in Damages as SCO Offers $250k Reward, php , 2004.
[3] M. Christodorescu and S. Jha, "Testing Malware Detectors," Proc. ACM/SIGSOFT Int'l Symp. Software Testing and Analysis (ISSTA '04), pp. 34-44, 2004.
[4] F. Cohen, "Computer Viruses: Theory and Experiments," Computers and Security, vol. 6, no. 1, pp. 22-35, Feb. 1987.
[5] J. Newsome, B. Karp, and D.X. Song, "Polygraph: Automatically Generating Signatures for Polymorphic Worms," Proc. IEEE Symp. Security and Privacy (S&P '05), pp. 226-241, 2005.
[6] M.R. Chouchane, A. Walenstein, and A. Lakhotia, "Statistical Signatures for Fast Filtering of Instruction-Substituting Metamorphic Malware," Proc. Fifth ACM Workshop Recurring Malcode (WORM '07), pp. 31-37, 2007.
[7] J.T. Giffin, D. Dagon, S. Jha, W. Lee, and B.P. Miller, "Environment-Sensitive Intrusion Detection," Proc. Eighth Int'l Symp. Recent Advances in Intrusion Detection (RAID '05), pp. 185-206, 2005.
[8] T. Holz, F. Freiling, and C. Willems, "Toward Automated Dynamic Malware Analysis Using CWSandbox," Proc. IEEE Symp. Security and Privacy (S&P '07), pp. 32-39, 2007.
[9] A. Vasudevan and R. Yerraballi, "Cobra: Fine-Grained Malware Analysis Using Stealth Localized-Executions," Proc. IEEE Symp. Security and Privacy (S&P '06), pp. 264-279, 2006.
[10] U. Bayer, A. Moser, C. Krügel, and E. Kirda, "Dynamic Analysis of Malicious Code," J. Computer Virology, vol. 2, no. 1, pp. 67-77, 2006.
[11] K. Natvig, "Sandbox Technology inside AV Scanners," Proc. Virus Bull. Conf., pp. 475-487, Sept. 2001.
[12] A. Moser, C. Kruegel, and E. Kirda, "Exploring Multiple Execution Paths for Malware Analysis," Proc. IEEE Symp. Security and Privacy (S&P '07), pp. 231-245, 2007.
[13] P. Godefroid, N. Klarlund, and K. Sen, "Dart: Directed Automated Random Testing," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI '05), pp. 213-223, 2005.
[14] K. Sen, D. Marinov, and G. Agha, "CUTE: A Concolic Unit Testing Engine for C," Proc. 10th European Software Eng. Conf./13th ACM SIGSOFT Int'l Symp. Foundations of Software Eng. (ESEC/FSE '05), pp. 263-272, 2005.
[15] J. Bergeron, M. Debbabi, J. Desharnais, M. Erhioui, Y. Lavoie, and N. Tawbi, "Static Detection of Malicious Code in Executable Programs," Proc. Symp. Requirements Eng. for Information Security (SREIS), 2001.
[16] P. Singh and A. Lakhotia, "Static Verification of Worm and Virus Behavior in Binary Executables Using Model Checking," Proc. Fourth IEEE Information Assurance Workshop (IAW '03), June 2003.
[17] A. Lakhotia and P. Singh, "Challenges in Getting "Formal" with Viruses," Virus Bull., pp. 15-19, Sept. 2003.
[18] M. Christodorescu and S. Jha, "Static Analysis of Executables to Detect Malicious Patterns," Proc. 12th Usenix Security Symp., pp. 169-186, Aug. 2003.
[19] M. Christodorescu, S. Jha, S.A. Seshia, D.X. Song, and R.E. Bryant, "Semantics-Aware Malware Detection," Proc. IEEE Symp. Security and Privacy (S&P '05), pp. 32-46, 2005.
[20] M. Dalla Preda, M. Christodorescu, S. Jha, and S.K. Debray, "A Semantics-Based Approach to Malware Detection," Proc. 34th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL '07), pp. 377-388, 2007.
[21] E. Clarke and E. Emerson, "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic," Proc. Logics of Programs Workshop, pp. 52-71, 1981.
[22] J.-P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Proc. Int'l Symp. Programming, pp. 337-351, 1982.
[23] E. Clarke, O. Grumberg, and D. Long, Model Checking. MIT Press, 1999.
[24] M. Oberhumer and L. Molnár, Ultimate Packer for eXecutables, http:/, 2008.
[25] Xtreeme, Fast Small Good, http:/, 2008.
[26] M. Christodorescu, S. Jha, J. Kinder, S. Katzenbeisser, and H. Veith, "Software Transformations to Improve Malware Detection," J. Computer Virology, vol. 3, no. 4, pp. 253-265, Nov. 2007.
[27] Hex-Rays SA, IDA Pro, http://www.hex-rays.comidapro/, 2008.
[28] C. Linn and S.K. Debray, "Obfuscation of Executable Code to Improve Resistance to Static Disassembly," Proc. 10th ACM Conf. Computer and Comm. Security (CCS '03), pp. 290-299, 2003.
[29] C. Kruegel, W. Robertson, F. Valeur, and G. Vigna, "Static Disassembly of Obfuscated Binaries," Proc. 13th Usenix Security Symp., pp. 255-270, 2004.
[30] P. Ször, "Attacks on Win32," Proc. Virus Bull. Conf., pp. 47-68, 2000.
[31] P. Ször, The Art of Computer Virus Research and Defense, chapter 7, Addison-Wesley, pp. 251-294, 2005.
[32] E.H. Spafford, "Computer Viruses as Artificial Life," Artificial Life, vol. 1, no. 3, pp. 249-265, 1994.
[33] H. Hungar, O. Grumberg, and W. Damm, "What If Model Checking Must Be Truly Symbolic," Proc. IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME '95), pp. 1-20, 1995.
[34] J. Bohn, W. Damm, O. Grumberg, H. Hungar, and K. Laster, "First-Order-CTL Model Checking," Proc. 18th Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS '98), pp. 283-294, 1998.
[35] J. Kinder and H. Veith, "Jakstab: A Static Analysis Platform for Binaries," Proc. 20th Int'l Conf. Computer Aided Verification (CAV '08), pp. 423-427, 2008.
[36] A. Holzer, J. Kinder, and H. Veith, "Using Verification Technology to Specify and Detect Malware," Proc. 11th Int'l Conf. Computer Aided Systems Theory (EUROCAST '07), pp. 497-504, 2007.
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool