Cette thèse s'attaque au problème de détection de malware en utilisant des techniques de model-checking: les automates à pile sont utilisés pour modéliser les programmes binaires, et la logique CARET (et ses variantes) sont utilisées pour représenter les comportements malicieux. La détection de malware est alors réduite au problème de model-checking des automates à pile par rapport à ces logiques CARET. Cette thèse propose alors différents algorithmes de model-checking des automates à pile par rapport à ces logiques CARET et montre comment ceci peut s'appliquer pour la détection de 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 thesis, we propose to use CARET (a temporal logic of calls and returns) for malicious behavior specification. CARET model checking for Pushdown Systems (PDSs) was never considered in the literature. Previous works only dealt with the model checking problem for Recursive State Machine (RSMs). While RSMs are a good formalism to model sequential programs written in structured programming languages like C or Java, they become non suitable for modeling binary or assembly programs, since, in these programs, explicit push and pop of the stack can occur. Thus, it is very important to have a CARET model checking algorithm for PDSs. We tackle this problem in this thesis. We reduce it to the emptiness problem of Büchi Pushdown Systems. Since CARET formulas for malicious behaviors are huge, we propose to extend CARET with variables, quantifiers and predicates over the stack. This allows to write compact formulas for malicious behaviors. Our new logic is called Stack linear temporal Predicate logic of CAlls and RETurns (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. We then define the Branching temporal logic of CAlls and RETurns (BCARET) that allows to write branching temporal formulas while taking into account the matching between calls and returns and we proposed model-checking algorithms of PDSs for BCARET formulas. Finally, we consider Dynamic Pushdown Networks (DPNs) as a natural model for multithreaded programs with (recursive) procedure calls and thread creation. We show that the model-checking problem of DPNs against CARET formulas is decidable.
| Identifer | oai:union.ndltd.org:theses.fr/2018USPCC061 |
| Date | 05 July 2018 |
| Creators | Nguyen, Huu vu |
| Contributors | Sorbonne Paris Cité, Touili, Tayssir |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation, Text, Collection, StillImage |
Page generated in 0.0019 seconds