Polubelova, Marina
[Author]
;
Université Paris sciences et lettres
[Contributor];
Bhargavan, Karthikeyan
[Contributor]
Construction d'une bibliothèque cryptographique multi-plateformes formellement vérifiée à haute performance en F* ; Building a formally verified high-performance multi-platform cryptographic library in F*
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Construction d'une bibliothèque cryptographique multi-plateformes formellement vérifiée à haute performance en F* ; Building a formally verified high-performance multi-platform cryptographic library in F*
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Beaucoup de logiciels critiques d'un point de vue sécurité ont besoin d'implémentations d'algorithmes cryptographiques sûres et performantes. Pour répondre à ce besoin, des bibliothèques cryptographiques généralistes comme OpenSSL incluent des douzaines d'implémentations hybrides C/Assembleurs pour chaque primitive, chacune de ces implémentations étant spécialisée et optimisée pour une plateforme répandue. La plupart des optimisations présentes dans ces implémentations exploitent le parallélisme Single Instruction, Multiple Data (SIMD) qui nécessite de changer de manière significative la structure du code, de telle sorte qu'il ne ressemble plus que très peu à l'algorithme scalaire originel. Cependant, et malgré des années de conception et d'implémentation méticuleuse, des bugs et attaques continuent d'être trouvées dans ces bases de code optimisées. Ces bugs et attaques incluent des erreurs de sûreté mémoire, des fuites d'information par attaque temporelle et des bugs de correction fonctionnelle. La probabilité de détecter ces bugs par des méthodes de test est extrêmement faible, mais ils peuvent quand même être exploités pour conduire une attaque. Nous défendons l'utilisation de méthodes formelles afin de prouver mathématiquement l'absence de tels bugs dans les implémentations. À l'inverse d'autres approches comme le test ou l'audit, l'utilisation de méthodes formelles apporte des garanties forte concernant la sûreté mémoire du code, sa correction fonctionnelle par rapport à une spécification hautniveau, et enfin son indépendance par rapport aux données secrètes (constant-time) qui protège contre certaines attaques temporelles par canaux auxiliaires. Le défi est ici de vérifier des centaines de milliers de lignes de code extrêmement optimisées ; nous avons donc besoin d'une approche systématique à ce problème. Cette dissertation présente une nouvelle approche pour la construction d'une bibliothèque cryptographique multiplateforme formellement vérifiée qui compile du code générique vérifié écrit en F? vers du ...