Home

Overview

SMODIC is a model checker for self-modifying binary code. SMODIC uses Self Modifying Pushdown Systems (SM-PDS)[1][2] to model self-modifying binary code. This allows to faithfully represent the program's stack as well as the self-modifying instructions of the program. SMODIC takes a self-modifying binary code or a self modifying pushdown system as input. It can then perform reachability analysis and LTL/CTL model-checking for these models. We successfuly used SMODIC to model-check more than 900 self-modifying binary codes. In particular, we applied SMODIC for malware detection, since malwares usually use self-modifying instructions, and since malicious behaviors can be described by LTL or CTL formulas. In our experiments, SMODIC was able to detect 895 malwares and to prove that 22 benign programs were benign. SMODIC was also able to detect several malwares that well-known antiviruses such as Bit-Defender, Kinsoft, Avira, eScan, Kaspersky, Baidu, Avast, and Symantec failed to detect.

Architecture

The Architecture of SMODIC is shown in the Figure below.

SMODIC takes as input either a binary program or a SM-PDS. SMODIC can perform both reachability analysis and LTL/CTL model checking.

If the input of SMODIC is a binary program, it is passed to the component Oracle. This component is based on the disassembler Jakstab. It takes as input a binary program, and outputs its corresponding assembly program, its corresponding Control Flow Graph (CFG) equipped with the assembly instructions corresponding to each edge, together with informations about the called API functions, and the different values of the registers and memory addresses at each control point (state). All these outputs are fed to the component Model Builder that will compute the corresponding SM-PDS. The Reachability component takes as input a SM-PDS, and a sequence of API functions, and checks whether the SM-PDS has a run that calls these API functions in this order. For example, if we consider the sequence f1, f2, f3, then the Reachability component checks whether the SM-PDS has a run that calls first f1, then f2, then f3. The LTL component takes as input a SM-PDS and an LTL formula, and checks whether the SM-PDS satisfies the LTL formula. Similarly, the CTL component takes as input a SM-PDS and a CTL formula, and checks whether the SM-PDS satisfies the CTL formula.

Downloads

SMODIC can be obtained here: SMODIC.

It uses the following libraries:

Manual

To be able to use the SMODIC, you need to be familiar with the syntax of the logics LTL and CTL. The implementation of LTL and CTL operators in SMODIC are as follows:

Operators for LTL formulas
Propositonal Symbols:	true
	false
	any lowercase string
Boolean operators	! (negation)

	<-> (equivalence)
	&& (and)
	\|\| (or)
Temporal operators	[] p (p always holds)
	<> p (eventually p holds)
	p U q (p holds until q holds)
	X p (p holds next time)

Operators for CTL Formulas
Propositonal Symbols:	tt（true）
	ff(false)
	any lowercase string
Path quantifiers	A (for all paths)
Path quantifiers	E (there exists a path)
Boolean operators	! (negation)
	&& (and)
	\|\| (or)
Temporal operators	Xp (p holds next time)
	pRq (p holds until q does't hold)
	pUq (p holds until q holds)

Quick Start

After downloading the above file, we can execute SMODIC by the following commands

./SMODIC < option1 > < modelfile > < option2 > < formula >

Option1 specifies the input file of SMODIC:
- -M: the input is a SM-PDS model.
- -B: the input is a binary program
Option2 specifies the model checking strategy:
- -L: use the LTL model checking algorithm
- -C: use the CTL model checking algorithm
- -R1: perform the Reachability Analysis using pre*
- -R2: perform the Reachability Analysis using post*
The model file can be either a program or a SM-PDS (.smpds file). The output have three files: one for the Control Flow Graph, one for assembly codes, and one for the generated SM-PDS. A SM-PDS consists of four parts: a finite set of standard PDS transition rules, a finite set of self-modifying transition rules, an initial phase (the initial set of transition rules) and an initial configuration (initial control location equipped with the stack contents).
In order to show this, we will use the following command to check whether the program cmd.exe can eventually call the API function GetModuleA or not. For this case, we execute the following command:
./SMODIC B cmd.exe L "< > getmodulea"

Here is the snapshot of the command to start SMODIC. In this command, “B" is Option1 specifying that the input is a binary program. ”L" specifies that the strategy of model checking is LTL.< > getmodulea is the LTL formula F (call GetModuleA).

Reachability Analysis in SMODIC

Let us show how to use SMODIC to perform reachability analysis on SMPDSs and self-modifying code. To start the reachability analysis, we need to specify the options. Let us consider Option1 B, and Option2 R2(or R1). We also need to specify the sequence of API functions. For example, to perform the reachability analysis on the sequence of API functions "Call GetModuleA", "Call CopyFile" , "call SendFile", we put the names of the functions in lowercase and use the symbol ";" to separate the names. To use the post* approach to check whether the above sequence of API functions can be reached or not, we use the following command(see the following figure): ./SMODIC B malware/cmd.exe R2 getmodulea;copyfile;sendfile

The result is shown in the figure below:

LTL/CTL Model Checking in SMODIC

We show how to apply LTL/CTL model checking to malware detection. Let us take a spy worm as example. Such a worm can record data and send it using the Socket API functions. For example, Keylogger is a spy worm that can record the keyboard states by calling the API functions GetAsyKeyState and GetKeyState and send this to the specific server by calling the socket function sendto. This behavior can be specified by the following LTL formula: F ((call GetAsyncKeyState ∨ call GetRawInputData)∧ F( call sendto ∨call send)). To check whether the program cmd.exe satisfies this formula or not, first, we need to rewrite this formula to the form supported by our tool SMODIC. Because all the propositions are lowercase strings, we rewrite API function calls (like call GetAsyncKeyState) by removing the word "call" and changing the name of the function in lowercase string. The operators are in spin syntax. Thus, the formula is rewritten as:
< > ((getasynckeystate || getrawinputdata)&& < > ( sendto || send))

So, we can check whether the program cmd.exe satisfies this formula or not by using the following command (shown in the figure above):

./SMODIC B malware/cmd.exe L "< > ((getasynckeystate || getrawinputdata)&& < >( sendto || send))".
The result is shown in the figure below. The result of the computation is that there is no accepting run. The output of the tool is No, i.e. cmd.exe is not a spyware.

References

[1] Tayssir Touili and Xin Ye. "Reachability analysis of self modifying code." 22nd International Conference on Engineering of Complex Computer Systems (ICECCS). IEEE, 2017.
[2] Tayssir Touili and Xin Ye. "LTL model checking of self modifying code." 24th International Conference on Engineering of Complex Computer Systems (ICECCS). IEEE, 2019.

SMODIC