SCD-Universite de Rennes 1 Mécanisme de sécurité contre les attaques temporelles via une coopération entre logiciel et matériel embarqué Constant time security through cooperation between software and embedded hardware Coopération matériel/logicielAttaques temporelles contre le cacheProgrammation temps constant Hardware/Software co-designTiming cache attacksConstant-time programming Systèmes informatiques -- Mesures de sûreté Systèmes embarqués (informatique) La programmation temps constant est utilisée pour produire des programmes immunisés contre les attaques temporelles. Cependant, cette discipline impose plusieurs contraintes au développeur de logiciels, ce qui rend la mise en œuvre complexe et les programmes résultants parfois plus lents. Nous proposons un nouveau mécanisme de protection spécialisé pour les systèmes embarqués qui est implémenté dans le matériel mais utilisable à partir du logiciel. Grâce à cette protection, les contraintes de la programmation temps constant peuvent être assouplies, ce qui rend cette discipline plus simple et permet de produire des programmes plus rapides. Cette protection fonctionne en verrouillant des parties de la mémoire dans le cache, de sorte que les accès vers ces parties de la mémoire soient protégés contre les attaques temporelles. Nous réutilisons les techniques de preuve utilisées pour certifier le compilateur CompCert. Dans notre cas, nous l'utilisons pour certifier qu'aucune attaque par cache ne peut exposer nos accès mémoire protégés. Nous montrons le gain de performance permis par notre nouvelle protection sur plusieurs algorithmes cryptographiques, et nous proposons une nouvelle méthode de tri rapide qui est temps constant grâce ce mécanisme de verrouillage du cache. Constant-time programming is used to produce programs immune to timing attacks. However, this discipline imposes several constraints on the software developer, making implementation complex and sometimes slow. We propose a new protection mechanism specialized for embedded systems and implemented in hardware but usable from software. With this protection, the constraints of constant-time programming can be relaxed, making constant-time secure programs easier to produce and faster in several cases. This protection works by locking chunks of the memory in the cache, such that memory accesses toward these chunks are protected against timing attacks. We reuse proof techniques used to formally verify the CompCert compiler. In our case, we use it to certify that no cache attacks could expose our protected memory accesses. We show the performance gain allowed by our new protection on several cryptographic algorithms, and we propose a new fast sorting method that is constant-time with this cache-locking mechanism. Electronic Thesis or DissertationText en application/pdf1 : 1536 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/f58f57ad-0923-4417-b79f-286436bc2212 Hatchikian-Houdot Jean-Loup 1996-12-14 FR 284518476 jhatchik@laposte.net 2024URENS101 http://www.theses.fr/2024URENS101 2024-12-16 Informatique Université de Rennes thesis.degree.grantor_1 26693823X Doctorat non ouiHietGuillaumeintervenant_1133411206PierreLaurenceintervenant_2075611341HietGuillaumeintervenant_1133411206BessonFrédéricintervenant_3070000182WilkePierreintervenant_4199148848GrimaudGillesintervenant_5122743083FrancillonAurélienintervenant_6197695663 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 HietGuillaumePierreLaurenceBessonFrédéricWilkePierreGrimaudGillesFrancillonAurélienUniversité de Rennes MATISSE IRISA ASCII PDF 1572756