We consider the LTL model-checking problem of concurrent self-modifying code, i.e., concurrent code that has the ability to modify its own instructions during execution time. This style of code is frequently utilized by malware developers to make their malicious code hard to detect. To model such programs, we consider Self-Modifying Dynamic Pushdown Networks (SM-DPN). A SM-DPN is a network of Self-Modifying Pushdown processes, where each process has the ability to modify its current set of rules and to spawn new processes during execution time. We consider model checking SM-DPNs against single indexed LTL formulas, i.e., conjunctions of separate LTL formulas on each single process. This problem is non-trivial since the number of spawned processes in a given run can be infinite. Our approach is based on computing finite automata representing the set of configurations from which the SM-DPN has a run that satisfies the single-indexed LTL formula. We implemented our techniques in a tool and obtained promising results. We demonstrate that our tool successfully detects concurrent and self-modifying malware.

International audience

In this paper, we present SMODIC, a model checker for self-modifying binary codes. SMODIC uses Self Modifying Pushdown Systems (SM-PDS) 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 successfully 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 200 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. SMODIC can be found in https://lipn.univ-paris13.fr/~touili/smodic

With the huge impact that internet is having in our daily life, it is becoming urgent to have efficient malware detection techniques. In this paper, we present a new approach to perform malware detection. We use register automata to describe malware specifications, and pushdown systems to model the program. This allows to keep track of both the program’s stack and the values of the registers. Indeed, both the stack and the registers are needed to have precise malware specifications. To check whether the program contains some malicious behavior, we perform a kind of product between the pushdown system and the register automaton describing the malicious behaviors. Whether the program is malicious or not is then reduced to reachability checking in pushdown systems. We implemented our techniques in a prototype and obtained encouraging preliminary results.

In recent years, the damage cost caused by malwares is huge. Thus, malware detection is a big challenge. The task of specifying malware takes a huge amount of time and engineering effort since it currently requires the manual study of the malicious code. Thus, in order to avoid the tedious manual analysis of malicious codes, this task has to be automatised. To this aim, we propose in this work to represent malicious behaviours using extended API call graphs, where nodes correspond to API function calls, edges specify the execution order between the API functions, and edge labels indicate the dependence relation between API functions parameters. We define new static analysis techniques that allow to extract such graphs from programs, and show how to automatically extract, from a set of malicious and benign programs, an extended API call graph that represents the malicious behaviours. Finally, we show how this graph can be used for malware detection. We implemented our techniques and obtained encouraging results: 95.66% of detection rate with 0% of false alarms.

Self-modifying code is extensively used to obfuscate malware and to make reverse engineering harder. It consists in code that can modify its own instructions during the execution. Being able to analyse such code is crucial nowadays. In this paper, we consider the CTL model-checking problem of self modifying code. To model such programs, we use Self Modifying Pushdown Systems (SM-PDS), an extension of pushdown systems whose set of rules can be modified during execution. We reduce the CTL model-checking problem to the emptiness problem of Self-Modifying Alternating Büchi pushdown systems (SM-ABPDS). We implemented our techniques in a tool. We obtained encouraging results. In particular, our tool was able to detect several self-modifying malwares; it could even detect several malwares that well-known antiviruses such as McAfee, Norman, BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast, and Symantec failed to detect.

One of the main challenges in malware detection is the discovery of malicious behaviors. This task requires a huge amount of engineering and manual study of the code. To avoid this tedious manual task, we propose in this paper a tool, called STAMAD, that, given a training set of known malwares and benign programs, (1) either automatically extracts malicious behaviors using Information Retrieval techniques, or (2) applies machine learning techniques to automatically learn malwares. Then, in both cases, STAMAD can classify a new given unseen program as malicious or benign.

Self modifying code is code that can modify its own instructions during the execution of the program. It is extensively used by malware writers to obfuscate their malicious code. Thus, analysing self modifying code is nowadays a big challenge. In this paper, we consider the LTL model-checking problem of self modifying code. We model such programs using self-modifying pushdown systems (SM-PDS), an extension of pushdown systems that can modify its own set of transitions during execution. We reduce the LTL model-checking problem to the emptiness problem of self-modifying Buchi pushdown systems (SM-BPDS). We implemented our techniques in a tool that we successfully applied for the detection of several self-modifying malware. Our tool was also able to detect several malwares that well-known antiviruses such as BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec failed to detect.

Machine learning techniques were extensively applied to learn and detect malware. However, these techniques use often rough abstractions of programs. We propose in this work to use a more precise model for programs, namely extended API call graphs, where nodes correspond to API function calls, edges specify the execution order between the API functions, and edge labels indicate the dependence relation between API functions parameters. To learn such graphs, we propose to use Generalized Random Walk Graph Kernels (combined with Support Vector Machines). We implemented our techniques and obtained encouraging results for malware detection: 96.73% of detection rate with 0.73% of false alarms.

In recent years, the damage cost caused by malwares is huge. Thus, malware detection is a big challenge. The task of specifying malware takes a huge amount of time and engineering effort since it currently requires the manual study of the malicious code. Thus, in order to avoid the tedious manual analysis of malicious codes, this task has to be automatized. To this aim, we propose in this work to represent malicious behaviors using extended API call graphs, where nodes correspond to API function calls, edges specify the execution order between the API functions, and edge labels indicate the dependence relation between API functions parameters. We define new static analysis techniques that allow to extract such graphs from programs, and show how to automatically extract, from a set of malicious and benign programs, an extended API call graph that represents the malicious behaviors. Finally, We show how this graph can be used for malware detection. We implemented our techniques and obtained encouraging results: 95.66% of detection rate with 0% of false alarms.

The number of Android malware is increasing every day. Thus Android malware detection is nowadays a big challenge. One of the most tedious tasks in malware detection is the extraction of malicious behaviors. This task is usually done manually and requires a huge effort of engineering. To avoid this step, we propose in this paper to use machine learning techniques for malware detection. Unlike the existing learning based approaches, we propose to use API call graphs to represent the behaviors of Android applications. Then, given a set of malicious applications and a set of benign applications, we apply well-known learning techniques based on Random Walk Graph Kernel (combined with Support Vector Machines). We can achieve a high detection rate with only few false alarms (98.76% for detection rate with 0.24% of false alarms).

Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because they allow to accurately model procedure calls and mimic the program's stack. In this work, we propose to extend the PushDown System model with selfmodifying rules. We call the new model Self-Modifying Push- Down System (SM-PDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. We show how SMPDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SM-PDSs. We implemented our techniques in a tool and obtained encouraging results. In particular, we successfully applied our tool for the detection of self-modifying malware.

The number of malware is growing significantly fast. Traditional malware detectors based on signature matching or code emulation are easy to get around. To overcome this problem, model-checking emerges as a technique that has been extensively applied for malware detection recently. Pushdown systems were proposed as a natural model for programs, since they allow to keep track of the stack, while extensions of LTL and CTL were considered for malicious behavior specification. However, LTL and CTL like formulas don't allow to express behaviors with matching calls and returns. In this paper, we propose to use CARET for malicious behavior specification. Since CARET formulas for malicious behaviors are huge, we propose to extend CARET with variables, quantifiers and predicates over the stack. Our new logic is called SPCARET. We reduce the malware detection problem to the model checking problem of PDSs against SPCARET formulas, and we propose efficient algorithms to model check SPCARET formulas for PDSs. We implemented our algorithms in a tool for malware detection. We obtained encouraging results.

Abstract A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. Thus, it is important to have model checking algorithms for DPNs. We consider in this work model checking DPNs against single-indexed LTL and CTL properties of the form ⋀ f i such that f i is a LTL/CTL formula over the PDS i . We consider the model checking problems w.r.t. simple valuations (i.e., whether a configuration satisfies an atomic proposition depends only on its control location) and w.r.t. regular valuations (i.e., the set of the configurations satisfying an atomic proposition is a regular set of configurations). We show that these model checking problems are decidable. We propose automata-based approaches for computing the set of configurations of a DPN that satisfy the corresponding single-indexed LTL/CTL formula.

We present PoMMaDe, a Pushd own Model-checking based M alware D etector. In PoMMaDe, a binary program is modeled as a pushdown system (PDS) which allows to track the stack of the program, and malicious behaviors are specified in SCTPL or SLTPL, where SCTPL (resp. SLTPL) is an extension of CTL (resp. LTL) with variables, quantifiers, and predicates over the stack (needed for malware specification). The malware detection problem is reduced to SCTPL/SLTPL model-checking for PDSs. PoMMaDe allows us to detect 600 real malwares, 200 new malwares generated by two malware generators NGVCK and VCL32, and prove benign programs are benign. In particular, PoMMaDe was able to detect several malwares that could not be detected by well-known anti-viruses such as Avira, Avast, Kaspersky, McAfee, AVG, BitDefender, Eset Nod32, F-Secure, Norton, Panda, Trend Micro and Qihoo 360.

We consider the verification problem of multithreaded recursive programs. We use Process Rewrite Systems (PRS) to model such programs. This allows the use of all the existing results for the analysis of PRS to analyse multithreaded recursive programs. We first give a fully automatic translation from parallel recursive programs to PRS. As far as we know, this is the first time that a formal translation from multithreaded programs to PRS is given. The obtained PRS is an abstraction of the program. We identify a class of programs for which our translation is exact. We also propose a refinement procedure that allows to create more precise PRS models of a given program. We applied our techniques successfuly for the analysis of two versions of a Windows NT Bluetooth driver.

In this paper, we present PuMoC, a CTL model checker for Pushdown systems (PDSs) and sequential C/C++ and Java programs. PuMoC allows to do CTL model-checking w.r.t simple valuations, where the atomic propositions depend on the control locations of the PDSs, and w.r.t. regular valuations, where atomic propositions are regular predicates over the stack content. Our tool allowed to (1) check 500 randomly generated PDSs against several CTL formulas; (2) check around 1461 versions of 30 Windows drivers taken from SLAM benchmarks; (3) check several C and Java programs; and (4) perform data flow analysis of real-world Java programs. Our results show the efficiency and the applicability of our tool.

Multiset pushdown systems have been introduced by Sen and Viswanathan as an adequate model for asynchronous programs where some procedure calls can be stored as tasks to be processed later. The model is a pushdown system supplied with a multiset of pending tasks. Tasks may be added to the multiset at each transition, whereas a task is taken from the multiset only when the stack is empty. In this paper, we consider an extension of these models where tasks may be of different priority level, and can be preempted at any point of their execution by tasks of higher priority. We investigate the control point reachability problem for these models. Our main result is that this problem is decidable by reduction to the reachability problem for a decidable class of Petri nets with inhibitor arcs. We also identify two subclasses of these models for which the control point reachability problem is reducible respectively to the reachability problem and to the coverability problem for Petri nets (without inhibitor arcs).

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras.

Proposes a natural subclass of regular languages, called alphabetic pattern constraints (APC), which is effectively closed under permutation rewriting, i.e. under iterative application of rules of the form ab/spl rarr/ba. It is well-known that regular languages do not have this closure property in general. Our result can be applied for example to regular model checking, for verifying properties of parametrized linear networks of regular processes and for modeling and verifying properties of asynchronous distributed systems. We also consider the complexity of testing membership in APC, and show that the question is complete for PSPACE when the input is an NFA (nondeterministic finite automaton) and complete for NLOGSPACE when it is a DFA (deterministic finite automaton). Moreover, we show that both the inclusion problem and the question of closure under permutation rewriting are PSPACE-complete when we restrict ourselves to the APC class.