Abstract
Over the past decade, malware costs more than $10 billion every year and the cost is still increasing. Classical signature-based and emulation-based methods are becoming insufficient, since malware writers can easily obfuscate existing malware such that new variants cannot be detected by these methods. Thus, it is important to have more robust techniques for malware detection. In our previous work [24], we proposed to use model-checking to identify malware. We used pushdown systems (PDSs) to model the program (this allows to keep track of the program’s stack behavior), and we defined the SCTPL logic to specify the malicious behaviors, where SCTPL can be seen as an extension of the branching-time temporal logic CTL with variables, quantifiers, and predicates over the stack. Malware detection was then reduced to SCTPL model-checking of PDSs. However, in our previous work [24], the way we used SCTPL to specify malicious behaviors was not very precise. Indeed, we used the names of the registers and memory locations instead of their values. We show in this work how to sidestep this limitation and use precise SCTPL formulas that consider the values of the registers and memory locations to specify malware. Moreover, to make the detection procedure more efficient, we propose an abstraction that reduces drastically the size of the program model, and show that this abstraction preserves all SCTPL∖X formulas, where SCTPL∖X is a fragment of SCTPL that is sufficient to precisely characterize malware specifications. We implemented our techniques in a tool and applied it to automatically detect several malwares. The experimental results are encouraging.
Work partially funded by ANR grant ANR-08-SEGI-006.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Avast. Free avast antivirus, http://www.avast.com , Version 6.0.1367
Avira, http://www.avira.com , Version 12.0.0.849
Babić, D., Reynaud, D., Song, D.: Malware Analysis with Tree Automata Inference. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 116–131. Springer, Heidelberg (2011)
Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., Teitelbaum, T.: Model Checking x86 Executables with CodeSurfer/x86 and WPDS++. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 158–163. Springer, Heidelberg (2005)
Bergeron, J., Debbabi, M., Desharnais, J., Erhioui, M., Lavoie, Y., Tawbi, N.: Static detection of malicious code in executable programs. In: SREIS (2001)
Bonfante, G., Kaczmarek, M., Marion, J.-Y.: Architecture of a Morphological Malware Detector. Journal in Computer Virology 5, 263–270 (2009)
Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. In: 12th USENIX Security Symposium, pp. 169–186 (2003)
Christodorescu, M., Jha, S., Seshia, S.A., Song, D.X., Bryant, R.E.: Semantics-aware malware detection. In: IEEE Symposium on Security and Privacy, pp. 32–46 (2005)
Eric, S.: 10 most destructive computer worms and viruses ever (2010), http://wildammo.com/2010/10/12/10-most-destructive-computer-worms-and-viruses-ever
Esparza, J., Schwoon, S.: A BDD-Based Model Checker for Recursive Programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)
Gostev, A.: Kaspersky security bulletin, malware evolution. Kaspersky Lab ZAO (2010), http://www.securelist.com/en/analysis/204792161/Kaspersky_Security_Bulletin_Malware_Evolution_2010
Heavens, V.: http://vx.netlux.org
Hex-Rays. IDAPro (2011)
Holzer, A., Kinder, J., Veith, H.: Using Verification Technology to Specify and Detect Malware. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 497–504. Springer, Heidelberg (2007)
Kaspersky, http://www.kaspersky.com , Version 12.0.0.374
Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting Malicious Code by Model Checking. In: Julisch, K., Kruegel, C. (eds.) DIMVA 2005. LNCS, vol. 3548, pp. 174–187. Springer, Heidelberg (2005)
Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Proactive detection of computer worms using model checking. IEEE Trans. on Dependable and Secure Computing 7(4) (2010)
Kinder, J., Veith, H.: Jakstab: A Static Analysis Platform for Binaries. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 423–427. Springer, Heidelberg (2008)
Lakhotia, A., Boccardo, D.R., Singh, A., Manacero, A.: Context-sensitive analysis of obfuscated x86 executables. In: PEPM (2010)
Lakhotia, A., Kumar, E.U., Venable, M.: A method for detecting obfuscated calls in malicious binaries. IEEE Trans. Software Eng. 31(11) (2005)
Qihoo 360, http://www.360.cn
Singh, P.K., Lakhotia, A.: Static verification of worm and virus behavior in binary executables using model checking. In: IAW, pp. 298–300 (2003)
Song, F., Touili, T.: Efficient Malware detection using model-checking. Research report (2012), http://www.liafa.jussieu.fr/~song/full.pdf
Song, F., Touili, T.: Pushdown Model Checking for Malware Detection. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 110–125. Springer, Heidelberg (2012)
Wong, W.: Analysis and detection of metamorphic computer viruses. Master’s thesis, San Jose State University (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Song, F., Touili, T. (2012). Efficient Malware Detection Using Model-Checking. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-32759-9_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32758-2
Online ISBN: 978-3-642-32759-9
eBook Packages: Computer ScienceComputer Science (R0)