Secure compilation against side channel attacks (Compilation sécurisée contre les attaques par canaux auxiliaires) Raimondi, Gautier - (2023-12-18) / Université de Rennes Secure compilation against side channel attacks Accéder au document :  https://ged.univ-rennes1.fr/nuxeo/site/esupversion...

Langue : Anglais Directeur(s) de thèse:  Jensen, Thomas; Besson, Frédéric Discipline : Informatique Laboratoire :  IRISA Ecole Doctorale : MATISSE Classification : Informatique Mots-clés : Compilation Sécurisée, Constant-Time, Vérification Formelle, Transformation de Programme Compilation (informatique) Langages formels Méthodes formelles (informatique) Cyberdéfense Langages de programmation -- Sémantique

Résumé : 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. Abstract : 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.