Apple a publié le 22 mai 2025 le code source de corecrypto sur GitHub. Cette bibliothèque cryptographique de bas niveau alimente le chiffrement, le hachage, la génération de nombres aléatoires et les signatures numériques sur iPhone, Mac et l’ensemble de ses appareils.
Cette publication s’inscrit dans la continuité des travaux post-quantiques engagés par Apple depuis 2024, date à laquelle le protocole PQ3 avait été introduit dans iMessage avec iOS 17.4.
A lire aussi
- Tineco dévoile une flopée de nouveaux produits à l’IFA, votre maison va être plus propre que jamais
- iPhone 18 : Apple préparerait un bouleversement majeur dans la gamme
Ce que contient le dépôt GitHub
Le dépôt rendu public inclut les implémentations d’Apple pour ML-KEM et ML-DSA, les deux algorithmes post-quantiques retenus pour corecrypto. Ces algorithmes correspondent aux standards FIPS 203 et FIPS 204 publiés par le NIST.
ML-KEM sert à établir des clés de chiffrement sécurisées, tandis que ML-DSA est utilisé pour les signatures numériques. Les deux sont conçus pour résister aux menaces que pourraient poser des ordinateurs quantiques suffisamment puissants.
Le dépôt comprend également des outils de test et de performance, des cibles de compilation, ainsi qu’un dossier dédié à la vérification formelle. Ce dernier rassemble les preuves et les outils utilisés pour s’assurer que les implémentations respectent bien les standards du NIST.
Une vérification formelle sur mesure
Apple a développé une approche de vérification propre, car les outils existants ne couvraient pas l’ensemble de ses besoins. La bibliothèque corecrypto doit fonctionner sur toute la gamme de produits Apple, qui repose sur différentes générations de puces Apple Silicon.
Les implémentations combinent du code C portable et du code assembleur ARM64 optimisé à la main pour tirer parti des processeurs maison. Cette hétérogénéité rendait les méthodes de vérification classiques insuffisantes.
Cette rigueur a eu des conséquences concrètes. Apple indique avoir identifié, grâce à ce processus, une étape manquante dans une première version de son implémentation ML-DSA : dans de rares cas, des entrées auraient pu dépasser la plage attendue et produire un résultat incorrect, sans qu’aucun test classique ne le détecte. Un autre bug avait été repéré dans une preuve tierce, qu’Apple a corrigé de façon indépendante.
Un geste vers la communauté de la sécurité
En plus du code, Apple a publié sur son blog Security Research une note technique détaillant sa démarche. L’entreprise met à disposition trois ressources complémentaires : un article académique sur la vérification formelle appliquée à corecrypto, un traducteur Cryptol-vers-Isabelle développé en interne, et des théories Isabelle intégrées à l’archive source.
Ces outils permettent à des experts extérieurs de reproduire et d’évaluer les preuves formelles produites par Apple. L’objectif affiché est d’encourager une adoption plus large de ces méthodes et d’ouvrir le travail d’Apple à un examen critique indépendant.
La publication intervient dans un contexte où plusieurs organisations gouvernementales et industrielles accélèrent leur migration vers des standards résistants aux ordinateurs quantiques. En rendant son code accessible, Apple positionne ses choix techniques comme une référence potentielle pour l’ensemble du secteur.
Source : 9to5Mac
