Behavior Analysis of Malware by Rewriting-Based Abstraction

Organisation:	INRIA Nancy Grand Est / LORIA University of Nancy
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Security.
Period:	2011-2012
Size:	n/a
Description:	Behavior analysis detects malware (in particular, of unknown nature) in software applications. In general, a behavior is described by a sequence of system calls and recognition uses the formalism of finite state automata. This work proposes a formal approach for high-level behavior analysis based on language theory, term rewriting, and first-order temporal logic. The approach enables to determine whether a program exhibits a certain malicious high-level behavior. Detection is achieved in two steps. First, traces of the program are abstracted to reveal the sequences of high-level functionalities they realize. Then, abstracted traces are compared with the behavior formula using model-checking techniques. Functionalities have parameters representing the manipulated data, making the approach suitable for the protection against generic threats, like the leak of sensitive information. Behavior pattern abstraction and behavior detection in the presence of data are performed using CADP. The set of traces of a given program is represented by a system of communicating processes expressed in LOTOS, with a particular gate on which communications correspond to library calls. Then, the computation of the abstract set of traces is done by synchronization with another LOTOS process, which simulates the transducer realizing the abstraction. Abstract behaviours denoting several kinds of information leaks (keystroke capture functionality, network send functionality, overwriting or freeing, and dependences) are formulated in FOLTL (First-Order LTL) and subsequently encoded in MCL. The detection of malware is carried out by verifying the resulting MCL formulas on the set of abstract program traces using the EVALUATOR 4.0 model checker. The approach was successfully applied to two case studies: keylogger programs written in C for Windows, and an Android application for cell-phone that maliciously forward received SMS to the attacker.
Conclusions:	The malware detection approach proposed uses an abstracted form for program traces and behaviors, therefore being independent of the program implementation and able to handle similar behaviors in a generic way. The fact that high-level behaviors are combinations of elementary patterns enables to efficiently summarize and compact the possible combinations likely to compose suspicious behaviors. The applicability of the detection approach could be further enhanced by automating the construction of reference behavior patterns, e.g., using data mining techniques.
Publications:	[Beaucamps-Gnaedig-Marion-11] Philippe Beaucamps, Isabelle Gnaedig, and Jean-Yves Marion. "Behavior Analysis of Malware by Rewriting-based Abstraction". Research Report, LORIA, 2011. Available on-line from: http://hal.inria.fr/inria-00594396/en or from the CADP Web site in PDF or PostScript [Beaucamps-11] Philippe Beaucamps. "Analyse de Programmes Malveillants par Abstraction de Comportements". PhD thesis, Institut National Polytechnique de Lorraine, 2011. Available on-line from: http://hal.inria.fr/tel-00646395 or from the CADP Web site in PDF or PostScript [Beaucamps-Gnaedig-Marion-12] Philippe Beaucamps, Isabelle Gnaedig, and Jean-Yves Marion. "Abstraction-Based Malware Analysis Using Rewriting and Model Checking". Proceedings of the 17th European Symposium on Research in Computer Security ESORICS'2012 (Pisa, Italy), LNCS vol. 7459, pages 806-823, Springer Verlag, 2012. Available on-line from: http://hal.inria.fr/hal-00762252/en or from the CADP Web site in PDF or PostScript
Contact:	Jean-Yves Marion LORIA - INPL 615, rue du Jardin Botanique BP-101 F-54602 Villers-lès-Nancy FRANCE Tel: +33 (0)3 54 95 84 60 Email: [email protected] Web: http://www.loria.fr/~marionjy/
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page