Malware is a constant threat for the security of devices and users. Successful and automatic malware detection is a critical necessity [1]. Existing malware detection solutions cannot accurately characterize the behavior of a malware and, thereby, they rely on other indicators, e.g., digital signatures. Nevertheless, behavior-based detection is an active field of research since it can deal with zero-day malware. Although many proposals leveraging machine learning (ML) classifiers have been put forward, finding proper behavioral features is still an open problem. Existing solutions typically consider either static or dynamic software features. Static refers to the program syntax while dynamic refers to features observed at runtime. However, both of them sufer from limitations which impact on the efectiveness of the ML classification.
Malware is one of the main threats that come along with the difusion and growth of digital
technologies. In the past few years, we have observed a dramatic rise of malware attacks also in
the context of cyberespionage and sabotage [
In principle, to efectively detect a malware, we should consider its behavior to understand whether it carries our malicious operations. Nevertheless, finding a suitable definition of malware behavior is non trivial. An approach followed by most authors is to consider API calls. Under reasonable assumptions, APIs are the only way for a software to interact with the underlying operating systems and its resources, e.g., to read files and open connections. Thus, most of the malicious operations carried out by a piece of malware involve one or more APIs.
There are two ways to inspect how APIs are used by a software. Static approaches are based on code analysis and do not require program execution. On the other hand, dynamic approaches observes the API invocations performed during one or more executions of the target binary inside a sandbox environment. Nevertheless, these approaches have some serious limitations. As a matter of fact, in most cases static analysis cannot deal with runtime properties related to data and control flows inside the program, e.g., execution branches and invocation arguments. Symmetrically, dynamic analysis can only observe a limited amount of the possible execution traces of a program. The result is that modern malware have plenty of countermeasures to fool automatic classifiers using either static or dynamic features.
Ideally, there is one static technique that can accurately model the actual behavior of software,
that is symbolic execution [
In this paper we propose a novel technique that combines symbolic execution and MLbased malware detection. The idea is to take advantage of symbolic execution to extract accurate, meaningful behavioral features from malware samples and to apply state-of-the-art ML classifiers to identify suspicious features profiles. To avoid the complexity blowup of symbolic execution, we recur to local, bounded exploration. In particular, we locally explore limited sequences of program instructions instead of the entire code. In this way, symbolic expressions are kept under control and SMT solvers can be eficiently applied to reasonably small problems. Clearly, this comes at the price of an over-approximation of the actual behavior of the target program. Nevertheless, our features are both () more accurate than standard, static features, and () more general than dynamically generated execution traces.
To obtain this result, we introduce a novel specification for behavioral features called Symbolic Feature Specification Language (SFSL). SFSL feature allows to model sort sequences of APIs and relationships between their arguments and return values. Whenever a match is found between a SFSL rule and the target code, a corresponding element of the feature vector is activated. Eventually, the feature vector of a program is passed to a trained ML classifier that decides whether the program should be considered suspicious.
Contributions. The major technical contributions of this paper are the following. • We describe a novel feature specification language known as SFSL to encode the rule used for malware classification. • We introduce a novel symbolic feature extraction technique based on matching the rule with the target code in a binary sample. • We show the efectiveness of our technique by presenting analysis of real-world malware sample in Section 2. • We implemented our approach by combining symbolic feature extraction technique with machine learning classifiers for malware classification.
Paper organization. In Section 2 we introduce a motivating example that we will develop along the paper. In Section 3 we present our methodology based on symbolic feature extraction. Experimental results are given in Section 4. In Section 5 we present the related work. Section 6 summarizes the final thoughts and ideas for further investigation.
In this section we present our motivating example based on malware Derusbi [
Although the above fragment only involves a few instructions, static analyzers based on API
name inspection cannot efectively understand the malicious nature of the performed
operation. The reason is twofold. On the one hand, the chain of involved APIs is standard for most
applications, including benign one. As a matter of fact, according to oficial documentation [
Loosely speaking, our approach amounts to ML-based malware classification, that is, we train a machine learning classifiers to distinguish between malicious and benign software. The main diference with previous proposals is the feature extraction methodology.
Our methodology involves three phases that we list below.
• Phase 1: Features definition. We implement it by defining a feature specification language called SFSL. A SFSL specification consists of a list of rules, each defining a sequence of security relavent APIs together with a boolean condition. Roughly speaking, this corresponds to asking whether the program under analysis can execute the API sequence so that the rule condition is satisfied. • Phase 2: Feature exploration. We implement a feature extraction engine that performs symbolic exploration of a program to check whether program instructions matches the SFSL rule. The result of this phase is a vector of program features where every location contains 1 if the corresponding SFSL rule is satisfied (0 otherwise). • Phase 3: Training machine learning classifier. The features generated by the extraction algorithm are used for training several machine learning classifiers. Trained classifiers are then used in our experiments for assessing the methodology.
SPEC ::= FEAT; …; FEAT; FEAT ::= DECL; PATH; BPRE DECL ::= TYPE VAR, …, TYPE VAR TYPE ::= int | char | string PATH ::= CALL, …, CALL CALL ::= VAR := API(VAR, …, VAR) BPRE ::= ¬ BPRE | BPRE ∧ BPRE | BPRE ∨ BPRE | true | false | SPRE | APRE SPRE ::= VAR in SEXP SEXP ::= [WCHR … WCHR] APRE ::= AEXP = AEXP | AEXP > AEXP
AEXP ::= NUM | VAR | AEXP + AEXP | AEXP - AEXP | AEXP × AEXP | AEXP / AEXP
The abstract syntax of our feature specification language is given in Table 1. A specification (SPEC) amounts to a finite sequence of features (FEAT). Each feature is a triple consisting of some declarations (DECL), a path (PATH) and a Boolean predicate (BPRE). Each declaration is a pair of a type (TYPE) and a variable name (VAR). Supported types include the C base types. For the sake of presentation, here we restrict ourselves to integers, characters and strings. A variable name is any valid identifier. A path is a sequence of API calls (CALL). Each call consists of an assignment of a variable (for the return value) to an API invocation with a list of variables (for the API parameters). Boolean predicates include standard propositional logic connectives as well as string and arithmetic predicates (SPRE and APRE, respectively). A string predicate checks whether a variable matches a certain sequence of characters (WCHR) between […]. For string matching, we use . as a wildcard to denote that the corresponding position in the string can be any character. For instance x in [a.a] is valid for both x=aaa and x=aba. Instead, arithmetic predicates are comparisons between expressions (AEXP).
For brevity, we feel free to use parentheses for grouping and to introduce some abbreviations. In particular, we use ? in API calls in place of a variable name when the variable is immaterial, i.e., it does not appear in the Boolean predicate of the feature specification (and we skip the declaration of such a variable). Also, in case the return variable is equal to ? we simply omit it.
Finally, we use constants in API calls as a shortcut for equality checks as in the following. int x; f(x, 0); x > 2; ≜
int x, int y; f(x, y); x > 2 ∧ y = 0; Example 1. We introduce the following SFSL rule to model the behavior discussed in Section 2. i n t r , i n t s , i n t d , s t r i n g e , i n t h , i n t g ; r : = O p e n S C M a n a g e r A ( ? , ? , ? ) , s : = O p e n S e r v i c e W ( d , e , ? ) , C o n t r o l S e r v i c e ( h , g , ? ) ; r = d ∧ s = h ∧ g = 1 ∧ (e i n [ W i n D e f e n d ] ∨ e i n [ w u a u s e r v ] ∨ e i n [ w s c s v s ] ); The rule above declares 6-variables, i.e., r , s , d , e , h and g . Then, it contains a path consisting of the three API invocations appearing in Listing 1. Finally, the rule concludes with a boolean predicate. The predicate defines a relationship between the invocations by stating that () O p e n S e r v i c e W is invoked on the same service database returned by O p e n S C M a n a g e r A , i.e., r = d , and () C o n t r o l S e r v i c e is invoked on the same service returned by O p e n S e r v i c e W , i.e., s = h . Also, the predicate says that g = 1 , i.e., the command to be issued to the target service is S E R V I C E _ C O N T R O L _ S T O P (1 ). Finally, the rule is matched if the second O p e n S e r v i c e W argument belongs to a list of relevant Windows defense services, i.e., W i n D e f e n d , w u a u s e r v or w s c s v s .
The feature extraction algorithm aims to compile a vector of features for ML classification. We implemented a bounded symbolic exploration strategy. The algorithm used for symbolic feature extraction is given below 1. Application of algorithm on example mentioned in Section 2 is illustrated Example 2.
Algorithm 1 Symbolic Feature Extraction algorithm 1: Input Rule R = ( DECL; PATH; PRED) Sample S 2: for e a c h f u n c t i o n f i n s a m p l e S do 3: C ∶= set of calls to PATH[0] 4: for e a c h c a l l c i n C do 5: init := empty_symbolic_state(f) 6: ∶= explore(init,c) 7: add_bindings ( ,DECL) 8: target := next(PATH) 9: repeat 10: := explore( ,target) 11: add_bindings ( ,DECL) 12: target := next(PATH) 13: until end(PATH) 14: add_predicate( ,PRED) 15: if satisfiable( ) then 16: vector(R) :=1 17: exit; 18: end if 19: end for 20: end for 21: vector(R):=0 22: end Input
Symbolic feature extraction methodology is based on below mentioned Algorithm 1. Algorithm takes RULE(R) as an input. RULE(R) is a triple of DECL (declaration), PATH (path) and PRED (predicate) mentioned in Subsection 3.2. Symbolic state is a set of boolean predicates. Exploration is bounded in nature. Exploration begins by checking the presence of API calls in set C inside a function f of a sample, S and by initializing empty symbolic state. Function explore is called with parameters namely, initialized symbolic state and call c to PATH[0]( ifrst API in a RULE R). Output of the explore function is symbolic state. Then, function add_bindings performs binding between resulting symbolic state from explore and DECL at line 7. Then, we move to next API in a PATH, see Subsection 3.2. This process is repeated until all PATH exhausted(i.e. we reach at last API in a PATH). At line 14, boolean predicates are added by function add_predicate that takes (symbolic state) and PRED as arguments, where here is state obtained after reaching last API in PATH. At the end of exploration of a RULE R, satisfiability check is performed at line 15. If this check amounts to True, one is added to the feature vector and exit is performed to check next RULE R. Otherwise, zero is added to the Vector(R) and we move to the next RULE R.
Example 2. Consider again the fragment of code provided in Section 2. We show the symbolic exploration steps applied to the code fragment and the feature given in Example 1. Exploration starts from a fully symbolic state 0 = ∅. The first instruction to be symbolically executed is s e r v i c e _ d b = O p e n S C M a n a g e r A ( N U L L , N U L L , G E N E R I C _ E X E C U T E ) Since no implementation is given of API O p e n S C M a n a g e r A , it is treated as a purely symbolic function, i.e., such that its return value is unconstrained. Thus, after symbolic evaluations, the next state is 1 = 0 = ∅. Since the previous instruction corresponds to an invocation of the first API of the feature under analysis, the next operation is to add to 1 new bindings between the feature variables and the state variables. In this case we obtain 2 = {s e r v i c e _d b = r }. The next instruction is an if statement. Clearly, when the guard is satisfied, i.e., when s e r v i c e _ d b = = N U L L , the execution jumps to another location and our exploration fails. Thus, we proceed with the new symbolic state 3 = 2 ∪ {s e r v i c e _d b ≠ 0}. The next instruction is
s e r v i c e = O p e n S e r v i c e W ( s e r v i c e _ d b , ( p o i n t e r + 2 0 ) , 0 x 2 0 ) Again, since this API is the next in the feature under evaluation, the new symbolic state 4 must contains bindings between the invocation arguments and the feature variables, that is 4 = 3 ∪ {s e r v i c e = s , s e r v i c e _d b = d , p o i n t e r + 2 0 = e }. Then, the symbolic execution proceeds with another conditional statement. In this case, we want the guard to be satisfied, which implies 5 = 4 ∪ {s e r v i c e ≠ 0}. The next instruction is
e r r = C o n t r o l S e r v i c e ( s e r v i c e , S E R V I C E _ C O N T R O L _ S T O P , & s e r v i c e _ s t a t e )
This API is last in the feature under evaluation, the new symbolic state 6 must contain bindings between the feature variables, the invocation arguments, and symbolic expression that is 6 = 5 ∪ {s e r v i c e = h , S E R V I C E _C O N T R O L _S T O P = g } ∪ {( r = d ∧ s = h ∧ g = 1 ∧ ( e i n [ W i n D e f e n d ] ∨ e i n [ w u a u s e r v ] ∨ e i n [ w s c s v c ] ) ) . After reaching symbolic state 6, SMT solver check for which input values of parameters r , s , d , e , h , g can make the symbolic expression hold true (i.e satisfiable). The solver constraints will look like a sequence of assignments r = d , s = h , g = 1 , e = W i n D e f e n d , s e r v i c e _ d b , s e r v i c e , p o i n t e r . If SMT solver is able to solve constraints in symbolic state 6, presence of a feature is marked. For instance, values that satisfy the assignment are r = 1 , d = 1 , s = 2 , h = 2 , g = 1 , e = W i n D e f e n d , s e r v i c e _ d b = 1 , s e r v i c e = 2 , p o i n t e r = x x x x x x x x x x x x x x x x x x x x W i n D e f e n d . Therefore, there exists a program executable path corresponding to our feature mentioned in Example 1. End result for this feature check provides us with one in our feature vector.
To evaluate the proposed method and create a symbolic feature set, we collected 32-bit Portable
Executable (PE) samples for both malware and benignware. In particular, our corpus of malware
dataset consists of samples from APT Malware Dataset.2 The corpus of benignware is made
up of samples presented in [
We run our experiments on a x64 18.04 Ubuntu, Intel®Core™i7-9750H CPU @ 2.60GHz machine,
with 16 GB RAM. The feature extraction algorithm has been implemented in Python and we
adopted Angr [
The objective of this experiment is to study the performance of the proposed symbolic feature set. Stratified K-Fold splits the dataset on K folds such that each fold contains approximately the same percentage of samples of each target class as the complete set. Stratified K-fold reduces the chance of overfitting. We conducted five separate stratified 4-fold cross-validation experiments. For each of the four partitions, 3 of the folds are used as training data. Validation of the resulting model is done on the remaining data by using it as a test set. Receiver operating characteristic (ROC) curve tracking the relationship between a classifier’s detection threshold and its true and false positive rates for classifiers trained and tested on a symbolic feature set is shown in Figure 2 (a,b,c,d,e). Area under curve (AUC) values shown in Figure 2 (a,b,c,d,e) provide an aggregate measure of performance across all possible classification thresholds. It can be observed that RF and LR performance are the best among all classifiers, while NB gives lowest AUC value. Figure 2 (f) shows the box plot output of classifier’s accuracy collected during stratified 4-fold cross validation trained on symbolic feature set containing 102 features. It is observed that RF and DT have high accuracy and low variation where others have more variation with low accuracy. 2https://github.com/cyber-research/APTMalware 3https://www.malwaredatascience.com/
ROC fold 0 (AUC = 0.89) ROC fold 1 (AUC = 0.89) ROC fold 2 (AUC = 0.89) ROC fold 3 (AUC = 0.89) Chance Mean ROC (AUC = 0.89 ± 0.00) ± 1 std. dev.
ROC fold 0 (AUC = 0.88) ROC fold 1 (AUC = 0.89) ROC fold 2 (AUC = 0.89) ROC fold 3 (AUC = 0.90) Chance Mean ROC (AUC = 0.89 ± 0.01) ± 1 std. dev.
ROC fold 0 (AUC = 0.87) ROC fold 1 (AUC = 0.85) ROC fold 2 (AUC = 0.85) ROC fold 3 (AUC = 0.87) Chance Mean ROC (AUC = 0.86 ± 0.01) ± 1 std. dev.
b) 1.0 ) 1 l: e lab0.8 e v iit so0.6 P ( e t aR0.4 e v iit s Po0.2 e u r T 0.0 d) 1.0 ) 1 l: e lab0.8 e v iit so0.6 P ( e t aR0.4 e v iit s Po0.2 e u r T 0.0 f) 0.84 0.82 y c a r cu0.80 c A 1.0 ) 1 l: e lab0.8 e v iit so0.6 P ( e t aR0.4 e v iit s Po0.2 e u r T 0.0 c) 1.0 ) 1 l: e lab0.8 e v iit so0.6 P ( e t aR0.4 e v iit s Po0.2 e u r T 0.0 e) 1.0 ) 1 l: e lab0.8 e v iit so0.6 P ( e t aR0.4 e v iit s Po0.2 e u r T 0.0
These experiments are only the first attempt to use symbolic features for malware detection and classification. Nevertheless, the results presented above show that malware detection based on symbolic features is feasible. In general, we expect that the number and type of the used rules afects the overall performance of detectors and classifiers implemented in this way. However, the study of this aspect is beyond the scope of the present work.
In this section, we discuss the related work on malware analysis. We categorize existing works as follows.
Static Analysis. Approaches based on static analysis scan the sample without actually
executing it [
Dynamic analysis. These techniques capture the behavior of the program at runtime. One
method to capture such a behavior is to observe the interactions of the program with the
underlying operating system in terms of API calls [
Some approaches [
Discussion. The state of the art discussed above shows that malware detection based on both static and dynamic features have serious limitations. Mainly, static features struggle in capturing a precise definition of malware behavior, while dynamic features cannot efectively explore the program execution paths. While hybrid techniques can partially overcome these issue, a proper definition of “malicious” behavior is still missing. Our technique cope with this limitation by introducing a dedicated feature specification language.
This paper presented a novel symbolic execution-based feature extraction technique that is combined with machine learning to perform malware detection. The main motivation behind the choice of extracting features based on symbolic execution is its ability to provide us with behavioral features without executing the malware. Symbolic execution examines alternative execution paths by exploring the code without running it on a real machine, potentially ofering a more comprehensive understanding of malware’s actions.
As future work, we plan to continue the assessment of our technique. In particular, we plan to extend corpus of malware samples as well as dataset of rules. Another experiment we want to carry out is for measuring the efectiveness of our methodology against zero-day malware. For instance, this might be estimated by () only training our classifier with malware released before a certain date and () testing the classification accuracy by using more recent malware samples. Finally, we want to consider integration of our SFSL with existing specification languages, such as YARA. [26] D. Brumley, C. Hartwig, Z. Liang, J. Newsome, D. Song, H. Yin, Automatically identifying trigger-based behavior in malware, in: Botnet Detection, Springer, 2008, pp. 65–88.