Soutenance de thèse de Solène Mirliaz : "Analyse statique relationnelle de coût sur architecture superscalaire"

J'ai le plaisir de vous inviter à ma soutenance de thèse qui aura lieu le 16 décembre 2024 à l’ENS Rennes, en salle du conseil, à 14h00.

Résumé :

Avec leur utilisation intensive, les primitives cryptographiques sont optimisées pour économiser des cycles processeur. Les cryptographes optimisent leur fonction à la main en ayant en tête les mécanismes des processeurs modernes.

Cette thèse a pour but de faciliter l'évaluation du coût d'un programme sur une architecture moderne où les instructions peuvent être spéculées et parallélisées. L'analyse automatique du coût se base sur l'interprétation abstraite du programme pour obtenir un invariant liant le coût du programme à la taille de son entrée, ce qui en fait un invariant relationnel. L'accent est mis sur la définition d'une sémantique d'un processeur et la preuve de correction de l'analyse statique finale. Cette preuve est menée progressivement via des sémantiques intermédiaires.

Les analyses numériques relationnelles étant coûteuses par nature, la thèse se penche également sur la conception d'une analyse statique numérique relationnelle qui serait flot-insensitive, c'est-à-dire qui ne conserverait qu'un invariant pour tout le programme. Cette analyse serait réalisable grâce à une représentation particulière du programme dont on donne les propriétés et l'algorithme d’obtention.

Title : Relational static cost analysis for superscalar architecture

Abstract :

Cryptographic primitives are executed extensively and thus cryptographers sought after saving processor cycles. They hand-optimize their primitives with the mechanisms of modern processors in mind.
This thesis aimed at easing the evaluation of the cost of a program on a modern architecture where the instructions can be speculated and parallelized. The analysis is based on abstract interpretation of the program to obtain a sound invariant linking the cost of the program to the size of its input. This is a relational invariant. This document focuses on the definition of a semantic for the processor and the proof of soundness of the final static analysis. The proof is made step by step through intermediate semantics.
Relational analyses are inherently costly, and thus the thesis also studies the conception of a flow-insensitive relational numerical static analysis. Such analyses have only one invariant but require a specific program representation whose properties are given in this document. The algorithm to obtain this program representation is also presented.