Malware behavioral models : bridging abstract and operational virology
Institution:
Rennes 1Disciplines:
Directors:
Abstract EN:
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. L'approche opérationnelle introduit un langage comportemental abstrait, décorrélé de l'implémentation. 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 multicouche basée sur le parsing. Sur la base de ce même langage, des techniques de mutation comportementale sont également formalisées à l'aide de techniques de compilation. Ces mutations se révèlent un outil intéressant pour l'évaluation de produits antivirus. L'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.
Abstract FR:
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 operational approach introduces an abstract behavioral language, independent from implementation. 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 multi-layered detection method based on parsing. Its deployment has shown satisfying results in terms of coverage. On the basis of the same language, some techniques of behavioral mutation have been formalized using compilation techniques. These mutations have proved themselves interesting tools for the evaluation of antiviral products. The theoretical approach introduces a formal viral model, no longer based on functional paradigms, but on process algebras. This new model enables the description 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.