mlkem-native

mlkem-native es una implementación segura, rápida y portable en C90¹ de ML-KEM². Es un fork de la implementación de referencia de ML-KEM³.

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⁴. 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⁵.

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⁶ o 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⁸: 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⁹ y los vectores de prueba ML-KEM de Wycheproof¹⁰.

ACVP

Puede ejecutar las pruebas ACVP usando el script tests o el cliente ACVP directamente:

# 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

Puede ejecutar las pruebas Wycheproof¹⁰ usando el script tests o el cliente Wycheproof directamente:

# Using the tests script
./scripts/tests wycheproof

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

Benchmarking

Puede medir el rendimiento, el uso de memoria y el tamaño del binario usando el 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

Para resultados de benchmark de CI y datos históricos de rendimiento, consulte la página de benchmarking.

Uso

Si desea usar mlkem-native, importe mlkem en el árbol de fuentes de su proyecto y compile usando su sistema de compilación favorito. Consulte mlkem para más información, y examples/basic para un ejemplo sencillo. El sistema de compilación proporcionado en este repositorio es solo para fines de desarrollo.

Consulte API-CONVENTIONS.md para las convenciones que se aplican a todas las funciones públicas, como valores de retorno, validez de punteros y el estado de los buffers de salida en caso de error.

¿Puedo traer mi propio FIPS-202?

mlkem-native depende de una implementación de FIPS-202¹¹ e incluye una. Si su biblioteca tiene su propia implementación de FIPS-202, puede usarla en lugar de la que se incluye con mlkem-native. Consulte FIPS202.md, y examples/bring_your_own_fips202 para un ejemplo que usa tiny_sha3¹².

¿Necesito usar los backends de ensamblador?

No. Si desea una compilación solo en C, simplemente omita los directorios mlkem/src/native y/o mlkem/src/fips202/native de su importación y desactive MLK_CONFIG_USE_NATIVE_BACKEND_ARITH y/o MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 en su mlkem_native_config.h.

¿Necesito configurar CBMC para usar mlkem-native?

No. Si bien recomendamos que considere usarlo, mlkem-native se compilará y ejecutará correctamente sin CBMC -- solo asegúrese de incluir cbmc.h y tener CBMC sin definir. En particular, no necesita eliminar todos los contratos de funciones e invariantes de bucle del código; se ignorarán a menos que CBMC esté definido.

¿Soporta mlkem-native todos los niveles de seguridad de ML-KEM?

Sí. El nivel de seguridad es un parámetro de tiempo de compilación configurado estableciendo MLK_CONFIG_PARAMETER_SET=512/768/1024 en mlkem_native_config.h. Si su biblioteca/aplicación requiere múltiples niveles de seguridad, puede compilar y enlazar tres instancias de mlkem-native mientras comparte código común; esto se denomina 'compilación multinivel' y se demuestra en examples/multilevel_build. Consulte también mlkem.

¿Puedo traer mi propio backend?

Sí, puede añadir más backends para la aritmética nativa de ML-KEM y/o para FIPS-202. Siga los backends existentes como plantillas o consulte examples/custom_backend para un ejemplo mínimo de cómo registrar un backend personalizado.

¿Tiene una Pregunta?

Si cree que ha encontrado un fallo de seguridad en mlkem-native, por favor reporte la vulnerabilidad a través del reporte privado de vulnerabilidades de Github. Por favor, no cree un issue público de GitHub.

Si tiene cualquier otra pregunta / problema no relacionado con seguridad / solicitud de funcionalidad, por favor abra un issue de GitHub.

Contribuciones

Si desea ayudarnos a construir mlkem-native, póngase en contacto. Puede contactar al equipo de mlkem-native a través del Discord de PQCA. Consulte también CONTRIBUTING.md.