Université de Rennes Secure compilation against side channel attacks Compilation sécurisée contre les attaques par canaux auxiliaires Compilation SécuriséeConstant-TimeVérification FormelleTransformation de Programme Secure CompilationConstant-TimeFormal VerificationProgram Transformation Compilation (informatique) Langages formels Méthodes formelles (informatique) Cyberdéfense Langages de programmation -- Sémantique De par leur omniprésence, la sécurité des systèmes informatiques est un enjeu majeur. Dans cette thèse, nous visons à garantir une sécurité contre un certain type d'attaque : les attaques par canal caché temporel. Ces attaques utilisent le temps d'exécution d'un programme pour déduire des informations sur le système. En particulier, on dit d'un programme qu'il est constant-time lorsqu'il n'est pas sensible à ce type d'attaques. Cela passe par des contraintes sur le programmes, qui ne doit ni réaliser de décisions en utilisant de valeurs secrètes, ni utiliser un de ces secrets pour accéder à la mémoire. Nous présentons dans ce document une méthode permettant de garantir la propriété constant-time d'un programme. Cette méthode est une transformation à haut niveau, suivi d'une compilation par Jasmin pour préserver la propriété. Nous présentons également la preuve de la sécurité et de la préservation sémantique de cette méthode. Given their ubiquity, the security of computer systems is a major issue. In this thesis, we aim to guarantee security against a certain type of attack: timing side-channel attacks. These attacks use the execution time of a program to deduce information about the system. In particular, a program is said to be constant-time when it is not sensitive to this type of attack. This requires constraints on the program, which must neither make decisions using secret values, nor use one of these secrets to access memory. In this document, we present a method for guaranteeing the constant-time property of a program. This method is a high-level transformation, followed by compilation using Jasmin to preserve the property. We also present a proof of the security and semantic preservation of this method. Electronic Thesis or DissertationText en application/pdf1 : 1299 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/1d849a4e-63a8-4e92-9356-f7b18ebb4780 Raimondi Gautier 1998-09-22 FR 277014026 gautier.raimondi@gmail.com 2023URENS094 http://www.theses.fr/2023URENS094 2023-12-18 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiJensenThomasintervenant_1059884959BessonFrédéricintervenant_2070000182BlazySandrineintervenant_3153042567JensenThomasintervenant_1059884959BessonFrédéricintervenant_2070000182SignolesJulienintervenant_6111306469MerzStephanintervenant_4120558513ConchonSylvainintervenant_5073639206 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 JensenThomasBessonFrédéricBlazySandrineMerzStephanConchonSylvainSignolesJulienUniversité de RennesMATISSE IRISA ASCII PDF 1330657