Pommade
A ModelChecker for Malware Detection
Introduction 
PoMMaDe is a malware detector based on Pushdown ModelChecking 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 ModelChecking 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 modelchecking). Otherwise, Model Builder is called (we need to apply modelchecking 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 modelchecking, 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. ModelChecking Engines takes as input the PDS from Model Builder and performs modelchecking 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.
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.hexrays.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.
cudd2.4.2 is in PoMMaDe. Uptodate versions can be obtained from the CU Decision Diagram Package . Use the following commands to install CUDD.
tar zxvf PuMoC.tar.gz
cd PuMoC/cudd2.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 cudd2.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 libcstl2.0.1. Uptodate 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
After installing the above libraries and PoMMaDe , you can evaluate an example by the following commands:
./pommade l3fI2 malware/EmailWorm.Win32.NetSky.a formulas/sp.ctpl
Here the file malware/EmailWorm.Win32.NetSky.a is an emailworm, formulas/sp.ctpl contains a SCTPL formula that specifies the selfpropagation 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 modelchecking using the following commands:
./pommade l5fI2 malware/EmailWorm.Win32.NetSky.a formulas/sp.ltpl
The results are shown in the following figures.
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  FSecure 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%

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

Eo x if x is used in atomic predicates


∀x

As x if x is used in regular variable expressions

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.
identiﬁer

[azAZ09][azAZ09 $:]


+

+

·

.

Γ



*

*

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) ) )
<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 modelchecking with regular valuations for pushdown systems
In: Specify the filter strategy: direct strategy, or keywords strategy or sequence strategy.
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.
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.
[TACAS12] Fu Song and Tayssir Touili. Pushdown ModelChecking for Malware Detection. In TACAS 2012. [ PDF]
[FM12] Fu Song and Tayssir Touili. Efficient Malware Detection Using ModelChecking. In FM 2012. [ PDF]
[TACAS13] Fu Song and Tayssir Touili. LTL ModelChecking for Malware Detection. In TACAS 2013. [ PDF]
[ESECFSE] Fu Song and Tayssir Touili. POMMADE:PushdOwn Modelchecking for Malware DEtection. In ESEC/FSE 2013. [ PDF]
[STTT13] Fu Song and Tayssir Touili. Pushdown ModelChecking for Malware Detection. In STTT 2013. [ PDF]
Contact: PoMMaDe is written and maintained by Fu Song.