Skip to Main content Skip to Navigation
Conference papers

Abstraction-based Malware Analysis Using Rewriting and Model Checking

Philippe Beaucamps 1 Isabelle Gnaedig 1, * Jean-Yves Marion 1
* Corresponding author
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We propose a formal approach for the detection of high-level malware behaviors. Our technique uses a rewriting-based abstraction mechanism, producing abstracted forms of program traces, independent of the program implementation. It then allows us to handle similar be- haviors in a generic way and thus to be robust with respect to variants. These behaviors, defined as combinations of patterns given in a signa- ture, are detected by model-checking on the high-level representation of the program. We work on unbounded sets of traces, which makes our technique useful not only for dynamic analysis, considering one trace at a time, but also for static analysis, considering a set of traces inferred from a control flow graph. Abstracting traces with rewriting systems on first order terms with variables allows us in particular to model dataflow and to detect information leak.
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download
Contributor : Isabelle Gnaedig <>
Submitted on : Monday, December 10, 2012 - 4:36:26 PM
Last modification on : Tuesday, December 18, 2018 - 4:48:02 PM
Document(s) archivé(s) le : Monday, March 11, 2013 - 11:25:35 AM


Files produced by the author(s)




Philippe Beaucamps, Isabelle Gnaedig, Jean-Yves Marion. Abstraction-based Malware Analysis Using Rewriting and Model Checking. ESORICS - 17th European Symposium on Research in Computer Security - 2012, Sep 2012, Pisa, Italy. pp.806-823, ⟨10.1007/978-3-642-33167-1⟩. ⟨hal-00762252⟩



Record views


Files downloads