mlkem-native

mlkem-native es una implementación segura, rápida y portable en C90[^C90] de ML-KEM[^FIPS203]. Es un fork de la implementación de referencia de ML-KEM[^REF].

Todo el código C en mlkem/src/* y mlkem/src/fips202/* está demostrado como seguro en memoria (sin desbordamientos de memoria) y seguro en tipos (sin desbordamientos de enteros) usando CBMC[^CBMC]. Todo el ensamblador AArch64 y x86_64 está demostrado como funcionalmente correcto, seguro en memoria y de temporización independiente del secreto (tiempo constante), usando HOL-Light[^HOL-Light].

mlkem-native incluye backends nativos para Arm (64 bits, Neon), Intel/AMD (64 bits, AVX2), RISC-V (64 bits, RVV) y POWER (ppc64le, VSX). Consulte benchmarks para datos de rendimiento.

mlkem-native cuenta con el apoyo de la Post-Quantum Cryptography Alliance como parte de la Linux Foundation.

Inicio rápido para 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

Consulte BUILDING.md para más información.

Aplicaciones

mlkem-native se utiliza en

• libOQS del proyecto Open Quantum Safe desde 0.13.0 (como la implementación ML-KEM por defecto)
• La biblioteca de criptografía de AWS AWS-LC desde v1.50.0
• La biblioteca TLS rustls escrita en Rust desde 0.23.28 (a través de AWS-LC como proveedor de criptografía por defecto)
• Pavona - una biblioteca de bloques de silicio abiertos modulares, probados en tapeout y seguros por diseño

Verificación Formal

Todo el código C en mlkem/src/* y mlkem/src/fips202/* está demostrado como seguro en memoria (sin desbordamientos de memoria) y seguro en tipos (sin desbordamientos de enteros). Esto utiliza el C Bounded Model Checker (CBMC) y se basa en contratos de funciones y anotaciones de invariantes de bucle en el código fuente. Consulte proofs/cbmc para más detalles.

Todo el ensamblador AArch64 y x86_64 está demostrado como funcionalmente correcto, seguro en memoria y con temporización independiente del secreto (tiempo constante), a nivel de código objeto. Esto utiliza el demostrador de teoremas interactivo HOL-Light y la infraestructura de verificación s2n-bignum (que incluye modelos de las partes relevantes de las arquitecturas Arm y x86). Consulte proofs/hol_light para más detalles.

NOTA: La verificación formal nunca es absoluta. Consulte SOUNDNESS.md para un análisis detallado del alcance, las suposiciones y los riesgos de los esfuerzos de verificación formal en torno a mlkem-native.

Seguridad

Todo el ensamblador AArch64 y x86_64 en mlkem-native está formalmente demostrado en HOL Light como libre de flujo de control dependiente del secreto, patrones de acceso a memoria e instrucciones de latencia variable, frustrando la mayoría de los canales laterales de temporización (consulte proofs/hol_light para más detalles). El código C está endurecido contra canales laterales de temporización introducidos por el compilador (como KyberSlash[^KyberSlash] o clangover[^clangover]) mediante barreras adecuadas y patrones de tiempo constante.

La ausencia de ramas dependientes del secreto, patrones de acceso a memoria e instrucciones de latencia variable también se prueba usando valgrind con varias combinaciones de compiladores y opciones de compilación.

Otros ataques. mlkem-native solo tiene como objetivo la resistencia contra canales laterales de temporización. Otras clases de ataques, como canales laterales de potencia y electromagnéticos, canales laterales microarquitectónicos (por ejemplo, ejecución especulativa) o ataques de inyección de fallos, están actualmente fuera de alcance.

Diseño

mlkem-native se divide en un frontend y dos backends para aritmética y FIPS202 / SHA3. El frontend es fijo, está escrito en C y cubre todas las rutinas que no son críticas para el rendimiento. Los backends son flexibles, se encargan de las rutinas sensibles al rendimiento y pueden implementarse en C o código nativo (ensamblador/intrínsecos); consulte mlkem/src/native/api.h para el backend aritmético y mlkem/src/fips202/native/api.h para el backend FIPS-202.

mlkem-native ofrece actualmente los siguientes backends:

• Backend C portable por defecto
• Backend Arm de 64 bits (usando Neon)
• Backend Intel/AMD de 64 bits (usando AVX2)
• Backend RISC-V de 64 bits (usando RVV)
• Backend POWER de 64 bits (ppc64le, usando VSX; soporta POWER8 y superiores)
• Backend Armv8.1-M de 32 bits (usando Helium/MVE) -- consulte #1501. Esto sigue siendo experimental y está deshabilitado por defecto.

Si desea contribuir con nuevos backends, póngase en contacto o simplemente abra un PR.

Nuestro ensamblador AArch64 se desarrolla usando el superoptimizador SLOTHY, siguiendo el enfoque descrito en el artículo de SLOTHY[^SLOTHY_Paper]: Escribimos ensamblador 'limpio' a mano y automatizamos micro-optimizaciones (por ejemplo, consulte el NTT AArch64 limpio vs optimizado). Consulte dev/README.md para más detalles.

Vectores de Prueba

mlkem-native se prueba contra todos los vectores de prueba oficiales ACVP ML-KEM[^ACVP] y los vectores de prueba ML-KEM de Wycheproof[^wycheproof].

ACVP