Nguyen, Huu vu
[Author]
;
Sorbonne Paris Cité
[Contributor];
Touili, Tayssir
[Contributor]
On CARET model-checking of pushdown systems : application to malware detection ; CARET model-checking d'automates à piles : application à la détection de malware
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
Still Image;
E-Book
Title:
On CARET model-checking of pushdown systems : application to malware detection ; CARET model-checking d'automates à piles : application à la détection de malware
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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 ...