On appelle résilient un système capable de conserver ses propriétés de sûreté de fonctionnement en dépit des changements (nouvelles menaces, mise-à-jour,…). Les évolutions rapides des systèmes, y compris des systèmes embarqués, implique des modifications des applications et des configurations des systèmes, en particulier au niveau logiciel. De tels changements peuvent avoir un impact sur la sûreté de fonctionnement et plus précisément sur les hypothèses des mécanismes de tolérance aux fautes. Un système est donc résilient si de pareils changements n’invalident pas les mécanismes de sûreté de fonctionnement, c’est-à-dire, si les mécanismes déjà en place restent cohérents malgré les changements ou dont les incohérences peuvent être rapidement résolues. Nous proposons tout d’abord dans cette thèse un modèle pour les systèmes résilients. Grâce à ce modèle nous pourrons évaluer les capacités d’un ensemble de mécanismes de tolérance aux fautes à assurer les propriétés de sûreté issues des spécifications non fonctionnelles. Cette modélisation nous permettra également de définir un ensemble de mesures afin de quantifier la résilience d’un système. Enfin nous discuterons dans le dernier chapitre de la possibilité d’inclure la résilience comme un des objectifs du processus de développement

Depuis 2000 les couplages sont devenus un très bon outil pour la conception de nouveaux protocoles cryptographiques. Les signatures courtes et le chiffrement basé sur l'identité sont devenus réalisables grâce aux couplages. Les travaux réalisés dans cette thèse comprennent deux aspects complémentaires. Une partie consiste en l'implémentation optimisée de couplages sur différentes courbes elliptiques, en fonction des protocoles visés. Une implémentation sur des courbes supersingulières en grande caractéristique et sur des courbes de Barreto-Naehrig est détaillée. La bibliothèque développée au Laboratoire Chiffre de Thales est utilisée avec des courbes de Barreto-Naehrig dans un protocole de diffusion chiffrée. La seconde application évalue la différence de temps de calcul pour des protocoles utilisant les couplages sur des courbes d'ordre composé (un large module RSA) et la traduction de ces protocoles qui utilise plusieurs couplages sur des courbes plus habituelles. Les résultats montrent une différence d'un facteur de 30 à 250 en fonction des étapes des protocoles, ce qui est très important. Une seconde partie porte sur deux familles de courbes de genre deux. Les jacobiennes de ces courbes sont isogènes au produit de deux courbes elliptiques sur une extension de corps de petit degré. Cette isogénie permet de transférer les propriétés des courbes elliptiques vers les jacobiennes. Le comptage de points est aisé et ne requiert qu'un comptage de points sur une des courbes elliptiques isogènes, plus quelques ajustements. On présente aussi la construction de deux endomorphismes à la fois sur les jacobiennes et sur les courbes elliptiques. Ces deux endomorphismes permettent des multiplications scalaires efficaces en suivant la méthode de Gallant, Lambert et Vanstone, ici en dimension quatre.

Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property related to the safety of critical systems, but its estimation requires sophisticated techniques. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks. The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation. We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET.

Depuis le milieu des années 1980, les variétés abéliennes ont été abondamment utilisées en cryptographie à clé publique: le problème du logarithme discret et les protocoles qui s'appuient sur celles-ci permettent le chiffrement asymétrique, la signature, l'authentification. Dans cette perspective, les jacobiennes de courbes hyperelliptiques constituent l'un des exemples les plus intéressants de variétés abéliennes principalement polarisées. L'utilisation des fonctions thêta permet d'avoir des algorithmes efficaces sur ces variétés. En particulier nous proposons dans cette thèse une variante de l'algorithme ECM utilisant les jacobiennes de courbes de genre 2 décomposables. Par ailleurs, nous étudions les correspondances entre les coordonnées de Mumford et les fonctions thêta. Ce travail a permis la construction de lois d'additions complètes en genre 2. Finalement nous présentons un algorithme de calcul d'isogénies entre variétés abéliennes. La majorité des résultats de cette thèse sont valides pour des courbes hyperelliptiques de genre quelconque. Nous nous sommes cependant concentré sur le cas du genre 2, le plus intéressant en pratique. Ces résultats ont été implémentés dans un package Magma appelé AVIsogenies.

Cette thèse est dédiée à la cryptanalyse de l'AES (Advanced Encryption Standard) qui est l'un des systèmes de chiffrement par bloc les plus répandu dans le monde. Nous y présentons une nouvelle technique pour résoudre un type particulier d'équations spécialement conçu pour attaquer l'AES. Cette technique est basée sur l'algèbre linéaire ainsi que sur la technique de la " Rencontre par le Milieu " et offre pour un système donné, plusieurs algorithmes de résolution de complexités différentes mais prédictibles. Ainsi nous avons conçu un programme pour trouver l'algorithme le plus rapide. Dans un premier temps nous l'avons appliqué directement aux systèmes d'équations décrivant un nombre réduit de tours d'AES et avons trouvé de nouvelles attaques lorsque la quantité de couples clair/chiffré est très limitée, améliorant celles trouvées manuellement par d'autres chercheurs. La technique étant générale nous avons pu utiliser le programme pour étudier d'autres modèles comme celui des attaques par fautes et celui des attaques à clé choisie ainsi que d'autres primitives cryptographiques comme la fonction d'authentification Pelican-MAC et le système de chiffrement par flot LEX. Enfin nous présentons une généralisation des attaques de Demirci et Selçuk publiées à la conférence FSE2008 ainsi qu'un algorithme qui nous a permis de trouver les meilleures attaques de cette classe, avec certaines parmi les meilleures connues à ce jour. Cet algorithme repose sur l'utilisation du précédent programme afin de déterminer le nombre de valeurs prises par des sous-ensembles d'octets de clé ou des états internes ainsi que la complexité de les énumérer.

Avec l'avènement de l'Internet grand public et des réseaux numériques, de nouvelles transactions ont vu le jour. Ces transactions, dites "électroniques", sont désormais omniprésentes et régissent notre vie quotidienne : accès par badge à un bâtiment, envoi d'un SMS ou d'un courriel, paiement sur internet, retrait d'argent à un distributeur,... Les transactions électroniques ont ouvert la voie à une multitude de possibilités déclinées sous diverses formes : le portail internet d'une banque pour consulter ses comptes, effectuer des virements ou passer des ordres en bourses; une carte à puce permettant d'ouvrir une porte ou de valider son titre de transport en commun; une application téléchargée sur un ordinateur ou un équipement mobile comme un assistant personnel numérique ou un téléphone portable. Cette dernière catégorie d'équipement mobile est extrêmement porteuse en terme d'offres de services. En effet, un mobile est un équipement nomade, connecté à l'Internet avec des débits de plus en plus élevés, et il est aussi de plus en plus puissant. Avec l'avènement de la technologie Near Field Communication et des architectures sécurisées, le mobile a maintenant la possibilité d'héberger des applications sensibles dans une puce sécurisée. Cette puce peut être la carte SIM, une puce embarquée soudée à l'électronique du mobile et une carte mémoire amovible sécurisée. Cette puce sécurisée est appelée Secure Element.Les contributions de cette thèse sont de deux ordres. Tout d'abord, nous nous sommes attachés à la conception d'une plateforme de génération automatique de scripts pour le déploiement des services mobile sans contact. Cette plateforme est basée sur une modélisation par les ontologies d'un Secure Element conforme à la spécification GlobalPlatform. Ensuite, nous avons élaboré une plateforme de test et d'analyse des transactions sans contact basée sur les techniques de fuzzing.

Les systèmes biométriques sont de plus en plus utilisés pour vérifier ou déterminer l'identité d'un individu. Compte tenu des enjeux liés à leur utilisation, notamment pour des applications dans le domaine de commerce électronique, il est particulièrement important de disposer d'une méthodologie d'évaluation de tels systèmes. Le problème traité dans cette thèse réside dans la conception d'une méthodologie générique visant à évaluer un système biométrique. Trois méthodes ont été proposées dans cette thèse: 1) une méthode de qualité sans référence pour prédire la qualité d'une donnée biométrique, 2) une méthode d'usage pour évaluer l'acceptabilité et la satisfaction des usagers lors de l'utilisation des systèmes biométriques et 3) une méthode d'analyse sécuritaire d'un système biométrique afin de mesurer sa robustesse aux attaques

Dans cette th ese, nous proposons et utilisons de nouvelles briques conduisant a des protocoles e caces dans le cadre d'une approche modulaire de la cryptographie. Tout d'abord dans un contexte non-interactif en s'appuyant sur les preuves Groth-Sahai, puis avec des interactions en permettant aux Smooth Projective Hash Functions de g erer de nouveaux langages. Dans un premier temps cette th ese s'appuie sur la m ethodologie introduite par Groth et Sahai pour des preuves de connaissance non-interactives pour d evelopper divers protocoles de signatures de groupe dans le mod ele standard, puis de signatures en blanc. Pour cela, nous proposons un syst eme permettant de signer un chi r e de mani ere telle que, sous r eserve de connaissance d'un secret ind ependant du protocole de signature, il soit possible de retrouver une signature sur un clair. Cette approche nous permet entre autre de proposer un protocole de signatures en blanc avec un nombre optimal d'interactions a la n duquel le demandeur peut utiliser une signature usuelle et ce sous des hypoth eses classiques dans le mod ele standard. Ensuite nous proposons une nouvelle m ethodologie pour faire des preuves implicites de connaissance dans un contexte interactif sans oracle al eatoire. Pour cela nous utilisons les smooth projective hash functions, dans un premier temps pour faire des Oblivious Signature-Based Envelopes, puis dans des protocoles d'authenti cation et de mise en accord de cl es. Ce faisant nous pr ecisons la notion de langage, et elargissons grandement le spectre des langages pouvant ^etre trait es a l'aide de ces SPHF. Gr^ace a ce r esultat nous introduisons le concept de LAKE (Language Authenticated Key Exchange) ou encore Echange de cl es authenti e par un langage : un moyen pour deux utilisateurs de se mettre d'accord sur une cl e si chacun poss ede un secret v eri ant une contrainte esp er ee par l'autre. Nous montrons alors comment instancier plusieurs protocoles d' echange de cl e sous ce regard plus effi cacement qu'avec les techniques actuelles, et nous prouvons la s ecurit e de nos instanciations dans le mod ele UC sous des hypoth eses usuelles.

Les attaques ciblant les systèmes informatiques vont aujourd'hui au delà de simples logiciels malveillants et impliquent de plus en plus des composants matériels. Cette thèse s'intéresse à cette nouvelle classe d'attaques et traite, plus précisément, des attaques par entrées-sorties qui détournent des fonctionnalités légitimes du matériel, tels que les mécanismes entrées-sorties, à différentes fins malveillantes. L'objectif est d'étudier ces attaques, qui sont extrêmement difficiles à détecter par des techniques logicielles classiques (dans la mesure où leur mise en oeuvre ne nécessite pas l'intervention des processeurs) afin de proposer des contre-mesures adaptées, basées sur des composants matériels fiables et incontournables. Ce manuscrit se concentre sur deux cas : celui des composants matériels qui peuvent être délibérément conçus pour être malveillants et agissants de la même façon qu'un programme intégrant un cheval de Troie ; et celui des composants matériels vulnérables qui ont été modifiés par un pirate informatique, localement ou au travers du réseau, afin d'y intégrer des fonctions malveillantes (typiquement, une porte dérobée dans son firmware). Pour identifier les attaques par entrées-sorties, nous avons commencé par élaborer un modèle d'attaques qui tient compte des différents niveaux d'abstraction d'un système informatique. Nous nous sommes ensuite appuyés sur ce modèle d'attaques pour les étudier selon deux approches complémentaires : une analyse de vulnérabilités traditionnelle, consistant à identifier une vulnérabilité, développer des preuves de concept et proposer des contre-mesures ; et une analyse de vulnérabilités par fuzzing sur les bus d'entrées-sorties, reposant sur un outil d'injection de fautes que nous avons conçu, baptisé IronHide, capable de simuler des attaques depuis un composant matériel malveillant. Les résultats obtenus pour chacunes de ces approches sont discutés et quelques contre-mesures aux vulnérabilités identifiées, basées sur des composants matériels existants, sont proposées.

La stéganographie est l'art de la communication secrète. L'objectif est de dissimuler un message secret dans un médium anodin de sorte qu'il soit indétectable. De nos jours, avec la généralisation d'Internet et l'apparition des supports numériques (fichiers audio, vidéos ou images), plusieurs philosophies de conception de schéma stéganographique ont été proposées. Parmi les méthodes actuelles appliquées aux images numériques naturelles, nous trouvons les méthodes d'insertion adaptative, dont le principe repose sur la modification du médium de couverture avec une garantie d'avoir un certain niveau de sécurité. Ces méthodes représentent une véritable avancée en stéganographie.Dans ce manuscrit, après avoir rappelé les concepts récents de stéganographie adaptative, nous présentons une procédure automatique et complète pour l'insertion adaptative de données secrètes dans des images numériques naturelles. L'approche proposée est une " méta-méthode " basée " oracle ", appelée ASO (Adaptive Steganography by Oracle), qui permet de préserver à la fois la distribution de l'image de couverture et la distribution de la base d'images utilisée par l'émetteur. Notre approche permet d'obtenir des résultats nettement supérieurs aux méthodes actuelles de l'état de l'art, et est donc l'une, si ce n'est la meilleure approche du moment. Par ailleurs, nous définissons également un nouveau paradigme en stéganographie qui est la stéganographie par base, ainsi qu'une nouvelle mesure de sélection pour les images stéganographiées, permettant d'améliorer encore plus les performances de notre schéma d'insertion. Les différentes expérimentations, que nous avons effectuées sur des images réelles, ont confirmé la pertinence de cette nouvelle approche.