Applications of formal methods to malware detection.

Applications des méthodes formelles à la détection de logiciels malveillants. Détecter les logiciels malveillants est un défi complexe et en constante évolution. Dans cette thèse, nous explorons les méthodes existantes de détection de logiciels malveillants dans le but de séparer les étapes d'analyse et de détection et de les connecter en utilisant des méthodes formelles. Nous commençons par examiner le paysage actuel des menaces et les techniques de détection de menaces existantes afin d'identifier des motifs et comportements communs. Avec ces motifs en tête, nous proposons un modèle général pour la détection des menaces et une méthodologie claire permettant d'avoir l'analyse et la détection comme processus distincts. Nous introduisons un langage général pour construire une détection opérationnelle (Generic Threat Detection Language - GTDL) avec la sémantique formelle associée. Du côté de l'analyse, nous utilisons des arbres d'attaque pour décrire les menaces de manière rigoureuse. Nous utilisons ensuite des modèles formels et des outils de vérification (CADP) pour établir un lien entre la description de la menace et la détection opérationnelle dans le but d'aligner la détection avec les résultats de l'analyse. Notre objectif est de créer des systèmes et des méthodes de détection fiables et précis basés sur les insights de l'analyse. Nous proposons également une méthodologie pour créer une détection opérationnelle écrite en GTDL directement à partir de la description de la menace sous forme d'arbre d'attaque. Enfin, nous explorons comment extraire des spécifications à partir de grandes bases de données de logiciels malveillants connus en utilisant une analyse statistique, spécifications qui peuvent ensuite être utilisées pour créer automatiquement des détections opérationnelles efficaces.