pq-code-package/mlkem-nativeSichere, schnelle und portable C90-Implementierung von ML-KEM / FIPS 203
mlkem-native ist eine sichere, schnelle und portable C90[^C90]-Implementierung von ML-KEM[^FIPS203]. Es ist ein Fork der ML-KEM-Referenzimplementierung[^REF].
Der gesamte C-Code in mlkem/src/* und mlkem/src/fips202/* ist als speichersicher (kein Speicherüberlauf) und typsicher (kein Integer-Überlauf) bewiesen, unter Verwendung von CBMC[^CBMC]. Der gesamte AArch64- und x86_64-Assemblycode ist als funktional korrekt, speichersicher und mit geheimnisunabhängigem Timing (konstantzeitlich) bewiesen, unter Verwendung von HOL-Light[^HOL-Light].
mlkem-native enthält native Backends für Arm (64-Bit, Neon), Intel/AMD (64-Bit, AVX2), RISC-V (64-Bit, RVV) und POWER (ppc64le, VSX). Siehe Benchmarks für Leistungsdaten.
mlkem-native wird von der Post-Quantum Cryptography Alliance als Teil der Linux Foundation unterstützt.
# Basis-Pakete installieren
sudo apt-get update
sudo apt-get install make gcc python3 git
# mlkem-native klonen
git clone https://github.com/pq-code-package/mlkem-native.git
cd mlkem-native
# Build und Tests ausführen
make build
make test
# Dasselbe mit `tests`, einem Komfort-Wrapper um `make`
./scripts/tests all
# Alle Optionen anzeigen
./scripts/tests --help
Weitere Informationen finden Sie in BUILDING.md.
mlkem-native wird verwendet in
Der gesamte C-Code in mlkem/src/* und mlkem/src/fips202/* ist als speichersicher (kein Speicherüberlauf) und typsicher (kein Integer-Überlauf) bewiesen. Dies verwendet den C Bounded Model Checker (CBMC) und baut auf Funktionsverträgen und Schleifeninvarianten-Annotationen im Quellcode auf. Siehe proofs/cbmc für Details.
Der gesamte AArch64- und x86_64-Assemblycode ist als funktional korrekt, speichersicher und mit geheimnisunabhängigem Timing (konstantzeitlich) auf Objektcode-Ebene bewiesen. Dies verwendet den interaktiven Theorembeweiser HOL-Light und die Verifikationsinfrastruktur s2n-bignum (die Modelle der relevanten Teile der Arm- und x86-Architekturen enthält). Siehe proofs/hol_light für Details.
HINWEIS: Formale Verifikation ist niemals absolut. Siehe SOUNDNESS.md für eine detaillierte Analyse des Umfangs, der Annahmen und der Risiken der formalen Verifikationsbemühungen rund um mlkem-native.
Der gesamte AArch64- und x86_64-Assemblycode in mlkem-native ist in HOL Light formal als frei von geheimnisabhängigem Kontrollfluss, Speicherzugriffsmustern und Anweisungen mit variabler Latenz bewiesen, wodurch die meisten Timing-Seitenkanäle vereitelt werden (siehe proofs/hol_light für Details). C-Code ist gegen compilerinduzierte Timing-Seitenkanäle (wie KyberSlash[^KyberSlash] oder clangover[^clangover]) durch geeignete Barrieren und Konstantzeit-Muster gehärtet.
Die Abwesenheit von geheimnisabhängigen Verzweigungen, Speicherzugriffsmustern und Anweisungen mit variabler Latenz wird auch mit valgrind
mit verschiedenen Kombinationen von Compilern und Kompilierungsoptionen getestet.
Andere Angriffe. mlkem-native zielt nur auf Widerstand gegen Timing-Seitenkanäle ab. Andere Angriffsklassen wie Strom- und elektromagnetische Seitenkanäle, mikroarchitektonische Seitenkanäle (z. B. spekulative Ausführung) oder Fehlerinjektionsangriffe sind derzeit außerhalb des Rahmens.
mlkem-native ist in ein Frontend und zwei Backends für Arithmetik und FIPS202 / SHA3 aufgeteilt. Das Frontend ist fest, in C geschrieben und deckt alle Routinen ab, die nicht leistungskritisch sind. Die Backends sind flexibel, kümmern sich um leistungssensitive Routinen und können in C oder nativem Code (Assembly/Intrinsics) implementiert werden; siehe mlkem/src/native/api.h für das Arithmetik-Backend und mlkem/src/fips202/native/api.h für das FIPS-202-Backend.
mlkem-native bietet derzeit die folgenden Backends an:
Wenn Sie neue Backends beitragen möchten, kontaktieren Sie uns bitte oder eröffnen Sie einfach einen PR.
Unser AArch64-Assemblycode wird mit dem SLOTHY-Superoptimierer entwickelt, dem Ansatz aus dem SLOTHY-Papier[^SLOTHY_Paper] folgend: Wir schreiben 'sauberen' Assemblycode von Hand und automatisieren Mikrooptimierungen (z. B. siehe clean vs. optimized AArch64-NTT). Siehe dev/README.md für weitere Details.
mlkem-native wird gegen alle offiziellen ACVP-ML-KEM-Testvektoren[^ACVP] und die Wycheproof[^wycheproof]-ML-KEM-Testvektoren getestet.
Sie können ACVP-Tests mit dem tests-Skript oder dem ACVP-Client direkt ausführen:
# Mit dem tests-Skript
./scripts/tests acvp
# Mit einer bestimmten ACVP-Version
./scripts/tests acvp --version v1.1.0.41