< Retour au sommaire

Vérification de temps constant cryptographique au niveau binaire

Mathéo Vergnolle le

Lieu: Salle 1073

L’application de la politique de temps constant cryptographique permet de se protéger de certaines attaques par canaux auxiliaires, notamment les attaques temporelles et les attaques par cache. Mais cette politique peut être complexe à mettre en place, elle n’est pas toujours préservée par le compilateur, et par ailleurs le code source des implémentations cryptographiques n’est pas toujours disponible (ex : intégrations de composants tiers). Il est donc nécessaire de réaliser une analyse au niveau du code exécutable (code binaire) pour en vérifier la bonne mise en place au niveau du code exécutable. La méthode d’analyse la plus efficace à ce jour est l’exécution symbolique relationnelle de Binsec/Rel, développée au CEA List, mais elle souffre encore de problèmes de passage à l’échelle sur certaines primitives. On propose ici une exécution symbolique hybride, avec un raisonnement relationnel à la demande et des optimisations dédiées pour permettre une vérification efficace de la propriété de temps constant au niveau binaire. Cette méthode permet de réduire grandement le surcoût lié à l’analyse de temps constant d’un programme, le rapprochant de celui d’une simple exploration symbolique. Notre solution parvient ainsi à réaliser en moins d’une seconde une analyse complète d’un AES qui n’est pas temps constant, là où Binsec/Rel n’y parvenait pas en une heure de calcul. Par rapport à Binsec/Rel, nous obtenons sur des programmes complexes une accélération moyenne d’un facteur ×17.5 pour les programmes qui vérifient la propriété de temps constant, et ×13615 pour ceux qui ne la vérifient pas.