Apple publie ses implémentations post-quantiques et leurs preuves formelles, exposant au regard extérieur une infrastructure cryptographique déployée sur plus de 2,5 milliards d’appareils actifs.
Apple rend publics le code de ML-KEM et ML-DSA, deux algorithmes conçus pour résister aux futures attaques quantiques, ainsi que ses outils de vérification mathématique. Intégrées à CoreCrypto, ces technologies protègent déjà iMessage, des services VPN et des échanges TLS. L’entreprise dévoile aussi son traducteur de Cryptol vers Isabelle, utilisé pour démontrer la conformité du code aux normes officielles. Cette démarche a permis d’identifier une opération absente dans ML-DSA, susceptible de fragiliser l’authenticité des signatures numériques.
Une vérification ouverte du code post-quantique
Apple place une partie stratégique de son infrastructure cryptographique sous le regard des chercheurs indépendants. Le groupe publie les implémentations de ML-KEM et ML-DSA, accompagnées des bibliothèques, outils et documents nécessaires pour reproduire ses travaux de vérification formelle.
Ces deux algorithmes résistants aux attaques quantiques ont été sélectionnés parmi plusieurs solutions standardisées. Selon Apple, ils correspondaient le mieux à ses contraintes de sécurité, de performance et de compacité. Leur rôle consiste à préparer les communications numériques à l’émergence de futurs ordinateurs quantiques capables de menacer certains mécanismes cryptographiques actuellement utilisés.
Les implémentations concernées appartiennent à CoreCrypto, la bibliothèque centrale mobilisée par les systèmes d’exploitation d’Apple. Elle assure notamment le chiffrement, le déchiffrement, le hachage et les signatures numériques. Cette architecture fonctionne sur plus de 2,5 milliards d’appareils actifs, ce qui donne à chaque erreur potentielle une portée considérable.
Le déploiement post-quantique a commencé dans iMessage en 2024. Apple a ensuite étendu cette protection à des services VPN et aux protocoles réseau TLS. La publication du code permet désormais aux spécialistes d’examiner les choix techniques, de reproduire les démonstrations et d’identifier d’éventuelles faiblesses avant qu’elles ne deviennent exploitables.
Parmi les outils diffusés figure un traducteur développé par Apple entre Cryptol et Isabelle. Cryptol est un langage formel conçu par Galois pour décrire des opérations cryptographiques. Isabelle, issu de travaux universitaires menés à Cambridge et Munich, sert d’assistant de preuve mathématique.
Apple a d’abord représenté son code dans Cryptol, puis l’a converti vers Isabelle. Cette chaîne devait démontrer que les implémentations respectaient les spécifications officielles pour toutes les entrées couvertes. L’entreprise avait déjà employé Isabelle afin de vérifier certains composants cryptographiques matériels.
Une erreur critique détectée avant la production
La vérification formelle ne se contente pas d’exécuter une série de scénarios connus. Elle cherche à établir mathématiquement qu’un programme respecte une propriété donnée pour l’ensemble des entrées possibles. Cette différence devient décisive lorsque la complexité du code rend impossible une exploration exhaustive par des tests traditionnels.
Durant ce travail, les chercheurs ont repéré une étape de calcul absente dans l’implémentation de ML-DSA. Cette omission aurait pu rendre les signatures numériques non sécurisées. Si le défaut avait atteint les systèmes en production, certains messages iMessage auraient pu sembler correctement authentifiés sans l’être réellement. Les utilisateurs auraient alors pu ignorer que leurs communications étaient exposées.
Ce cas illustre la limite des campagnes de test classiques. Celles-ci examinent de nombreux comportements, erreurs et situations particulières. Elles ne peuvent toutefois parcourir toutes les combinaisons possibles dans un logiciel cryptographique complexe. Une anomalie discrète peut ainsi rester invisible entre deux cas testés, sans provoquer d’échec détectable.
Apple ne présente pas la preuve formelle comme un remplacement complet des méthodes existantes. Ses équipes reconnaissent que certains aspects du code ne peuvent pas être vérifiés avec les outils disponibles. Elles combinent donc plusieurs techniques : démonstration mathématique pour la correction fondamentale, tests conventionnels pour les propriétés non couvertes et évaluation critique du fonctionnement global.
« D’après nos travaux à ce jour, nous sommes convaincus que la meilleure garantie de sécurité possible repose sur la combinaison de la vérification formelle et des méthodes conventionnelles, ainsi que sur une évaluation critique des résultats de bout en bout », indique l’article publié par l’entreprise.
Apple estime que cette stratégie hybride fournit la protection la plus solide pour des composants cryptographiques critiques. L’ouverture du code et des outils ajoute une dimension essentielle : des chercheurs extérieurs peuvent désormais contrôler les résultats, contester les hypothèses et réutiliser les méthodes dans d’autres projets.
Dans la course au chiffrement post-quantique, la publication des preuves transforme ainsi un choix technique interne en ressource collective pour la cybersécurité et le renseignement défensif.
