mlkem-native

mlkem-native est une implémentation sécurisée, rapide et portable en C90[^C90] de ML-KEM[^FIPS203]. Il s'agit d'un fork de l'implémentation de référence de ML-KEM[^REF].

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[^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[^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[^KyberSlash] ou clangover[^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[^SLOTHY_Paper] : 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[^ACVP] et les vecteurs de test ML-KEM Wycheproof[^wycheproof].

ACVP