mlkem-native

mlkem-native è un'implementazione sicura, veloce e portabile in C90[^C90] di ML-KEM[^FIPS203]. È un fork dell'implementazione di riferimento di ML-KEM[^REF].

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[^CBMC]. Tutto l'assembly AArch64 e x86_64 è dimostrato funzionalmente corretto, memory-safe e con temporizzazione indipendente dai segreti (constant-time), usando HOL-Light[^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[^KyberSlash] o clangover[^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[^SLOTHY_Paper]: 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[^ACVP] e i vettori di test ML-KEM Wycheproof[^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