Apple met en ligne une nouvelle version du code source de corecrypto sur GitHub, accompagnée d’un billet technique détaillant ses travaux de cryptographie post‑quantique sur iPhone, Mac et d’autres plateformes.
Une étape de plus après PQ3 dans iMessage
Cette publication s’inscrit dans la continuité des efforts engagés publiquement en 2024 avec PQ3, le protocole post‑quantique d’iMessage annoncé avec iOS 17.4 (Apple Security Research). PQ3 ajoute une protection post‑quantique lors du démarrage d’une conversation, ainsi qu’au fil du temps lorsque les clés de chiffrement sont renouvelées.
Ce que contient le dépôt corecrypto
Le dépôt github.com/apple/corecrypto regroupe le code source de corecrypto, la bibliothèque cryptographique de bas niveau utilisée notamment par Security framework, CryptoKit et CommonCrypto pour le chiffrement, le hachage, la génération de nombres aléatoires et les signatures numériques.
- Implémentations ML‑KEM et ML‑DSA, les deux algorithmes post‑quantiques retenus par Apple pour corecrypto
- Tests, outils de performance et cibles de compilation destinés à l’évaluation et à l’intégration
- Dossier dédié à la vérification formelle, avec éléments de preuve et outils associés
Selon Apple, cette partie de vérification vise notamment à contrôler la conformité des implémentations avec FIPS 203 et FIPS 204, les standards du NIST pour ML‑KEM (établissement de clés) et ML‑DSA (signatures), conçus pour répondre aux menaces attendues des ordinateurs quantiques.
Pourquoi Apple insiste sur la vérification formelle
En parallèle du dépôt, Apple publie un article technique expliquant la méthode employée pour vérifier ce code avant ouverture à l’examen externe (Apple Security Research). Apple décrit un processus mêlant tests classiques, simulation, revue indépendante et vérification formelle interne.
Le groupe indique avoir dû élaborer une approche spécifique, corecrypto devant fonctionner sur l’ensemble de la gamme, y compris avec différentes déclinaisons d’Apple silicon. Les implémentations combinent du C portable et de l’assembleur ARM64 optimisé, ce qui limite l’efficacité d’approches de vérification « sur étagère ».
Apple explique que ce travail a permis d’identifier des problèmes qui auraient pu échapper aux seules batteries de tests, dont une étape manquante dans une implémentation précoce de ML‑DSA susceptible, dans de rares cas, de produire une sortie incorrecte, ainsi qu’une erreur dans une preuve tierce corrigée pour les paramètres utilisés.
Parmi les ressources fournies aux chercheurs, Apple cite le document « Formal verification for Apple corecrypto », un outil de traduction Cryptol‑to‑Isabelle (référence) et des théories Isabelle disponibles dans l’archive source (Apple_Isabelle_Libraries).
