L'objectif de cette thèse est le développement de méthodes de compréhension des logiciels malveillants, afin d'aider l'analyste humain à mieux appréhender cette menace. La première réalisation de cette thèse est une analyse à grande échelle et en profondeur des protections de logiciels malveillants. Plus précisément, nous avons étudié des centaines d'exemplaires de logiciels malveillants, soigneusement sélectionnés pour leur dangerosité. En mesurant de façon automatique un ensemble de caractéristiques originales, nous avons pu alors montrer l'existence d'un modèle de protection particulièrement prévalent dans ces programmes, qui est basé sur l'auto modification du code et sur une limite stricte entre code de protection et code utile. Ensuite, nous avons développé une méthode d'identification d'implémentations cryptographiques adaptée aux programmes en langage machine protégés. Nous avons validé notre approche en identifiant de nombreuses implémentations d'algorithmes cryptographiques -- dont la majorité sont complètement invisibles pour les outils existants --, et ceci en particulier dans des protections singulièrement obscures de logiciels malveillants. Finalement, nous avons développé ce qui est, à notre connaissance, le premier environnement d'émulation de réseaux de machines infectées avec plusieurs milliers de machines. Grâce à cela, nous avons montré que l'exploitation d'une vulnérabilité du protocole pair-à-pair du réseau Waledac permet de prendre son contrôle.

Ma thèse porte sur l'étude des couplages, et plus particulièrement leur utilisation en cryptographie. Mes premiers travaux ont portés sur l'arithmétique des couplages à travers une comparaison des complexités en nombre d'opérations des couplages de Weil et Tate. Puis je me suis intéressée à l'étude de l'arithmétique utile pour les couplages. Un de mes travaux propose d'utiliser une représentation alternative des corps finis pour améliorer l'efficacité des calculs impliqués dans les couplages. Le second étudie en détail l'arithmétique des couplages pour les courbes dont le degré d'enfoncement est 15. Ces premiers travaux m'ont permis de me familiariser avec les couplages et je me suis alors orientée vers la résistance aux attaques par canaux cachés des algorithmes de couplage. J'ai étudié les faiblesses de l'algorithme de Miller lorsqu'il subit des attaques par analyse de consommation de courant et par injection de fautes.

Dans cette thèse, nous nous intéressons à la cryptanalyse de certaines primitives de cryptographie symétrique qui utilisent les concepts de construction du schéma de chiffrement AES. Nous commençons par une analyse de l'AES lui-même dans trois modèles de sécurité différents: le modèle standard, le modèle à clefs reliées et le modèle ouvert. Dans le modèle standard, où l'adversaire cherche à récupérer la clef secrète, nous décrivons les meilleures attaques différentielles existantes sur cet algorithme de chiffrement, en améliorant les attaques différentielles précédemment publiées. Ensuite, nous procédons à une analyse structurelle de l'AES dans le modèle à clefs reliées. Nous montrons des résultats d'impossibilité, indiquant que l'on ne peut pas prouver la sécurité de la structure de l'AES contre les attaques différentielles dans ce modèle. Enfin, dans le modèle ouvert, nous proposons le premier distingueur pour neuf tours d'AES-128, ce qui résout un problème ouvert depuis plusieurs années dans la communauté symétrique. Dans une deuxième partie, nous analysons en détail l'application de l'attaque par rebond sur les primitives basées sur l'AES. Nous montrons qu'il est possible de considérer un tour de plus dans la première des deux phases de cette stratégie, ce qui améliore les meilleurs résultats connus sur les permutations à base d'AES. Ceci résout le problème ouvert consistant à augmenter le nombre total de tours attaqués grâce à cette technique. Nous montrons également qu'il est possible de relâcher certaines contraintes pour augmenter la probabilité de succès de la deuxième étape. Ceci conduit à une diminution des complexités de toutes les attaques publiées. Nous appliquons ces améliorations à la fonction de hachage Grostl, obtenant les meilleures attaques sur la permutation interne. Finalement, nous nous intéressons à la fonction de hachage ECHO pour montrer qu'il est possible d'appliquer plusieurs fois l'attaque par rebond et ainsi attaquer plus de tours de la permutation interne.

Cette thèse se propose de remédier à l'absence de formalisme dédié aux preuves de sécurité concrète à travers 3 contributions. Nous présentons d'abord la logique CIL (Computational Indistinguishability Logic), qui permet de raisonner sur les systèmes cryptographiques. Elle contient un petit nombre de règles qui correspondent aux raisonnements souvent utilisés dans les preuves. Leur formalisation est basée sur des outils classiques comme les contextes ou les bisimulations. Deuxièmement, pour plus d'automatisation des preuves, nous avons conçu une logique de Hoare dédiée aux chiffrement asymétrique dans le modèle de l'oracle aléatoire. Elle est appliquée avec succès sur des exemples de schémas existants. Enfin, nous proposons un théorème générique de réduction pour la preuve d'indifférentiabilité d'un oracle aléatoire de fonctions de hachage cryptographiques. La preuve du théorème, formalisée en CIL, en démontre l'applicabilité. Les exemples de Keccak et Chop-Merkle-Damgard illustrent ce résultat.

Le chapitre 2 présente la première partie importante de nos travaux : l'approche pour la détection que nous proposons. Nous avons tout d'abord expliqué les caractéristiques des attaques contre les données de calcul et en quoi ces dernières se distinguent des autres types d'attaque. Ceci nous a notamment permis de montrer que pour perpétuer une intrusion, un utilisateur malveillant va chercher à cibler un ensemble bien précis de données de calcul. À l'aide de la logique de Hoare, nous avons ensuite expliqué que le code source des applications peut contenir des informations qui peuvent être utilisées pour détecter ce type bien précis d'attaque. Nous avons détaillé cela sur un exemple d'exploitation de vulnérabilité. Puis, nous avons présenté notre modèle de détection. Nous l'avons tout d'abord présenté empiriquement sur un cas réel d'attaques contre les données de calcul. Pour cela, nous avons détaillé la vulnérabilité utilisée dans notre exemple ainsi que les différents scénarios d'attaque et comment des invariants portant sur certaines variables permettent de détecter ces attaques. Enfin, nous avons présenté formellement notre modèle de détection. Celui-ci correspond à l'ensemble des domaines de variation des variables qui influencent l'exécution des appels de fonction. Ces domaines de variation sont calculés juste avant les appels de fonction et uniquement pour les variables qui sont atteignables à ces endroits du code source. Nous avons ensuite présenté une méthode pour construire un tel modèle. Premièrement, nous proposons d'utiliser le graphe de dépendance du programme pour déterminer pour chaque appel de fonction l'ensemble des variables qui influencent son exécution. Deuxièmement, nous proposons d'utiliser l'interprétation abstraite pour calculer pour chacun de ces ensembles de variables leur domaine de variation. Pour finir, nous présentons une implémentation de notre approche que nous avons réalisée pour les programmes écrits en langage C. Nous détaillons d'abord la phase de construction du modèle qui repose sur un outil d'analyse statique existant, Frama-C. Nous détaillons ensuite la phase d'instrumentation, celle-ci ayant pour contrainte de ne pas modifier le processus original de compilation. Le chapitre 3 présente la seconde partie importante de nos travaux : l'approche pour l'évaluation que nous proposons. Nous commençons par aborder la problématique de la simulation des erreurs engendrées par les attaques contre les données de calcul. Pour cela, nous présentons d'abord le modèle de faute que nous proposons pour simuler ce type bien particulier d'attaques. Nous étudions les caractéristiques qui doivent être simulées, quel sera leur impact sur le programme et dans quel cas ces dernières peuvent être détectées. Nous expliquons ensuite comment nous proposons de construire notre modèle de simulation. La principale problématique ici est de savoir comment déterminer l'ensemble des cibles potentielles. Il s'agit du même ensemble de variables que pour la détection. Nous proposons donc à nouveau de nous reposer sur le graphe de dépendance du programme et d'embarquer les mécanismes d'injection au sein des applications. Nous expliquons ensuite comment notre modèle de faute peut être utilisé pour l'évaluation d'un système de détection d'intrusion. Nous posons comme objectif que le résultat obtenu doit être une sur-approximation du taux de faux négatifs réel. Cela implique que nous voulons placer le système de détection d'intrusion à évaluer dans la situation la moins favorable possible. Pour respecter cette contrainte, nous montrons que notre modèle de faute doit être utilisé pour simuler une intrusion qui ne nécessite qu'une seule exploitation de la vulnérabilité, que la vulnérabilité donne accès à l'ensemble de l'espace mémoire du processus et que l'exploitation ne vise qu'une seule variable. Nous présentons enfin les modifications que nous avons apportées à notre outil afin qu'il instrumente aussi les programmes pour l'injection et comment les mécanismes d'injection ainsi ajoutés doivent être utilisés. Le chapitre 4 présente la dernière partie de nos travaux : l'évaluation de notre système de détection d'intrusion, notamment à l'aide de notre modèle de simulation d'attaque. Nous commençons par présenter la plateforme de tests que nous avons développée autour de nos mécanismes d'injection. Il s'agit d'une plateforme qui automatise la réalisation de tests ainsi que l'analyse des résultats obtenus. Nous abordons tout d'abord les problématiques d'écriture des scénarios d'exécution et de collecte des informations. Les scénarios doivent permettre de couvrir suffisamment le code des programmes utilisés pour les tests. Nous avons choisi de mesurer ce taux de couverture en fonction des appels de fonction. Les informations collectées sont utilisées pour produire deux résultats : une sur-approximation du taux réel de faux négatifs et une évaluation du taux de détection pour les injections ayant provoqué une déviation comportementale. Pour finir, nous présentons les résultats de l'évaluation de notre système de détection d'intrusion. Nous commençons par donner les performances de l'analyse. On note que la durée d'analyse peut être très grande, notamment en fonction de la taille du code à analyser, mais qu'en fonction de la sémantique du code, deux programmes de taille similaire peuvent présenter des durées d'analyse complètement différentes. Puis, nous donnons le niveau de surcharge à l'exécution. On note que la surcharge induite par nos mécanismes de détection est très faible, toujours inférieure à 1%. Nous continuons avec les performances de la détection. Nous pouvons voir que les résultats de la détection varient grandement d'un programme à l'autre, malgré un taux d'instrumentation similaire. Ce qui change, c'est le nombre d'invariants vérifiés. On voit ici la limite de notre approche : si la sémantique du code original ne permet pas de calculer suffisamment d'invariants, l'efficacité de notre approche sera alors limitée. De plus, la propagation de l'erreur n'apporte que peu d'aide à notre modèle de détection. Dans tous les cas, nous avons pu vérifier que notre approche ne génère bien pas de faux positif.

Les contremesures de masquage et de dissimulation permettent de rendre plus compliquées les attaques sur les implémentations de chiffrement symétrique. Elles sont aussi toutes deux aisément implémentables (et ce de façon automatisable) dans des flots EDA (Electronic Design Automation) pour ASIC (Application Specific Integrated Circuit) ou FPGA (Field Programmable Gates Array), avec certes différents niveaux d'expertise requis selon la contremesure concernée. Le masquage assure une protection "dynamique" s'appuyant sur un mélange d'aléa en cours de calcul. Nous montrons comment optimiser l'usage de cet aléa grâce à un codage qui permet de compresser les fuites d'information (leakage squeezing). Les limites du masquage s'étudient grâce à des outils de statistique, en analysant des distributions de probabilités. L'outil maître pour évaluer les imperfections des logiques DPL (Dual-rail with Precharge Logic style) est l'analyse stochastique, qui tente de modéliser des fuites "statiques" combinant plusieurs bits. L'inconvénient du masquage est que les attaques sont structurelles à l'utilisation d'aléa : si une attaque réussit sur une partie de la clé (e.g. un octet), alors a priori tous les autres octets sont de façon consistante vulnérables à la même attaque. La situation est différente avec les DPL : en cas de problème d'implémentation, seuls les octets de clés impliqués dans les parties déséquilibrées sont compromis, et non toute la clé. Une façon encore moins coûteuse de protéger les implémentations cryptographiques contre les attaques physiques est la résilience. C'est un usage astucieux de primitives a priori non protégées qui permet d'assurer la protection des secrets. L'avantage des approches résilientes est leur simplicité de mise en oeuvre et (idéalement), leur prouvabilité. Le principal inconvénient est que les contraintes d'usage ne sont souvent pas compatibles avec les standards actuels. Ainsi, nous pensons que davantage de recherche dans ce domaine pourrait globalement être profitable à l'industrie de la sécurité de systèmes embarqués.

Les travaux de recherche de cette thèse s'inscrivent dans le cadre de la sécurité par chaos des réseaux locaux sans fil, en particulier les réseaux de capteurs sans fil. L'originalité de cette thèse consiste à proposer des cryptosystèmes à base de chaos plus adaptés aux réseaux de capteurs, en termes de consommation d'énergie, que les algorithmes conventionnels et à réaliser une implémentation sur une plateforme réelle. Nous présentons en premier lieu un état de l'art des réseaux, les menaces, les contraintes limitant le processus de sécurité des informations ainsi que les principales techniques de cryptographie. Nous donnons un aperçu sur la théorie de chaos et nous validons l'aspect aléatoire de plusieurs suites chaotiques par les tests statistiques du NIST. Nous proposons ensuite des nouvelles méthodes de construction de S-Box chaotiques tout en prouvant leur robustesse contre les attaques traditionnelles. Nous proposons enfin un nouvel algorithme de cryptage d'image dédié au réseau de capteurs sans fil. La validation de nos contributions est effectuée par simulation et par des mesures expérimentales sur une plateforme de réseaux de capteurs réels (SensLab).

Le chiffrement est sûrement une primitive fondamentale parmi les fonctions cryptogra- phiques. Cela rend possible à deux parties, d'ordinaire appelées Alice et Bob, de commu- niquer au travers d'un canal non sécurisé en permettant qu'un adversaire, Eve, ne puisse pas comprendre leur communication. Il pourrait sembler assez facile d'identifier les contraintes nécessaires pour le design d'un " bon " schéma de chiffrement. Il s'avère en réalité que la définition d'un modèle de sécurité rigoureux n'est pas trivial. Ceci dépend fortement du contexte. La sécurité même dépend du contexte. Ce document s'ouvre avec un chapitre d'introduction à la cryptographie à clé publique. Nous décrirons ensuite comment la sécurité d'une telle primitive est évaluée en définissant de façon rigoureuse un attaquant, en particulier cela signifie fixer son but et les moyens dont il dispose. La suite de ce document s'organise autour de deux parties. La première partie concerne l'anonymat révocable. Nous obtenons et présentons deux schémas pour garantir l'anonymat pour l'envoyeur d'un message chiffré mais avec la possibilité pour un troisième acteur de confiance, si le cas le nécessite, de révéler l'identité de l'envoyeur. Cette primitive a été appliquée dans les contextes du chiffrement à clé publique et du chiffrement broadcast. Dans la deuxième partie, nous nous dédions à l'étude et à l'amélioration d'un schéma de chiffrement à clé publique dont l'original est dû à Goldwasser et Micali. Notre travail généralise leur schéma en fournissant une famille de schémas de chiffrement. Notre travail est motivé par la recherche de l'amélioration de l'efficacité (en termes de bande passante) du schéma original, afin de pouvoir chiffrer des messages plus longs dans un chiffré de la même taille.

Ce document constitue un dossier de demande d'inscription a l'Habilitation a Diriger des Recherches. Il résume 10 années d'activités professionnelles passées en tant qu'enseignant-chercheur sur le campus de Rennes de Supelec. Ce document est constitue de deux parties. La première partie propose une présentation du candidat qui prend la forme d'un curriculum vitæ, d'une présentation des activités d'enseignement et d'une présentation des activités de recherche. L'ensemble se termine par une liste de publications. La seconde partie est une synthèse d'une partie des activités de recherche menées ces dix dernières années. Un état de l'art pose les concepts sur lesquels reposent ces travaux. Ensuite quatre activités de recherche sont présentées, chacune d'elle mettant en évidence la pertinence de certaines techniques de détection d'erreur dans le domaine de la détection d'intrusion.

Security critical applications often store keys on dedicated HSM or key-management servers to separate highly sensitive cryptographic operations from more vulnerable parts of the network. Access to such devices is given to protocol parties by the means of Security APIs, e.g., the RSA PKCS#11 standard, IBM's CCA and the TPM API, all of which protect keys by providing an API that allows to address keys only indirectly. This thesis has two parts. The first part deals with formal methods that allow for the identification of secure configurations in which Security APIs improve the security of existing protocols, e.g., in scenarios where parties can be corrupted. A promising paradigm is to regard the Security API as a participant in a protocol and then use traditional protocol analysis techniques. But, in contrast to network protocols, Security APIs often rely on the state of an internal database. When it comes to an analysis of an unbounded number of keys, this is the reason why current tools for protocol analysis do not work well. We make a case for the use of MSR as the back-end for verification and propose a new process calculus, which is a variant of the applied pi calculus with constructs for manipulation of a global state. We show that this language can be translated to MSR rules while preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a back-end. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and a contract signing protocol. The second part of this thesis aims at identifying security properties that a) can be established independent of the protocol, b) allow to catch flaws on the cryptographic level, and c) facilitate the analysis of protocols using the Security API. We adapt the more general approach to API security of Kremer et.al. to a framework that allows for composition in form of a universally composable key-management functionality. The novelty, compared to other definitions, is that this functionality is parametric in the operations the Security API allows, which is only possible due to universal composability. A Security API is secure if it implements correctly both key-management (according to our functionality) and all operations that depend on keys (with respect to the functionalities defining those operations). We present an implementation which is defined with respect to arbitrary functionalities (for the operations that are not concerned with key-management), and hence represents a general design pattern for Security APIs.