Sites Inria

English version

Recherche

Equipe PROSECCO -

HACL*

HACL*

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.

Equipe :  PROSECCO

Site internet:  https://github.com/mitls/hacl-star

Mots-clés : Cryptographie Sécurité Vérification Preuve

Haut de page

Suivez Inria