​Le CEA-List a déployé depuis plusieurs années des outils fondés sur les méthodes formelles pour vérifier l'absence de bugs dans les programmes. S'ils se sont avérés très efficaces pour lutter contre les attaques usuelles, ils le sont moins pour détecter des attaques d'un nouveau type, les attaques par canaux auxiliaires, qui exploitent les propriétés physiques de l'exécution d'un programme pour faire fuiter des informations. Parmi elles, les attaques temporelles visent à décoder les clés de cryptographie en comparant les temps de traitement de différentes opérations par un programme.

L'une des parades pour lutter contre ce type de piratage est une technique de codage dite « constant time ». Il s'agit de faire en sorte que le temps d'exécution d'une tâche, par exemple la vérification d'un mot de passe, ne dépende pas de la donnée d'entrée.
Cette discipline de programmation étant particulièrement délicate à mettre en œuvre, les chercheurs du CEA-List ont développé un outil capable de vérifier automatiquement qu'un code respecte la contrainte du « constant time ». Intégré sur la plate-forme d'analyse de code BINSEC, le module REL a été testé avec succès sur 338 implémentations cryptographiques.

Présenté à la conférence internationale IEEE Symposium on Security & Privacy 2020, ce travail ouvre la voie au développement de méthodes d'analyse de code dédiées à la prévention d'autres types d'attaques, et à une sécurisation renforcée et automatisée des programmes cryptographiques.