Université de Rennes 1 Vérification d'implémentations constant-time dans une chaîne de compilation vérifiée Verifying constant-time implementations in a verified compilation toolchain Vérification formellecompilationcanaux cachésCoqCompCertVerascoconstant-timeanalyse statique Formal verificationcompilationside-channelsCoqCompCertVerascoconstant-timestatic analysis Logiciels -- Vérification Thèses et écrits académiques Les attaques par canaux cachés sont une forme d'attaque particulièrement dangereuse. Dans cette thèse, nous nous intéressons au canal caché temporel. Un programme est dit ''constant-time'' lorsqu'il n'est pas vulnérable aux attaques par canal caché temporel. Nous présentons dans ce manuscrit deux méthodes reposant sur l'analyse statique afin de s'assurer qu'un programme est constant-time. Ces méthodes se placent dans le cadre de vérification formelle afin d'obtenir le plus haut niveau d'assurance possible en s'appuyant sur une chaîne de compilation vérifiée composée du compilateur CompCert et de l'analyseur statique Verasco. Nous proposons aussi une méthode de preuve afin de s'assurer qu'un compilateur préserve la propriété de constant-time lors de la compilation d'un programme. Side-channel attacks are an especially dangerous form of attack. In this thesis, we focus on the timing side-channel. A program is said to be constant-time if it is not vulnerable to timing attacks. We present in this thesis two methods relying on static analysis in order to ensure that a program is constant-time. These methods use formal verification in order to gain the highest possible level of assurance by relying on a verified compilation toolchain made up of the CompCert compiler and the Verasco static analyzer. We also propose a proof methodology in order to ensure that a compiler preserves constant-time security during compilation. Electronic Thesis or DissertationText en application/pdf1 : 1893 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/93e19454-ed5e-43f1-8d77-9267def7735d Trieu Alix 1991-06-04 FR 236436546 trieu.alix@gmail.com 2018REN1S099 http://www.theses.fr/2018REN1S099 2018-12-04 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiBlazySandrineintervenant_1153042567PichardieDavidintervenant_2093668392 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 IRISA partenaireRecherche_2 026386909 ddc:004 BlazySandrinePichardieDavidUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) IRISA ASCII PDF 1938414