Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Formal sofwtare methods for cryptosystems implementation security Pablo Rauzy T

Formal sofwtare methods for cryptosystems implementation security Pablo Rauzy To cite this version: Pablo Rauzy. Formal sofwtare methods for cryptosystems implementation security. Cryp- tography and Security [cs.CR]. T´ el´ ecom ParisTech, 2015. English. ¡ NNT : 2015ENST0039 ¿. HAL Id: tel-01341676 https://pastel.archives-ouvertes.fr/tel-01341676 Submitted on 4 Jul 2016 HAL is a multi-disciplinary open access archive for the deposit and dissemination of sci- entiﬁc research documents, whether they are pub- lished or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers. L’archive ouverte pluridisciplinaire HAL, est destin´ ee au d´ epˆ ot et ` a la diﬀusion de documents scientiﬁques de niveau recherche, publi´ es ou non, ´ emanant des ´ etablissements d’enseignement et de recherche fran¸ cais ou ´ etrangers, des laboratoires publics ou priv´ es. T H È S E 2015-ENST-0039 EDITE - ED 130 Doctorat ParisTech T H È S E pour obtenir le grade de docteur délivré par TELECOM ParisTech Spécialité « Informatique » présentée et soutenue publiquement par Pablo Rauzy le 13 juillet 2015 Méthodes logicielles formelles pour la sécurité des implémentations cryptographiques Directeur de thèse: Sylvain Guilley Jury M. François DUPRESSOIR, Chercheur, IMDEA Software Institute Examinateur M. Pierre-Alain FOUQUE, Professeur, Université Rennes 1 Rapporteur Mme. Karine HEYDEMANN, Maître de Conférence, UPMC Examinatrice M. David NACCACHE, Professeur, Université Panthéon-Assas Président Mme. Marie-Laure POTET, Professeure, Ensimag Rapporteuse M. Medhi TIBOUCHI, Chercheur, NTT Examinateur M. David VIGILANT, Chercheur, Gemalto Invité TELECOM ParisTech école de l’Institut Mines-Télécom - membre de ParisTech 46 rue Barrault 75013 Paris - (+33) 1 45 81 77 77 - www.telecom-paristech.fr 2 Refaire un peu le monde en posant des questions, Essayer d’y répondre avec de la technique, Créer l’étonnement, être pédagogique. Haïssant les erreurs, aimant les suggestions, Ecrire des papiers et des présentations. Riez de cette fable en vérité tragique Cachant tant bien que mal la formule magique : “H-index labidex !”. Comptez vos citations Et multipliez par, un jour de Lune noire, Le nombre de majeurs se levant à leur gloire, Inﬂexiblement droits, des mains des éditeurs. Bien ! Vous venez de faire un petit peu de science Résolument valide. . . aux yeux de la ﬁnance. Et si nous disions “zut” à ces inquisiteurs ? ∼p4bl0 3 4 0x0 Avant-propos 0.1 Contexte Ma thèse s’est déroulée à Télécom ParisTech, dans les locaux situés rue Dareau dans le 14ème arrondissement de Paris, au sein de l’équipe SEN (Sécurité Électronique Numérique) du département COMELEC (Communication et Électronique) du LTCI (Laboratoire Traitement et Communication de l’Information, UMR 5141 commune avec le CNRS). Les activités de l’équipe se focalisent autour de trois thèmes de recherche : ◦les contraintes de sécurité sont traitées dans la thématique Matériel pour l’informatique sécurisée et de conﬁance (Trusted Computing Hardware) ; ◦les contraintes de ﬁabilité sont traitées dans la thématique Analyse et concep- tion de processeurs ﬁables basés sur des technologies non ﬁables (Analysis and Design of Reliable Processeurs Based on Unreliable Technologies) ; ◦les contraintes de complexité et de consommation sont traitées dans la théma- tique Architectures optimales pour l’implémentation d’algorithmes complexes (Optimal Architectures for Complex Algorithms Implementations). Ma thèse se positionne dans le premier de ces trois thèmes, avec la particu- larité de s’attaquer au problème de la conﬁance en le matériel au niveau logiciel, puisque je suis informaticien d’origine. Je me suis ainsi positionné à l’interface en- tre deux mondes, celui de l’informatique théorique, d’où je venais après mes trois années passées à l’étudier à l’ENS, et celui du matériel, plus particulièrement de l’électronique embarquée. Au niveau de cette interface, c’est à la cryptologie et aux méthodes formelles que je me suis intéressé. Cette thèse a été encadrée par Sylvain Guilley et a été ﬁnancée par une bourse ministérielle obtenue via l’école doctorale ÉDITE (ED130). J’ai aussi bénéﬁcié d’une mission doctorale d’enseignement, que j’ai eﬀectuée à Polytech’UPMC. Les deux premières années, j’ai encadré au premier semestre les séances de TP du cours de “Programmation en C” des étudiant·e·s de 3ème année de la formation EI2I (Électronique et Informatique parcours Informatique Industrielle), et au second semestre les séances de TP du cours de “Développement Web” des étudiant·e·s de 3ème année de la formation AGRAL (Agroalimentaire). La troisième année, j’ai été seul en charge du cours de “Programmation orienté objet et langage C++” des étudiant·e·s de 4ème année de la formation EISE (Élec- tronique et informatique parcours Systèmes Embarqués). J’ai pu concevoir, donner, et évaluer les cours, les TP, les examens sur papier et sur machine, ainsi que les projets de ce module. Cela m’a permis d’expérimenter l’intégralité des aspects de l’enseignement d’un cours. 5 CHAPTER 0. AVANT-PROPOS 0.2 Remerciements Je vais commencer ces remerciements par les personnes qui m’ont permis de réaliser ma thèse en m’acceptant dans leur équipe malgré mon arrivée de dernière minute, en catastrophe : Jean-Luc Danger et Sylvain Guilley. Je tiens à remercier Sylvain tout particulièrement car c’est lui qui en pratique a encadré ma thèse, et je ne pense pas que quiconque aurait pu être un meilleur encadrant pour moi. Sylvain a su me laisser énormément d’autonomie et de liberté, tout en étant très présent lorsque je le sollicitais. Sur le plan scientiﬁque, il m’a laissé d’immenses marges de manœuvre dans nos articles et dans mes présentations, en m’oﬀrant des conseils précieux sans jamais rien m’imposer. Sur le plan personnel, il m’a laissé — sans m’en tenir rigueur — prendre du temps pour des activités annexes, commme travailler sur des projets avec le club Inutile1 (même à l’approche d’une échéance !), ou militer pour le libre accès à la recherche2. Son optimisme naturel et sa bonne humeur ont su me remotiver chaque fois que j’en ai eu besoin. Même si nous avons beaucoup moins travaillé ensemble, nombre de mes discus- sions avec Jean-Luc m’ont été utiles, et surtout, je voudrais ici rendre un hommage à sa pratique du jeu-de-mot-naze, que j’apprécie le plus sincèrement du monde, comme mes amis proches3 pourraient en témoigner. Ensuite, je veux remercier les membres de mon jury. Je suis extrêmement honoré que François Dupressoir, Pierre-Alain Fouque, Karine Heydemann, David Naccache, Marie-Laure Potet, Mehdi Tibouchi, et David Vigilant aient accepté de compter parmi les membres de mon jury de thèse. J’adresse naturellement un remerciement spécial à Marie-Laure et Pierre-Alain qui jouent pour ma thèse l’important rôle de rapporteu·se/r et qui m’ont permis grâce à leurs remarques d’améliorer sensiblement la qualité de mon tapuscrit. Un remerciement singulier va à David Naccache, qui a été mon professeur à l’École normale supérieure : je garde un génial souvenir de son cours d’Informatique scientiﬁque par la pratique qui m’a permis de voir pour la première fois ce que c’était que la recherche de l’intérieur, notamment la rédaction collaborative d’un article. En restant pour l’instant dans le monde de la recherche, je veux maintenant remercier tous les membres de l’équipe SEN. Des remerciements particuliers vont à Zakaria Najm, ingénieur de recherche au labo dit “ZakGyver”, pour son eﬃcacité et sa disponibilité impressionnantes, et pour tout le travail que l’on a fait ensemble, notamment les soirées pré-échéances que l’on a passées à travailler dans la bonne humeur. Il en va de même pour Taouﬁk Chouta, avec qui j’ai partagé mon bureau et de nombreuses rigolades pendant les deux premières années de ma thèse. Je tiens aussi à remercier Martin Moreau, qui est venu faire son stage de M2 avec Sylvain et moi. On s’est immédiatement très bien entendu, et j’espère sincèrement qu’il pourra continuer notre travail pendant sa thèse à partir de l’an prochain. Je remercie également les nombreuses autres personnes de la communauté scien- tiﬁque avec qui j’ai pu échanger lors de conférences, de séminaires, ou simplement par courriel. En particulier je voudrais chaleureusement remercier Gilles Barthe, Pierre-Yves Strub et François Dupressoir pour m’avoir invité à l’IMDEA Software Institute à Madrid, où j’ai passé un super mois. 1http://inutile.club/index.php?n=Activites.ProjectSK 2http://pablo.rauzy.name/openaccess.html 3Par exemple ceux qui l’appellent “Dr. Danger”, parce que c’est super classe. 6 Pablo Rauzy Formal Software Methods for Cryptosystems Implementation Security J’en viens maintenant à remercier ma famille. Ma sœur Nina, qui est actuelle- ment très occupée par sa noble mission consistant à parcourir le monde pour y répandre sa bonne humeur et la façon de Marseille. Mes petits frères, Raphaël et Manuel, qui sont une source inépuisable de joie de vivre. Mes parents, Magali Marcel et Antoine Rauzy, qui sont je pense les plus géniaux du monde, il n’y a pas vraiment besoin d’en dire plus. Ma belle-mère Anna aussi, qui fait partie de ma famille depuis plus de 10 ans maintenant. Enﬁn, tous les autres membres de ma famille moins proche : mes grands-parents, oncles, cousin, grands-cousin·e·s, et petits-neveux (et tous les {n,m}-parents qui existeraient mais n’entreraient pas dans les cases citées). Au tour des ami·e·s. C’est avec eux que j’ai passé l’essentiel de mon temps ces dernières années. Et c’est en grande partie grâce à eux aussi que ma vie est si géniale. Par souci de simplicité, je vais faire ça dans l’ordre chronologique. Je commence donc par remercier tou·te·s mes uploads/Science et Technologie/ these-rauzy.pdf