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

J'ai le plaisir de vous convier à ma soutenance de thèse qui aura lieu le lundi 16 décembre à 9h00 en salle Petri/Turing.

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 grace ce mécanisme de verrouillage du cache.

The Defense will take place on December 16th, 9am, in room Petri-Turing.

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,