Chercheurs du Institut d'État de recherche en informatique et en automatisation (INRIA), Présentation de Microsoft Research et de l'Université Carnegie Mellon la première édition d'essai de la bibliothèque cryptographique EverCrypt développé dans le cadre du projet Everest et utilisant des méthodes mathématiques de vérification formelle de fiabilité.
Pour ses capacités et ses performances, EverCrypt est très proche des bibliothèques cryptographiques existantes (OpenSSL) mais qui, contrairement à eux, offre des garanties supplémentaires de fiabilité et de sécurité.
Par exemple, le processus de vérification se résume à la définition de spécifications détaillées qui décrivent tous les comportements du programme et la preuve mathématique que le code écrit répond aux spécifications préparées.
Contrairement aux méthodes de contrôle de la qualité fondées sur des preuves, la vérification fournit des garanties fiables que le programme ne s'exécutera que comme prévu par les développeurs et qu'il n'y a pas de classes d'erreurs spécifiques.
Par exemple, la conformité à la spécification garantit un travail sûr avec la mémoire et l'absence d'erreurs entraînant un dépassement de mémoire tampon, pour déréférencer des pointeurs, pour accéder à des zones mémoire déjà libérées, ou pour doubler la libération de blocs mémoire.
Qu'est-ce qu'EverCrypt?
ToujoursCrypte fournit une vérification robuste du type et de la valeur- Un composant ne passera jamais de paramètres à l'autre composant non conforme et n'aura pas accès aux états internes des autres composants.
Le comportement d'entrée / sortie entièrement conforme aux actions de fonctions mathématiques simples, qui sont définis dans les normes cryptographiques.
Pour se protéger des attaques dans des canaux tiers, comportement lors des calculs (par exemple, la durée de l'exécution ou la présence d'accès à certaines mémoires) cela ne dépend pas des données secrètes traitées.
Le code du projet est écrit dans le langage fonctionnel F * (Étoile F) , qui fournit un système de types dépendants et de raffinements, qui permettent d'établir des spécifications exactes (modèle mathématique) pour les programmes et de garantir l'exactitude et l'absence d'erreurs dans la mise en œuvre au moyen de formules SMT et d'outils de test auxiliaires.
Le code en F * est distribué sous la licence Apache 2.0, et les derniers modules en C et l'assembleur sous la licence MIT.
Sur la base du code de référence F *, assembleur, C, OCaml, JavaScript est généré et le code d'assemblage Web.
Certaines parties du code préparé par le projet sont déjà utilisés dans Firefox, le noyau Windows , la blockchain de Tezos et VPN Wireguard.
Composants EverCrypt
En substance, EverCrypt combine deux projets auparavant disparates de HACL * et Vale, en fournissant une API unifiée basée sur eux et en les rendant aptes à une utilisation dans de vrais projets.
HACL * est écrit en Low* et son objectif est de fournir des primitives cryptographiques à utiliser dans les programmes C qui ils utilisent les API de style libsodium et NaCL.
Le projet Vale a développé un langage spécifique domaine pour créer des vérifications dans l'assembleur.
Environ 110 mille lignes de code HACL * en langage Low * et 25 mille lignes de code pour Vale sont combinées et ils sont réécrits dans environ 70 lignes de code dans le langage universel F *, qui est également en cours de développement dans le cadre du projet Everest.
La première version de la bibliothèque EverCrypt fonctionnalités mises en œuvre vérifiées des algorithmes cryptographiques suivants proposé en version C ou assembleur (lors de l'utilisation du.
Parmi ceux-ci, les suivants se démarquent sur la page du projet:
- Algorithmes de hachage: toutes les variantes de SHA2, SHA3, SHA1 et MD5
- Codes d'authentification: HMAC sur SHA1, SHA2-256, SHA2-384 et SHA2-512 pour l'authentification de la source de données
- Algorithme de génération de clé HKDF (fonction de dérivation de clé d'expansion et d'extraction basée sur HMAC)
- Cryptage de flux ChaCha20 (version C non optimisée disponible)
- Algorithme d'authentification de message (MAC) Poly1305 (version C et assembleur)
- Protocole Diffie-Hellman sur courbes elliptiques Curve25519 (versions C et assembleur avec optimisations basées sur les instructions BMI2 et ADX)
- Mode de chiffrement par bloc AEAD (chiffrement authentifié) ChachaPoly (version C non optimisée)
- Mode de chiffrement par bloc AEAD AES-GCM (version assembleur avec optimisations AES-NI).
En premier version alpha, la vérification du code est déjà terminée en grande partie, mais il y a encore des domaines non couverts.
En outre, L'API n'est pas encore stabilisée, qui sera élargi dans les versions alpha suivantes (Il est prévu d'unifier les structures pour toutes les API.
Parmi les failles, le support de l'architecture x86_64 est également mis en évidence (dans la première étape, l'objectif principal est la fiabilité, tandis que l'optimisation et les plates-formes seront implémentées dans un second temps).
source: https://jonathan.protzenko.fr