Pommade

A Model-Checker for Malware Detection

Introduction

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 formulas, PoMMaDe outputs Yes if the program satisfies one of the formulas. 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, it uses the corresponding unpacker (if it exists) to unpack the binary code and feed the resulting binary program to Oracle. Otherwise, it directly passes 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 strategy 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 Binary

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

All the experiments were run on a Linux platform (Fedora 13) with a 2.4GHz CPU, 2GB of memory. The time limit is fixed to 20 minutes.

Detecting Real Malwares:
PoMMaDe is applied to check more than 600 real malwares and 400 benign programs taken from Microsoft Windows System. PoMMaDe can detect all the real malwares and prove benign program are benign. In particular, our tool can detect the malware Flame, the most complex attack toolkit which can record audio conversations, intercept the keyboard, etc. Flame has been active for more that 5 years and was not detected by any antivirus.

The average time (resp. memory) of checking one malware against the satisfiable formula is 93.57 seconds (resp. 225.15 MB). The average time (resp. memory) of checking one benign program against all the malicious behaviors we considered is 24.73 seconds (resp. 21.86 MB) (Thanks to Filter, PoMMaDe does not need to apply model-checking for many benign programs).

PoMMaDe vs Existing Antiviruses:

To compare our tool with the well-known existing anti-viruses, and show its robustness, we automatically created 200 new malwares using the generators NGVCK and VCL32. [Wong06] showed that these systems are the best malware generators. These programs use very sophisticated features such as anti-disassembly, anti-debugging, anti-emulation, and anti-behavior blocking and come equipped with code morphing ability
which allows them to produce different-looking viruses. Our results are reported in the following Table. PoMMaDe was able to detect all these 200 malwares, whereas several well-known and widely used anti-viruses such as Avira, Kaspersky, Avast, Qihoo 360, McAfee, AVG, BitDefende, Eset Nod32, F-Secure, Norton, Panda and Trend Micro were not able to detect several of them.

Generator	Number of Variants	PoMMaDe	Avira Detection Rate	Kaspersky Detection Rate	Avast Detection Rate	Qihoo 360 Detection Rate	McAfee Detection Rate	AVG Detection Rate	BitDefende Detection Rate	Eset Nod32 Detection Rate	F-Secure Detection Rate	Norton Detection Rate	Panda Detection Rate	Trend Micro Detection Rate
NGVCK	100	100%	0%	23%	18%	68%	100%	11%	97%	0%	68%	46%	0%	0%
VCL32	100	100%	0%	2%	100%	99%	0%	100%	100%	0%	99%	30%	0%	0%

Manual

To be able to use the PoMMaDe, you need to be familiar with the syntax of the logics SCTPL and SLTPL. Please see [ST12a], [ST12b] and [ST13] for the formal definition of these logics.

The implementation of SCTPL and SLTPL operators in PoMMaDe:

SCTPL/SLTPL Operators	Corresponding Operators in POMMADE
Atomic predicate	b(p1, ..., pn)
Regular predicate	#e#
¬	!
�?	\|\|
�?	&&
�?/span>x	Es x if x is used in regular variable expressions
�?/span>x	Eo x if x is used in atomic predicates
∀x	As x if x is used in regular variable expressions
∀x	Ao x if x is used in atomic predicates
X	X
F	F
G	G
U	U
R	W
A	A
E	E

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 (number or string), then pi should be 'n. (For example, if pi is the constant 100, we write '100). Otherwise, we know that pi is a variable.

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

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

identiﬁer	[a-zA-Z0-9][a-zA-Z0-9 $:]
+	+
·	.
Γ	\|
*	*

For example, 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.|*#) )

The SLTPL formula G ( F ( ∃x cmp(x, 5A4Dh) �?F ∃y cmp(y, 4550h) ) ) will be in PoMMaDe syntax as follows:

G ( F ( Eo x cmp(x, 5A4Dh) �?F Eo y cmp(y, 4550h) ) )

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 a SLTPL formula into a LTL formula with regular valuations, then apply LTL model-checking with regular valuations for pushdown systems

-A: Enable abstraction w.r.t. the specification (more details about the abstraction can be found in [ST12b]).
-o: Output the pushdown system modelling the binary program.
-In: Specify the filter strategy: direct strategy, or keywords strategy or sequence strategy.
-n=0: direct strategy, default.
-n=1: The strategy is keywords 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 a SCTPL formula.
-n=5: SLTPL model checking, i.e, the formula is a SLTPL formula.

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. [ PDF]
[ESECFSE] Fu Song and Tayssir Touili. POMMADE:PushdOwn Model-checking for Malware DEtection. In ESEC/FSE 2013. [ PDF]
[STTT13] Fu Song and Tayssir Touili. Pushdown Model-Checking for Malware Detection. In STTT 2013. [ PDF]

Contact: PoMMaDe is written and maintained by Fu Song.