|
RII à Nancy : cybersécurité, nouvelles technologies pour la protection des données et des systèmes numériques.
Jean-Karim Zinzindohoué de l'équipe-projet Prosecco : programmation sécurisée avec cryptographie. HACL* une bibliothèque cryptographique rapide et formellement vérifiée, sûre, correcte et sans canaux cachés.
Une bibliothèque cryptographique rapide et formellement vérifiée sûre, correcte et sans canaux cachés. Nous présentons HACL*, une bibliothèque cryptographique écrite en F* et compilée vers C. La vérification en F* garantit que le code source est sûr (memory-safe), fonctionnellement correct ainsi que l'absence de dépassements d'entiers et de certains types de fuite d'information par canaux cachés. La compilation s'appuie sur Kremlin, un compilateur de F* vers C, et une preuve formelle de la correction de cette transformation, et sur CompCert, un compilateur C vérifié. Nous illustrons l'usage de cette bibliothèque à travers une application de transfert de fichiers et une implémentation de référence de TLS.
|
