Analyse de Programmes Malveillants par Abstraction de Comportements

Philippe Beaucamps 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Résumé : L'analyse comportementale traditionnelle opère en général au niveau de l'implantation du comportement malveillant. Pourtant, elle s'intéresse surtout à l'identification d'un comportement donné, indépendamment de sa mise en œuvre technique, et elle se situe donc plus naturellement à un niveau fonctionnel. Dans cette thèse, nous définissons une forme d'analyse comportementale de programmes qui opère non pas sur les interactions élémentaires d'un programme avec le système mais sur la fonction que le programme réalise. Cette fonction est extraite des traces d'un programme, un procédé que nous appelons abstraction. Nous définissons de façon simple, intuitive et formelle les fonctionnalités de base à abstraire et les comportements à détecter, puis nous proposons un mécanisme d'abstraction applicable à un cadre d'analyse statique ou dynamique, avec des algorithmes pratiques à complexité raisonnable, enfin nous décrivons une technique d'analyse comportementale intégrant ce mécanisme d'abstraction. Notre méthode est particulièrement adaptée à l'analyse des programmes dans des langages de haut niveau ou dont le code source est connu, pour lesquels l'analyse statique est facilitée : les programmes conçus pour des machines virtuelles comme Java ou .NET, les scripts Web, les extensions de navigateurs, les composants off-the-shelf. Le formalisme d'analyse comportementale par abstraction que nous proposons repose sur la théorie de la réécriture de mots et de termes, les langages réguliers de mots et de termes et le model checking. Il permet d'identifier efficacement des fonctionnalités dans des traces et ainsi d'obtenir une représentation des traces à un niveau fonctionnel ; il définit les fonctionnalités et les comportements de façon naturelle, à l'aide de formules de logique temporelle, ce qui garantit leur simplicité et leur flexibilité et permet l'utilisation de techniques de model checking pour la détection de ces comportements ; il opère sur un ensemble quelconque de traces d'exécution ; il prend en compte le flux de données dans les traces d'exécution ; et il permet, sans perte d'efficacité, de tenir compte de l'incertitude dans l'identification des fonctionnalités. Nous validons nos résultats par un ensemble d'expériences, menées sur des codes malicieux existants, dont les traces sont obtenues soit par instrumentation binaire dynamique, soit par analyse statique.
Type de document :
Thèse
Logique en informatique [cs.LO]. Institut National Polytechnique de Lorraine - INPL, 2011. Français
Liste complète des métadonnées

https://tel.archives-ouvertes.fr/tel-00646395
Contributeur : Isabelle Gnaedig <>
Soumis le : mardi 29 novembre 2011 - 19:32:41
Dernière modification le : jeudi 22 septembre 2016 - 14:31:50

Identifiants

  • HAL Id : tel-00646395, version 1

Collections

Citation

Philippe Beaucamps. Analyse de Programmes Malveillants par Abstraction de Comportements. Logique en informatique [cs.LO]. Institut National Polytechnique de Lorraine - INPL, 2011. Français. <tel-00646395>

Partager

Métriques

Consultations de
la notice

357

Téléchargements du document

567