Apple publie une nouvelle version du code source de Corecrypto sur GitHub et détaille, pour la première fois à ce niveau, la méthode utilisée pour vérifier la cryptographie post-quantique. La démarche prolonge PQ3 dans iMessage, mais elle déplace le sujet vers un terrain plus technique : prouver que les systèmes en place tiennent vraiment la route avant leur disponibilité à grande échelle.

Apple Logo Cadenas Securite

Corecrypto est la bibliothèque bas niveau qui alimente plusieurs éléments de sécurité d’Apple, du chiffrement au hachage, en passant par la génération aléatoire et les signatures numériques. En ouvrant aussi ses implémentations de ML-KEM et ML-DSA (les deux algorithmes post-quantiques choisis par le fabricant pour Corecrypto), Apple expose désormais une partie du socle utilisé sur iPhone, Mac et d’autres appareils.

Le dépôt réunit notamment :

  • les implémentations d’Apple pour ML-KEM et ML-DSA
  • des tests
  • des outils de performance
  • des cibles de compilation
  • un dossier consacré à la vérification formelle.

Le mouvement s’inscrit dans la continuité de PQ3, lancé publiquement en 2024 avec iOS 17.4 pour iMessage. Cette première étape avait apporté une protection post-quantique au début des conversations et lors du renouvellement des clés. Cette fois, Apple met surtout en avant la manière dont il vérifie les algorithmes appelés à soutenir cette transition.

Apple mise sur une méthode de vérification conçue pour ses propres contraintes

Apple explique ne pas s’être contenté des outils existants. Corecrypto doit fonctionner sur une large gamme de produits et de puces Apple Silicon, tout en combinant du code C portable et de l’assembleur ARM64 optimisé à la main. Dans ce contexte, les méthodes de vérification disponibles ne couvraient pas à elles seules l’ensemble des besoins de l’entreprise.

Corecrypto Formal Verifcation Process

Le groupe dit donc avoir bâti une approche plus large, qui mêle des tests classiques, de la simulation, une revue indépendante et de la vérification formelle. L’objectif est de vérifier que ses implémentations collent bien à FIPS 203 et FIPS 204, les standards du NIST retenus pour ML-KEM et ML-DSA, deux éléments choisis pour répondre aux menaces associées aux futurs ordinateurs quantiques.

Apple résume l’esprit de cette publication en indiquant : « Avec la dernière publication du code source de Corecrypto, nous partageons des avancées significatives en vérification formelle appliquée avec la communauté cryptographique mondiale ». La société dit vouloir favoriser l’adoption, la relecture critique de ses travaux et l’amélioration générale des méthodes de validation pour les logiciels sensibles.

Des défauts détectés avant l’arrivée sur iPhone et Mac

Apple insiste aussi sur l’intérêt concret de cette vérification renforcée. La firme de Cupertino affirme avoir repéré une étape manquante dans une ancienne implémentation de ML-DSA, un défaut qui pouvait, dans de rares cas, faire sortir certains éléments de la plage attendue et produire un résultat incorrect.

Le point le plus important est ailleurs : Apple estime que les tests conventionnels n’auraient pas forcément vu ce problème avant l’intégration dans ses produits. Dans le pire scénario décrit, ce défaut aurait pu corrompre silencieusement des calculs cryptographiques sans alerte des suites de test existantes. Le fabricant d’iPhone dit aussi avoir trouvé une erreur dans une preuve tierce et l’avoir corrigée indépendamment pour les paramètres utilisés dans sa propre implémentation.

Pour appuyer cette ouverture, Apple ajoute plusieurs matériaux destinés aux chercheurs en sécurité. Le groupe renvoie vers son document sur la vérification formelle de Corecrypto, vers son outil de traduction Cryptol-to-Isabelle et vers les théories Isabelle intégrées à l’archive. L’idée est de rendre disponibles les éléments de preuve nécessaires pour que des spécialistes puissent reproduire, examiner et évaluer le travail réalisé.