mlkem-native

mlkem-native ist eine sichere, schnelle und portable C90¹-Implementierung von ML-KEM². Es ist ein Fork der ML-KEM-Referenzimplementierung³.

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⁴. Der gesamte AArch64- und x86_64-Assemblycode ist als funktional korrekt, speichersicher und mit geheimnisunabhängigem Timing (konstantzeitlich) bewiesen, unter Verwendung von 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.

Schnellstart für Ubuntu

# 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.

Anwendungen

mlkem-native wird verwendet in

• libOQS des Open Quantum Safe-Projekts seit 0.13.0 (als Standard-ML-KEM-Implementierung)
• AWS' Kryptographie-Bibliothek AWS-LC seit v1.50.0
• Der in Rust geschriebenen TLS-Bibliothek rustls seit 0.23.28 (über AWS-LC als Standard-Kryptographie-Anbieter)
• Pavona – eine Bibliothek modularer, tapeout-erprobter und standardmäßig sicherer Open-Silicon-Blöcke

Formale Verifikation

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.

Sicherheit

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⁶ oder 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.

Design

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:

• Standard-portables C-Backend
• 64-Bit-Arm-Backend (mit Neon)
• 64-Bit-Intel/AMD-Backend (mit AVX2)
• 64-Bit-RISC-V-Backend (mit RVV)
• 64-Bit-POWER-Backend (ppc64le, mit VSX; unterstützt POWER8 und höher)
• 32-Bit-Armv8.1-M-Backend (mit Helium/MVE) – siehe #1501. Dies ist noch experimentell und standardmäßig deaktiviert.

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⁸ 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.

Testvektoren

mlkem-native wird gegen alle offiziellen ACVP-ML-KEM-Testvektoren⁹ und die Wycheproof¹⁰-ML-KEM-Testvektoren getestet.

ACVP

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

# Mit dem ACVP-Client direkt
python3 ./test/acvp/acvp_client.py
python3 ./test/acvp/acvp_client.py --version v1.1.0.41

# Mit bestimmten ACVP-Testvektordateien (vom ACVP-Server heruntergeladen)
# python3 ./test/acvp/acvp_client.py -p {PROMPT}.json -e {EXPECTED_RESULT}.json
# Zum Beispiel, vorausgesetzt Sie haben das Obige ausgeführt
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

Sie können Wycheproof¹⁰-Tests mit dem tests-Skript oder dem Wycheproof-Client direkt ausführen:

# Mit dem tests-Skript
./scripts/tests wycheproof

# Mit dem Wycheproof-Client direkt
python3 ./test/wycheproof/wycheproof_client.py

Benchmarking

Sie können Leistung, Speichernutzung und Binärgröße mit dem tests-Skript messen:

# Geschwindigkeits-Benchmarks (-c wählt den Zykluszähler: NO, PMU, PERF oder MAC)
# Hinweis: PERF/MAC kann das -r-Flag erfordern, um Benchmark-Binaries mit sudo auszuführen
./scripts/tests bench -c PMU
./scripts/tests bench -c PERF -r

# Stack-Nutzungsanalyse
./scripts/tests stack

# Binärgrößenmessung
./scripts/tests size

Für CI-Benchmarkergebnisse und historische Leistungsdaten siehe die Benchmarking-Seite.

Verwendung

Wenn Sie mlkem-native verwenden möchten, importieren Sie mlkem in den Quellbaum Ihres Projekts und bauen Sie mit Ihrem bevorzugten Build-System. Siehe mlkem für weitere Informationen und examples/basic für ein einfaches Beispiel. Das in diesem Repository bereitgestellte Build-System dient nur Entwicklungszwecken.

Siehe API-CONVENTIONS.md für Konventionen, die für alle öffentlichen Funktionen gelten, wie Rückgabewerte, Zeigergültigkeit und den Zustand von Ausgabepuffern bei Fehlern.

Kann ich mein eigenes FIPS-202 mitbringen?

mlkem-native verlässt sich auf eine Implementierung von FIPS-202¹¹ und wird mit dieser geliefert. Wenn Ihre Bibliothek eine eigene FIPS-202-Implementierung hat, können Sie diese anstelle der mit mlkem-native gelieferten verwenden. Siehe FIPS202.md und examples/bring_your_own_fips202 für ein Beispiel mit tiny_sha3¹².

Muss ich die Assembly-Backends verwenden?

Nein. Wenn Sie einen reinen C-Build möchten, lassen Sie einfach die Verzeichnisse mlkem/src/native und/oder mlkem/src/fips202/native aus Ihrem Import weg und setzen Sie MLK_CONFIG_USE_NATIVE_BACKEND_ARITH und/oder MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 in Ihrer mlkem_native_config.h zurück.

Muss ich CBMC einrichten, um mlkem-native zu verwenden?

Nein. Obwohl wir empfehlen, die Verwendung in Betracht zu ziehen, baut und läuft mlkem-native auch ohne CBMC einwandfrei – stellen Sie nur sicher, dass Sie cbmc.h einbinden und CBMC undefiniert lassen. Insbesondere müssen Sie nicht alle Funktionsverträge und Schleifeninvarianten aus dem Code entfernen; sie werden ignoriert, es sei denn, CBMC ist gesetzt.

Unterstützt mlkem-native alle Sicherheitsstufen von ML-KEM?

Ja. Die Sicherheitsstufe ist ein Kompilierzeitparameter, der durch Setzen von MLK_CONFIG_PARAMETER_SET=512/768/1024 in mlkem_native_config.h konfiguriert wird. Wenn Ihre Bibliothek/Anwendung mehrere Sicherheitsstufen erfordert, können Sie drei Instanzen von mlkem-native bauen und verlinken, während gemeinsamer Code geteilt wird; dies wird als 'Multi-Level-Build' bezeichnet und ist in examples/multilevel_build demonstriert. Siehe auch mlkem.

Kann ich mein eigenes Backend mitbringen?

Ja, Sie können weitere Backends für ML-KEM-native Arithmetik und/oder für FIPS-202 hinzufügen. Folgen Sie den vorhandenen Backends als Vorlagen oder siehe examples/custom_backend für ein minimales Beispiel, wie Sie ein benutzerdefiniertes Backend registrieren.

Haben Sie eine Frage?

Wenn Sie glauben, einen Sicherheitsfehler in mlkem-native gefunden zu haben, melden Sie die Schwachstelle bitte über Githubs private Schwachstellenmeldung. Bitte erstellen Sie kein öffentliches GitHub-Issue.

Wenn Sie eine andere Frage / ein nicht sicherheitsbezogenes Problem / eine Feature-Anfrage haben, eröffnen Sie bitte ein GitHub-Issue.

Mitwirken

Wenn Sie uns beim Aufbau von mlkem-native helfen möchten, kontaktieren Sie uns bitte. Sie können das mlkem-native-Team über den PQCA-Discord erreichen. Siehe auch CONTRIBUTING.md.