Apple prouve mathématiquement son chiffrement, un précédent silencieux

Derrière l’annonce d’un chiffrement post-quantique open source, une mutation méthodologique qui va bien au-delà de la cryptographie

Une publication passée pour une simple mise en conformité

Fin mai 2026, Apple a publié sur GitHub le code source de ses implémentations post-quantiques ML-KEM et ML-DSA, intégrées à corecrypto, la bibliothèque cryptographique qui alimente le chiffrement, le hachage et les signatures numériques sur l’ensemble de ses systèmes d’exploitation.

La presse a largement résumé l’information sous l’angle attendu, celui d’Apple qui rend public son chiffrement résistant aux ordinateurs quantiques, dans la continuité de ce qui avait déjà été annoncé pour iMessage en 2024. Un point est pourtant passé presque inaperçu. Apple n’a pas seulement publié du code, elle a publié plus de cinquante mille étapes de preuve mathématique démontrant que ce code correspond exactement aux spécifications NIST FIPS 203 et FIPS 204.

Ce que la couverture médiatique a laissé de côté

Le sujet réel n’est pas l’algorithme post-quantique lui-même, déjà connu depuis deux ans. C’est la méthode qu’Apple a choisie pour garantir sa fiabilité.

Jusqu’ici, la vérification formelle chez Apple restait cantonnée au silicium, avec quinze années d’usage sur les circuits et, depuis 2019, sur l’accélérateur matériel de clés publiques. En l’étendant pour la première fois à une bibliothèque logicielle partagée par des milliards d’appareils, Apple ne se contente pas de sécuriser un algorithme. Elle pose un nouveau seuil d’exigence pour tout code jugé suffisamment critique, un seuil que d’autres composants du système vont, tôt ou tard, devoir atteindre à leur tour.

La mécanique derrière la preuve

corecrypto n’est pas une bibliothèque parmi d’autres. Elle assure le chiffrement, le déchiffrement, le hachage, la génération de nombres aléatoires et les signatures numériques sur la totalité du parc actif d’Apple, soit environ 2,5 milliards d’appareils. Un bogue à cet endroit précis du système compromettrait potentiellement chaque application et chaque fonctionnalité qui en dépend.

Pour ML-KEM et ML-DSA, les deux algorithmes retenus par le NIST sous les références FIPS 203 et FIPS 204, Apple a construit une chaîne de preuve en plusieurs étapes.

L’implémentation initiale est écrite en C portable, puis traduite manuellement dans le langage Cryptol. L’outil SAW, Software Analysis Workbench développé par la société Galois, vérifie ensuite que ce modèle Cryptol correspond fidèlement au code C. Cryptol seul ne suffit toutefois pas à raisonner sur les mathématiques avancées des spécifications FIPS.

Apple fait donc appel à Isabelle, un assistant de preuve capable de manipuler ce niveau d’abstraction, déjà utilisé en interne pour la vérification du silicium depuis 2019. Un traducteur dédié, conçu par Apple et développé par Galois, convertit automatiquement le modèle Cryptol vers Isabelle, limitant le risque d’erreur humaine lors du passage d’un langage à l’autre. La spécification FIPS, elle, est traduite manuellement et avec le plus grand soin dans ce même environnement.

Une fois les deux représentations réunies dans Isabelle, Apple peut démontrer leur équivalence exacte, sous-routine par sous-routine puis pour l’ensemble de l’algorithme. Reste ensuite le code assembleur ARM64, optimisé à la main pour tirer parti de fonctions matérielles comme Data Independent Timing et Pointer Authentication, qui protègent respectivement contre les attaques par canal auxiliaire liées au temps d’exécution et contre la corruption de mémoire. Plutôt que de prouver cet assembleur directement contre la spécification mathématique, ce qui aurait été extrêmement complexe, Apple le compare à la version C déjà validée, une étape nettement plus abordable.

Cette rigueur a payé de façon concrète. La vérification formelle a détecté, dans une première version de l’implémentation ML-DSA, une étape manquante qui aurait pu, dans de rares cas, laisser une valeur dépasser la plage attendue et corrompre silencieusement un calcul cryptographique, sans qu’aucun test conventionnel ne le remarque. C’est précisément le type d’anomalie que les tests classiques, aussi poussés soient-ils, ont statistiquement le plus de mal à révéler.

Ce que cela change dans les six prochains mois

Pour les équipes de sécurité et les développeurs professionnels, cette publication doit être lue comme un indicateur avancé plutôt que comme un aboutissement.

En pratique, les API quantum-safe déjà présentes dans Apple CryptoKit depuis l’automne dernier gagnent en crédibilité opérationnelle. Un chef de projet technique peut désormais justifier l’adoption anticipée du chiffrement post-quantique sur iMessage, VPN et TLS auprès d’une direction sécurité en s’appuyant sur des preuves publiques et vérifiables plutôt que sur la seule parole d’Apple.

À l’inverse, le rythme d’introduction de nouveaux algorithmes cryptographiques chez Apple risque de ralentir plutôt que d’accélérer. Construire une preuve formelle de cette ampleur demande un investissement considérable en temps et en expertise spécialisée, ce qui devrait pousser Apple à réserver cette méthode aux composants les plus critiques plutôt qu’à généraliser son usage rapidement.

Le signal le plus intéressant à surveiller d’ici la fin de l’année concerne les autres briques fondatrices du système. Si la logique observée sur corecrypto se confirme, il est raisonnable d’anticiper que le micrologiciel du Secure Enclave, la chaîne de démarrage sécurisé ou certaines primitives du noyau XNU deviennent les prochaines candidates à ce même traitement. Pour une équipe IT gérant un parc Apple en entreprise, cela signifie qu’un futur commit sur le dépôt public corecrypto, ou l’apparition d’un nouveau document de preuve formelle dans un domaine adjacent, vaudra probablement plus d’attention qu’une annonce marketing classique.

Enfin, cette démarche crée une forme de pression concurrentielle. En démontrant qu’il est possible de vérifier mathématiquement du code cryptographique critique en production à grande échelle, Apple relève implicitement la barre pour l’ensemble du secteur, Microsoft, Google et les grands fournisseurs de cloud compris, qui devront à leur tour justifier pourquoi leurs propres implémentations post-quantiques ne bénéficient pas du même niveau d’assurance.

Source principale : A blueprint for formal verification of Apple corecrypto — Apple Security Research

Titre de la page	URL officielle	Auteur	Date de publication
A blueprint for formal verification of Apple corecrypto	security.apple.com	Apple Security Engineering and Architecture (SEAR) et Hardware Technologies Formal Verification	22 mai 2026
Formal verification for Apple corecrypto (document technique)	github.com/apple/corecrypto	Apple Inc.	Mai 2026
How Apple turned to math to defend against next-gen attacks on encryption	appleinsider.com	AppleInsider	26 mai 2026

Vous avez une question, une idée ou une remarque ? Je serai ravi de vous lire ! ✉️ henrido@hdrapin.com