Un arnés de verificación diferencial y adversaria de criptografía post-cuántica: compara una implementación contra referencias independientes alimentando los mismos bytes deterministas, y prueba la validación de entrada que exige el estándar. Hoy diferencia el ml-kem de RustCrypto contra tres implementaciones (pq-crystals C, libcrux y AWS-LC) y su ml-dsa contra dilithium.

¿Encontraron un fallo en RustCrypto?

No. Este resultado es de aseguramiento: RustCrypto cumple los checks de conformidad verificados. Es un chequeo de conformidad, no una auditoría completa, y no cubre canales laterales.

¿Sirve para mi implementación post-cuántica?

Sí: el arnés puede diferenciar tu implementación contra referencias independientes y probar su validación de entrada, con controles positivos y parejas rojo/verde.

iraca: verificación diferencial de ML-KEM y ML-DSA contra tres implementaciones independientes

Q: ¿Por qué tres implementaciones y no una?

Porque un solo oráculo puede compartir el punto ciego del código que mide. Tres implementaciones independientes —una en otro lenguaje, otra formalmente verificada, otra de producción— casi nunca comparten el mismo error; que las cuatro coincidan bit a bit es una señal mucho más fuerte.

Qué hicimos

iraca es un arnés que verifica la criptografía post-cuántica que el ecosistema Rust realmente usa, diferenciándola contra implementaciones independientes. El crate ml-kem de RustCrypto (ML-KEM / FIPS 203) —muy usado y sin auditoría independiente publicada— resulta idéntico byte a byte a tres implementaciones que no se conocen entre sí: la referencia en C de pq-crystals, libcrux (de Cryspen, formalmente verificada) y AWS-LC (la de producción, de Amazon). Coinciden en generación de claves, encapsulación y decapsulación, en los tres niveles —ML-KEM-512, 768 y 1024—.

El mismo arnés diferencia ML-DSA (FIPS 204, la firma) en sus tres niveles —44, 65 y 87— contra la referencia dilithium, byte a byte, con verificación cruzada.

Es un chequeo de conformidad, no una auditoría completa, y no cubre canales laterales (la clase KyberSlash).

Por qué importa

Los estándares NIST (FIPS 203/204/205) son definitivos y la migración es obligatoria. Buena parte del mundo Rust usa los crates de RustCrypto, que hoy no tienen auditoría independiente. Y un solo oráculo puede compartir el punto ciego del código que mide. Tres implementaciones independientes —una en otro lenguaje, otra formalmente verificada, otra de producción endurecida— cierran ese hueco: que las cuatro coincidan bit a bit es una señal mucho más fuerte que coincidir con una sola.

El método: los mismos bytes crudos a todos los lados

iraca alimenta los mismos bytes al crate y a cada oráculo por sus entradas deterministas, sin DRBG y sin repetir vectores. Con determinismo de extremo a extremo, toda discrepancia es real, no ruido de aleatoriedad. Las referencias en C (pq-crystals y AWS-LC) se compilan desde el fuente y se enlazan tras un módulo FFI delgado; libcrux entra como dependencia de Rust; el resto es Rust seguro.

Una capa adversaria prueba además la validación de entrada: en ML-KEM genera claves de encapsulación no-canónicas (un coeficiente mayor o igual a q) y comprueba el rechazo que exige FIPS 203 (el modulus check); en ML-DSA prueba la canonicidad del relleno del hint que exige FIPS 204. El oráculo de canonicidad es el estándar mismo, no otra implementación.

Resultados

ML-KEM-512/768/1024 (cuatro vías): claves, textos cifrados y secretos compartidos idénticos byte a byte entre RustCrypto, pq-crystals, libcrux y AWS-LC, en 128 semillas por nivel más un vector fijo.
ML-DSA-44/65/87 (dos vías): acuerdo byte a byte con la referencia dilithium en clave y firma determinista, con verificación cruzada (cada lado acepta la firma del otro) y la capa adversaria de canonicidad del hint.
Conformidad adversaria: RustCrypto rechaza las entradas no-canónicas que exigen los estándares, confirmado por lectura del fuente y por ejecución.

Cada resultado lleva su pareja rojo/verde y su control positivo. Que no haya discrepancia solo vale si el camino de comparación de verdad se ejecutó y sabe distinguir: lo probamos rompiendo un byte en cada implementación y comprobando que el banco se pone rojo.

Qué no es

No es una auditoría completa; no es análisis de canal lateral ni temporal; es una versión y unas propiedades concretas. El aseguramiento es acumulativo, no un sello único.

Reproducible y para colaborar

El arnés es pequeño, determinista y pensado para re-correrse. Si mantienes una implementación post-cuántica y quieres una pasada diferencial y adversaria independiente, o un oráculo contra el cual diferenciar tu trabajo, para eso es. También colaboro con el esfuerzo post-cuántico de la Ethereum Foundation en verificación de esquemas de firma.