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) Hatchikian-Houdot, Jean-Loup - (2024-12-16) / Université de Rennes  - Mécanisme de sécurité contre les attaques temporelles via une coopération entre logiciel et matériel embarqué Accéder au document :  https://ged.univ-rennes1.fr/nuxeo/site/esupversion...

Langue : Anglais Directeur(s) de thèse:  Hiet, Guillaume Discipline : Informatique Laboratoire :  IRISA Ecole Doctorale : MATISSE Classification : Informatique Mots-clés : Coopération matériel/logiciel, Attaques temporelles contre le cache, Programmation temps constant Systèmes informatiques -- Mesures de sûreté Systèmes embarqués (informatique)

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