mlkem-native

mlkem-native è un'implementazione sicura, veloce e portabile in C90¹ di ML-KEM². È un fork dell'implementazione di riferimento di ML-KEM³.

Tutto il codice C in mlkem/src/* e mlkem/src/fips202/* è dimostrato memory-safe (nessun overflow di memoria) e type-safe (nessun overflow di interi) usando CBMC⁴. Tutto l'assembly AArch64 e x86_64 è dimostrato funzionalmente corretto, memory-safe e con temporizzazione indipendente dai segreti (constant-time), usando HOL-Light⁵.

mlkem-native include backend nativi per Arm (64-bit, Neon), Intel/AMD (64-bit, AVX2), RISC-V (64-bit, RVV) e POWER (ppc64le, VSX). Vedi benchmarks per i dati sulle prestazioni.

mlkem-native è supportato dalla Post-Quantum Cryptography Alliance come parte della Linux Foundation.

Avvio rapido per 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

Vedi BUILDING.md per maggiori informazioni.

Applicazioni

mlkem-native è utilizzato in

• libOQS del progetto Open Quantum Safe dalla 0.13.0 (come implementazione ML-KEM predefinita)
• La libreria crittografica di AWS AWS-LC dalla v1.50.0
• La libreria TLS rustls scritta in Rust dalla 0.23.28 (tramite AWS-LC come provider crittografico predefinito)
• Pavona - una libreria di blocchi siliconici open source modulari, tapeout-proven e sicuri per impostazione predefinita

Verifica formale

Tutto il codice C in mlkem/src/* e mlkem/src/fips202/* è dimostrato memory-safe (nessun overflow di memoria) e type-safe (nessun overflow di interi). Questo utilizza il C Bounded Model Checker (CBMC) e si basa su contratti di funzione e annotazioni di invarianti di ciclo nel codice sorgente. Vedi proofs/cbmc per i dettagli.

Tutto l'assembly AArch64 e x86_64 è dimostrato funzionalmente corretto, memory-safe e con temporizzazione indipendente dai segreti (constant-time), a livello di codice oggetto. Questo utilizza il dimostratore interattivo di teoremi HOL-Light e l'infrastruttura di verifica s2n-bignum (che include modelli delle parti rilevanti delle architetture Arm e x86). Vedi proofs/hol_light per i dettagli.

NOTA: La verifica formale non è mai assoluta. Vedi SOUNDNESS.md per un'analisi dettagliata dell'ambito, delle assunzioni e dei rischi degli sforzi di verifica formale attorno a mlkem-native.

Sicurezza

Tutto l'assembly AArch64 e x86_64 in mlkem-native è formalmente dimostrato in HOL Light essere privo di flusso di controllo dipendente dai segreti, pattern di accesso alla memoria e istruzioni a latenza variabile, ostacolando la maggior parte dei canali laterali temporali (vedi proofs/hol_light per i dettagli). Il codice C è indurito contro i canali laterali temporali introdotti dal compilatore (come KyberSlash⁶ o clangover⁷) tramite barriere adeguate e pattern constant-time.

L'assenza di rami dipendenti dai segreti, pattern di accesso alla memoria e istruzioni a latenza variabile è anche testata usando valgrind con varie combinazioni di compilatori e opzioni di compilazione.

Altri attacchi. mlkem-native mira alla resistenza contro i canali laterali temporali soltanto. Altre classi di attacco, come i canali laterali di potenza ed elettromagnetici, i canali laterali microarchitetturali (ad es. esecuzione speculativa) o gli attacchi di iniezione di guasti, sono attualmente fuori ambito.

Design

mlkem-native è suddiviso in un frontend e due backend per l'aritmetica e FIPS202 / SHA3. Il frontend è fisso, scritto in C, e copre tutte le routine che non sono critiche per le prestazioni. I backend sono flessibili, gestiscono le routine sensibili alle prestazioni e possono essere implementati in C o codice nativo (assembly/intrinsici); vedi mlkem/src/native/api.h per il backend aritmetico e mlkem/src/fips202/native/api.h per il backend FIPS-202.

mlkem-native offre attualmente i seguenti backend:

• Backend C portabile predefinito
• Backend Arm a 64 bit (usando Neon)
• Backend Intel/AMD a 64 bit (usando AVX2)
• Backend RISC-V a 64 bit (usando RVV)
• Backend POWER a 64 bit (ppc64le, usando VSX; supporta POWER8 e successivi)
• Backend Armv8.1-M a 32 bit (usando Helium/MVE) -- vedi #1501. Questo è ancora sperimentale e disabilitato per impostazione predefinita.

Se desideri contribuire con nuovi backend, contattaci o apri semplicemente una PR.

Il nostro assembly AArch64 è sviluppato usando il superottimizzatore SLOTHY, seguendo l'approccio descritto nell'articolo SLOTHY⁸: Scriviamo assembly 'pulito' a mano e automatizziamo le micro-ottimizzazioni (ad es. vedi il NTT AArch64 clean vs ottimizzato). Vedi dev/README.md per maggiori dettagli.

Vettori di test

mlkem-native è testato contro tutti i vettori di test ufficiali ACVP ML-KEM⁹ e i vettori di test ML-KEM Wycheproof¹⁰.

ACVP

Puoi eseguire i test ACVP usando lo script tests o il client ACVP direttamente:

# 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

Puoi eseguire i test Wycheproof¹⁰ usando lo script tests o il client Wycheproof direttamente:

# Using the tests script
./scripts/tests wycheproof

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

Benchmarking

Puoi misurare prestazioni, utilizzo della memoria e dimensione del binario usando lo 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

Per i risultati dei benchmark CI e i dati storici sulle prestazioni, vedi la pagina di benchmarking.

Utilizzo

Se vuoi usare mlkem-native, importa mlkem nell'albero dei sorgenti del tuo progetto e compila usando il tuo sistema di build preferito. Vedi mlkem per maggiori informazioni, e examples/basic per un esempio semplice. Il sistema di build fornito in questo repository è solo per scopi di sviluppo.

Vedi API-CONVENTIONS.md per le convenzioni che si applicano a tutte le funzioni pubbliche, come valori di ritorno, validità dei puntatori e lo stato dei buffer di output in caso di errore.

Posso usare il mio FIPS-202?

mlkem-native si affida a e include un'implementazione di FIPS-202¹¹. Se la tua libreria ha la propria implementazione FIPS-202, puoi usarla al posto di quella inclusa in mlkem-native. Vedi FIPS202.md, e examples/bring_your_own_fips202 per un esempio che usa tiny_sha3¹².

Devo usare i backend assembly?

No. Se vuoi una build solo C, ometti semplicemente le directory mlkem/src/native e/o mlkem/src/fips202/native dal tuo import e disattiva MLK_CONFIG_USE_NATIVE_BACKEND_ARITH e/o MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 nel tuo mlkem_native_config.h.

Devo configurare CBMC per usare mlkem-native?

No. Anche se raccomandiamo di considerarne l'uso, mlkem-native verrà compilato ed eseguito correttamente senza CBMC -- assicurati solo di includere cbmc.h e avere CBMC non definito. In particolare, non devi non rimuovere tutti i contratti di funzione e gli invarianti di ciclo dal codice; verranno ignorati a meno che CBMC non sia impostato.

mlkem-native supporta tutti i livelli di sicurezza di ML-KEM?

Sì. Il livello di sicurezza è un parametro a tempo di compilazione configurato impostando MLK_CONFIG_PARAMETER_SET=512/768/1024 in mlkem_native_config.h. Se la tua libreria/applicazione richiede più livelli di sicurezza, puoi compilare e collegare tre istanze di mlkem-native condividendo codice comune; questo è chiamato 'build multilivello' ed è dimostrato in examples/multilevel_build. Vedi anche mlkem.

Posso portare il mio backend?

Sì, puoi aggiungere ulteriori backend per l'aritmetica nativa ML-KEM e/o per FIPS-202. Segui i backend esistenti come modelli o vedi examples/custom_backend per un esempio minimale su come registrare un backend personalizzato.

Hai una domanda?

Se pensi di aver trovato un bug di sicurezza in mlkem-native, segnala la vulnerabilità tramite la segnalazione privata di vulnerabilità di Github. Per favore non creare un issue pubblico su GitHub.

Se hai qualsiasi altra domanda / problema non legato alla sicurezza / richiesta di funzionalità, apri un issue su GitHub.

Contribuire

Se vuoi aiutarci a costruire mlkem-native, contattaci. Puoi contattare il team di mlkem-native tramite il Discord PQCA. Vedi anche CONTRIBUTING.md.