PoMMaDe -- A PushdOwn Model-checker for MAlware DEtection

Introduction

PoMMaDe is a malware detector based on Pushdown Model-Checking techniques. Given a binary program, and a set of malicious behaviors expressed by SCTPL or SLTPL, PoMMaDe outputs Yes if the program satisfies one formula. It means that the binary program may be a malware. Otherwise, PoMMaDe outputs No meaning that the binary program is benign. As shown in the following figure, PoMMaDe consists of five components: Preprocessor, Oracle, Filter, Model Builder and Model-Checking Engines.

Preprocessor uses PEfile to check whether the binary program is packed or not. If this is the case, we use the corresponding unpacker (if it exists) to unpack the binary code and feed the resulting binary program to Oracle. Otherwise, we directly pass the binary code to Oracle. So far, PoMMaDe supports dozens of popular packers for Windows, and hundreds of packers for Linux. Moreover, users can easily add a new unpacking tool by modifying the database file. Oracle takes as input a (unpacked) binary program and outputs the assembly program, and the informations of API functions and the states (values of the registers and memory addresses at each control point). Oracle relies on Jakstab and IDA Pro. Jakstab performs static analysis of the binary program, provides an assembly program and the states. However, it does not allow to extract the informations of API functions and some indirect calls to the API functions. Oracle uses IDA Pro to get these informations. The outputs of Oracle are used by Filter to filter out benign programs P according to the given optimization strategies by ``syntactically" checking the assembly program. PoMMaDe provides three strategies: (1) keywords strategy, (2)sequence strategy and (3) direct strategy. When ``keywords strategy" is chosen, the user has to provide a set of instructions to PoMMaDe. Filter will syntactically check whether or not the assembly program contains these instructions. If this is not the case, PoMMaDe outputs No (we know that P does not contain this malicious behavior, no need to apply model-checking). Otherwise, Model Builder is called (we need to apply model-checking to decide whether P is a malware or not). When ``sequence strategy" is chosen, the user has to provide a sequence of instructions to PoMMaDe. Filter will ``syntactically" check in the control flow graph of the assembly program whether or not these instructions occur in the same order as in the sequence. If this is not the case,PoMMaDe outputs No (no need to apply model-checking, P is benign). Otherwise, Model Builder is called. If ``direct strategy" is chosen, Model Builder is directly called.Model Builder outputs a PDS modeling the assembly program. Model-Checking Engines takes as input the PDS from Model Builder and performs model-checking of the PDS against all the formulas given by the user. If there is one formula satisfied by the PDS, PoMMaDe outputs Yes. Otherwise PoMMaDe outputs No.

Download

PoMMaDe has been tested mainly on Linux distributions.

Tips for installing PoMMaDe on Linux.

PoMMaDe relies on a commerical tool IDA Pro and several open source tools (CUDD, libcstl and Jakstab). After downloading the source code of PoMMaDe, these tools have to be installed.

IDA Pro is a disassembler. You can get it here http://www.hex-rays.com/products/ida/index.shtml and put IDA Pro in the directory of PoMMaDe. After that, replace the file /IDAPRO/ida/idc/analysis.idc by our file analysis.idc, the file /IDAPRO/ida/idc/idc.idc by idc.idc.

cudd-2.4.2 is in PoMMaDe. Up-to-date versions can be obtained from the CU Decision Diagram Package . Use the following commands to install CUDD.

tar -zxvf PuMoC.tar.gz

cd PuMoC/cudd-2.4.2

make

Copy object files libcudd.a, libepd.a, libmtr.a, libst.a, libutil.a from the directory cudd, epd, mtr, st, util to the directory lib in cudd-2.4.2 by the following commands:

cp -i cudd/libcudd.a lib/

cp -i epd/libepd.a lib/

cp -i mtr/libmtr.a lib/

cp -i st/libst.a lib/

cp -i util/libutil.a lib/

libcstl is an open source library implementing STL library in C. PoMMaDe is equipped with libcstl-2.0.1. Up-to-date versions can be obtained from https://github.com/activesys/libcstl. Use the following commands to instal libcstl:

./configure --prefix=/.../pommade/libcstl

make

Jakstab is static analysis tool for X86 binaries. PoMMaDe is equipped with Jakstab. Compile compile.sh or compile.bat to install Jakstab.

Now, you can install PoMMaDe by the commands:

cd..

make

 

QuickStart

After installing the above libraries and PoMMaDe , you can evaluate an example by the following commands:

./pommade -l3fI2 malware/Email-Worm.Win32.NetSky.a formulas/sp.ctpl

Here the file malware/Email-Worm.Win32.NetSky.a is an email-worm, formulas/sp.ctpl contains a SCTPL formula that specifies the self-propagation behavior. -l3 specifies that the formula is in SCTPL. I2 specifies that the filter strategy is sequence strategy. The results are shown in the following figures.

PoMMaDe also supports SLTPL model-checking using the following commands:

./pommade -l5fI2 malware/Email-Worm.Win32.NetSky.a formulas/sp.ltpl

The results are shown in the following figures.

Experiments

PoMMaDe was able to detect more than 600 real malwares.

PoMMaDe is also applied to check 200 new malware generated by two malware generators NGVCK and VCL32. NGVCK and VCL32 are the best malware generators as shown in [Won06]. Malwares created by NGVCK and VCL32 use very sophisticated features such as anti-disassembly, antidebugging, anti-emulation, and anti-behavior blocking and come equipped with code morphing ability which allows them to produce different-looking viruses. PoMMaDe can detect all of these new malware, while several of them are not detected by several well-known anti-viruses such as Avira, Kaspersky, Avast, Qihoo 360, McAfee, AVG, BitDefende, Eset Nod32, F-Secure, Norton, Panda and Trend Micro.

Manual

The usage of PoMMaDe is as follows: pommade [-<options>] <modelfile> <formula>

<modelfile> should be a binary program. <formula> is either a SCTPL formula or SLTPL formula.

The options of PoMMaDe are as follows:

-n: Translate SLTPL formula into LTL formula with regular valuations, then apply LTL model-checking with regular valuations for pushdown systems

-A: Enable abstraction w.r.t. the specification.
-o: Output the pushdown system modelling the binary program.

-In: Specify the filter strategy: no strategy, or keyword strategy or sequence strategy.
-n=0: No strategy, default.
-n=1: The strategy is keyword strategy.
-n=2: The strategy is sequence strategy.

-ln: Specify the type of model checking.
-n=3: SCTPL model checking, i.e, the formula is in SCTPL logic.
-n=5: SLTPL model checking, i.e, the formula is in SLTPL logic.

The implementation of SCTPL and SLTPL operators in PoMMaDe.

Note that in the atomic predicate b(p1,...,pn), b is the operator of the instruction, p1,...,pn are operands of the instruction. If pi denotes some constant n, then pi='n. Otherwise, pi is a variable.

In the atomic predicate #e# , e is a regular expression defined as follows.

The syntax of regular variable expression (Regular Valuations) in PoMMaDe.

For example, the SCTPL formula, the SCTPL formula ∃x EF ( call(GetModuleFileNameA) ∧ 0xΓ*∧ EF(call(CopyFileA) ∧ xΓ*) ) will be in PoMMaDe syntax as follows:

Es x EF( call(GetModuleFileNameA) && 0.x.|*&& EF(call(CopyFileA) && x.|*) )

References

[TACAS12] Fu Song and Tayssir Touili. Pushdown Model-Checking for Malware Detection. In TACAS 2012. [ PDF]

[FM12] Fu Song and Tayssir Touili. Efficient Malware Detection Using Model-Checking.   In FM 2012. [ PDF]

[TACAS13] Fu Song and Tayssir Touili. LTL Model-Checking for Malware Detection.   In TACAS 2013.

[ESECFSE] Fu Song and Tayssir Touili. POMMADE:PushdOwn Model-checking for Malware DEtection.   In ESEC/FSE 2013.

[STTT13] Fu Song and Tayssir Touili. Pushdown Model-Checking for Malware Detection.   In STTT 2013.

Contact: PoMMaDe is written and maintained by Fu Song and Tayssir Touili.

Copyright © 2012-2013 LIAFA, University of Paris Diderot and CNRS.