mlkem-native

mlkem-native est une implémentation sécurisée, rapide et portable en C90¹ de ML-KEM². Il s'agit d'un fork de l'implémentation de référence de ML-KEM³.

Tout le code C dans mlkem/src/* et mlkem/src/fips202/* est prouvé sûr en mémoire (aucun débordement mémoire) et sûr en types (aucun débordement d'entier) à l'aide de CBMC⁴. Tout l'assembleur AArch64 et x86_64 est prouvé fonctionnellement correct, sûr en mémoire, et à temporisation indépendante des secrets (temps constant), à l'aide de HOL-Light⁵.

mlkem-native inclut des backends natifs pour Arm (64 bits, Neon), Intel/AMD (64 bits, AVX2), RISC-V (64 bits, RVV) et POWER (ppc64le, VSX). Voir benchmarks pour les données de performance.

mlkem-native est soutenu par la Post-Quantum Cryptography Alliance dans le cadre de la Linux Foundation.

Démarrage rapide pour Ubuntu

# Install base packages
sudo apt-get update
sudo apt-get install make gcc python3 git

# Clone mlkem-native
git clone https://github.com/pq-code-package/mlkem-native.git
cd mlkem-native

# Build and run tests
make build
make test

# The same using `tests`, a convenience wrapper around `make`
./scripts/tests all
# Show all options
./scripts/tests --help

Voir BUILDING.md pour plus d'informations.

Applications

mlkem-native est utilisé dans

• libOQS du projet Open Quantum Safe depuis 0.13.0 (comme implémentation ML-KEM par défaut)
• La bibliothèque de cryptographie d'AWS AWS-LC depuis v1.50.0
• La bibliothèque TLS rustls écrite en Rust depuis 0.23.28 (via AWS-LC comme fournisseur de cryptographie par défaut)
• Pavona - une bibliothèque de blocs de silicium ouverts modulaires, éprouvés en tapeout et sécurisés par défaut

Vérification formelle

Tout le code C dans mlkem/src/* et mlkem/src/fips202/* est prouvé sûr en mémoire (aucun débordement mémoire) et sûr en types (aucun débordement d'entier). Cela utilise le C Bounded Model Checker (CBMC) et s'appuie sur les contrats de fonctions et les annotations d'invariants de boucle dans le code source. Voir proofs/cbmc pour les détails.

Tout l'assembleur AArch64 et x86_64 est prouvé fonctionnellement correct, sûr en mémoire, et à temporisation indépendante des secrets (temps constant), au niveau du code objet. Cela utilise le prouveur de théorèmes interactif HOL-Light et l'infrastructure de vérification s2n-bignum (qui inclut des modèles des parties pertinentes des architectures Arm et x86). Voir proofs/hol_light pour les détails.

REMARQUE : La vérification formelle n'est jamais absolue. Voir SOUNDNESS.md pour une analyse détaillée de la portée, des hypothèses et des risques des efforts de vérification formelle autour de mlkem-native.

Sécurité

Tout l'assembleur AArch64 et x86_64 dans mlkem-native est formellement prouvé dans HOL Light comme étant exempt de flux de contrôle dépendant des secrets, de schémas d'accès mémoire et d'instructions à latence variable, contrecarrant la plupart des canaux auxiliaires temporels (voir proofs/hol_light pour les détails). Le code C est durci contre les canaux auxiliaires temporels introduits par le compilateur (tels que KyberSlash⁶ ou clangover⁷) grâce à des barrières appropriées et des schémas à temps constant.

L'absence de branches dépendantes des secrets, de schémas d'accès mémoire et d'instructions à latence variable est également testée à l'aide de valgrind avec diverses combinaisons de compilateurs et d'options de compilation.

Autres attaques. mlkem-native vise uniquement la résistance contre les canaux auxiliaires temporels. D'autres classes d'attaques, telles que les canaux auxiliaires de puissance et électromagnétiques, les canaux auxiliaires microarchitecturaux (par exemple l'exécution spéculative), ou les attaques par injection de fautes, sont actuellement hors de portée.

Conception

mlkem-native est divisé en un frontend et deux backends pour l'arithmétique et FIPS202 / SHA3. Le frontend est fixe, écrit en C, et couvre toutes les routines qui ne sont pas critiques pour la performance. Les backends sont flexibles, prennent en charge les routines sensibles à la performance, et peuvent être implémentés en C ou en code natif (assembleur/intrinsèques) ; voir mlkem/src/native/api.h pour le backend arithmétique et mlkem/src/fips202/native/api.h pour le backend FIPS-202.

mlkem-native propose actuellement les backends suivants :

• Backend C portable par défaut
• Backend Arm 64 bits (utilisant Neon)
• Backend Intel/AMD 64 bits (utilisant AVX2)
• Backend RISC-V 64 bits (utilisant RVV)
• Backend POWER 64 bits (ppc64le, utilisant VSX ; prend en charge POWER8 et supérieur)
• Backend Armv8.1-M 32 bits (utilisant Helium/MVE) -- voir #1501. Ce backend est encore expérimental et désactivé par défaut.

Si vous souhaitez contribuer de nouveaux backends, n'hésitez pas à nous contacter ou à ouvrir une PR.

Notre assembleur AArch64 est développé à l'aide du superoptimiseur SLOTHY, suivant l'approche décrite dans l'article SLOTHY⁸ : Nous écrivons un assembleur « propre » à la main et automatisons les micro-optimisations (par exemple, voir le NTT AArch64 clean vs optimisé). Voir dev/README.md pour plus de détails.

Vecteurs de test

mlkem-native est testé contre tous les vecteurs de test officiels ACVP ML-KEM⁹ et les vecteurs de test ML-KEM Wycheproof¹⁰.

ACVP

Vous pouvez exécuter les tests ACVP à l'aide du script tests ou du client ACVP directement :

# Using the tests script
./scripts/tests acvp
# Using a specific ACVP release
./scripts/tests acvp --version v1.1.0.41

# Using the ACVP client directly
python3 ./test/acvp/acvp_client.py
python3 ./test/acvp/acvp_client.py --version v1.1.0.41

# Using specific ACVP test vector files (downloaded from the ACVP-Server)
# python3 ./test/acvp/acvp_client.py -p {PROMPT}.json -e {EXPECTED_RESULT}.json
# For example, assuming you have run the above
python3 ./test/acvp/acvp_client.py \
  -p ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/prompt.json \
  -e ./test/acvp/.acvp-data/v1.1.0.41/files/ML-KEM-keyGen-FIPS203/expectedResults.json

Wycheproof

Vous pouvez exécuter les tests Wycheproof¹⁰ à l'aide du script tests ou du client Wycheproof directement :

# Using the tests script
./scripts/tests wycheproof

# Using the Wycheproof client directly
python3 ./test/wycheproof/wycheproof_client.py

Analyse comparative

Vous pouvez mesurer la performance, l'utilisation de la mémoire et la taille du binaire à l'aide du script tests :

# Speed benchmarks (-c selects cycle counter: NO, PMU, PERF, or MAC)
# Note: PERF/MAC may require the -r flag to run benchmarking binaries using sudo
./scripts/tests bench -c PMU
./scripts/tests bench -c PERF -r

# Stack usage analysis
./scripts/tests stack

# Binary size measurement
./scripts/tests size

Pour les résultats d'analyse comparative CI et les données de performance historiques, voir la page d'analyse comparative.

Utilisation

Si vous souhaitez utiliser mlkem-native, importez mlkem dans l'arborescence source de votre projet et compilez avec votre système de compilation préféré. Voir mlkem pour plus d'informations, et examples/basic pour un exemple simple. Le système de compilation fourni dans ce dépôt est uniquement destiné au développement.

Voir API-CONVENTIONS.md pour les conventions qui s'appliquent à toutes les fonctions publiques, telles que les valeurs de retour, la validité des pointeurs et l'état des tampons de sortie en cas d'erreur.

Puis-je apporter mon propre FIPS-202 ?

mlkem-native s'appuie sur une implémentation de FIPS-202¹¹ et en fournit une. Si votre bibliothèque possède sa propre implémentation FIPS-202, vous pouvez l'utiliser à la place de celle fournie avec mlkem-native. Voir FIPS202.md, et examples/bring_your_own_fips202 pour un exemple utilisant tiny_sha3¹².

Dois-je utiliser les backends assembleur ?

Non. Si vous souhaitez une compilation uniquement en C, omettez simplement les répertoires mlkem/src/native et/ou mlkem/src/fips202/native de votre import et désactivez MLK_CONFIG_USE_NATIVE_BACKEND_ARITH et/ou MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 dans votre mlkem_native_config.h.

Dois-je configurer CBMC pour utiliser mlkem-native ?

Non. Bien que nous recommandions d'envisager de l'utiliser, mlkem-native se compile et fonctionne parfaitement sans CBMC — assurez-vous simplement d' inclure cbmc.h et d'avoir CBMC non défini. En particulier, vous n'avez pas besoin de supprimer tous les contrats de fonctions et invariants de boucle du code ; ils seront ignorés sauf si CBMC est défini.

mlkem-native prend-il en charge tous les niveaux de sécurité de ML-KEM ?

Oui. Le niveau de sécurité est un paramètre de compilation configuré en définissant MLK_CONFIG_PARAMETER_SET=512/768/1024 dans mlkem_native_config.h. Si votre bibliothèque/application nécessite plusieurs niveaux de sécurité, vous pouvez compiler + lier trois instances de mlkem-native tout en partageant le code commun ; cela s'appelle une « compilation multi-niveaux » et est démontré dans examples/multilevel_build. Voir aussi mlkem.

Puis-je apporter mon propre backend ?

Oui, vous pouvez ajouter d'autres backends pour l'arithmétique native ML-KEM et/ou pour FIPS-202. Suivez les backends existants comme modèles ou voir examples/custom_backend pour un exemple minimal de la façon d'enregistrer un backend personnalisé.

Une question ?

Si vous pensez avoir trouvé un bug de sécurité dans mlkem-native, veuillez signaler la vulnérabilité via le signalement privé de vulnérabilités de Github. Veuillez ne pas créer de problème GitHub public.

Si vous avez toute autre question / problème non lié à la sécurité / demande de fonctionnalité, veuillez ouvrir un problème GitHub.

Contribuer

Si vous souhaitez nous aider à construire mlkem-native, n'hésitez pas à nous contacter. Vous pouvez contacter l'équipe mlkem-native via le Discord PQCA. Voir aussi CONTRIBUTING.md.