ESIEA RECHERCHE

Résumé: Cette thèse s'intéresse à la modélisation des comportements malicieux au sein des codes malveillants, communément appelés malwares. Les travaux de thèse s'articulent selon deux directions, l'une opérationnelle, l'autre théorique. L'objectif à terme est de combiner ces deux approches afin d'élaborer des méthodes de détection comportementales couvrant la majorité des malwares existants, tout en offrant des garanties formelles de sécurité contre ceux susceptibles d'apparaître.

La première approche opérationnelle introduit un langage comportemental abstrait, décorrélé des aspects liés à l'implémentation tels que les langages de programmation ou les environnements d'exécution. Le langage en lui-même repose sur le formalisme des grammaires attribuées permettant d'exprimer la sémantique des comportements. A l'intérieur du langage, plusieurs descriptions de comportements malicieux sont spécifiées afin de construire une méthode de détection basée sur le parsing. Cette méthode supporte une architecture multi-couche composée de modules d'abstraction et d'automates génériques. Sa mise en oeuvre a montré des résultats prometteurs en termes de couverture, allant de 51% pour les exécutables jusqu'à 91% pour les scripts. Sur la base de ce même langage, des techniques de mutation comportementale allant au delà de celles existantes sont également formalisées à l'aide de techniques de compilation. Ces mutations se révèlent un outil intéressant dans le cadre de l'évaluation de produits antivirus.

La seconde approche théorique introduit un nouveau modèle viral formel, non plus basé sur les paradigmes fonctionnels, mais sur les algèbres de processus. Ce nouveau modèle permet la description de l'auto-réplication ainsi que d'autres comportements plus complexes, basés sur les interactions. Il supporte la redémonstration de résultats fondamentaux tels que l'indécidabilité de la détection et la prévention par isolation. En outre, le modèle supporte la formalisation de plusieurs techniques existantes de détection comportementale, permettant ainsi d'évaluer formellement leur résistance.

Mots clés : Virologie informatique, détection virale, comportements de codes, join-calculus, pi-calcul, interactions fonctionnelles.

Le manuscrit de thèse est disponible en version PDF ; les transparents sont ici.

Abstract: This thesis is devoted to the modeling of malicious behaviors inside malevolent codes, commonly called malware. The thesis work follows two directions, one operational, one theoretical. The objective is to eventually combine these two approaches in order to elaborate detection methods covering most of existing malware, while offering formal security guarantees against appearing ones.

The first operational approach introduces an abstract behavioral language, independent from implementation aspects such as programming languages or execution environments. The language itself relies on the attribute-grammar formalism, capable of expressing the behavior semantics. Within the language, several behavior descriptions are specified in order to build a detection method based on parsing. The method supports a multi-layered architecture constituted of abstraction modules and generic automata. Its deployment has shown satisfying results in terms of coverage, ranging from 51% for malicious executables to 91% for scripts. On the basis of the same language, some techniques of behavioral mutation going further than existing ones have been formalized using compilation techniques. These mutations have proved themselves interesting tools in the context of antiviral product evaluation.

The second theoretical approach introduces a formal viral model, no longer based on functional paradigms, but on process algebras. This new model enables the description of of self-replication as well as other more complex behaviors based on interactions. It supports the redemonstration of fundamental results such as the detection undecidability or the prevention by isolation. Moreover, the model supports the formalization of several existing techniques of behavioral detection, thus allowing the formal evaluation of their resilience.

Keywords: Computer virology, malware detection, program behaviour, join-calculus, pi-calculus, program interactions.

The thesis is available as a PDF file; slides are here (in French).