mlkem-native

mlkem-native — это безопасная, быстрая и переносимая реализация ML-KEM[^FIPS203] на C90[^C90]. Она является форком эталонной реализации ML-KEM[^REF].

Весь код на C в mlkem/src/* и mlkem/src/fips202/* доказанно безопасен по памяти (без переполнения памяти) и безопасен по типам (без переполнения целых чисел) с использованием CBMC[^CBMC]. Весь ассемблер для AArch64 и x86_64 доказанно функционально корректен, безопасен по памяти и имеет независимое от секретов время выполнения (constant-time), с использованием HOL-Light[^HOL-Light].

mlkem-native включает нативные бэкенды для Arm (64-бит, Neon), Intel/AMD (64-бит, AVX2), RISC-V (64-бит, RVV) и POWER (ppc64le, VSX). См. benchmarks для данных о производительности.

mlkem-native поддерживается Post-Quantum Cryptography Alliance в составе Linux Foundation.

Быстрый старт для 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

См. BUILDING.md для получения дополнительной информации.

Применение

mlkem-native используется в

• libOQS проекта Open Quantum Safe начиная с 0.13.0 (как реализация ML-KEM по умолчанию)
• Криптографической библиотеке AWS AWS-LC начиная с v1.50.0
• TLS-библиотеке rustls, написанной на Rust, начиная с 0.23.28 (через AWS-LC как провайдер криптографии по умолчанию)
• Pavona — библиотеке модульных, проверенных в производстве и безопасных по умолчанию открытых кремниевых блоков

Формальная верификация

Весь код на C в mlkem/src/* и mlkem/src/fips202/* доказанно безопасен по памяти (без переполнения памяти) и безопасен по типам (без переполнения целых чисел). Для этого используется C Bounded Model Checker (CBMC), и это опирается на контракты функций и аннотации инвариантов циклов в исходном коде. См. proofs/cbmc для подробностей.

Весь ассемблер для AArch64 и x86_64 доказанно функционально корректен, безопасен по памяти и имеет независимое от секретов время выполнения (constant-time), на уровне объектного кода. Для этого используется интерактивный доказатель теорем HOL-Light и инфраструктура верификации s2n-bignum (которая включает модели соответствующих частей архитектур Arm и x86). См. proofs/hol_light для подробностей.

ПРИМЕЧАНИЕ: Формальная верификация никогда не является абсолютной. См. SOUNDNESS.md для подробного анализа области применения, допущений и рисков усилий по формальной верификации вокруг mlkem-native.

Безопасность

Весь ассемблер для AArch64 и x86_64 в mlkem-native формально доказан в HOL Light как свободный от зависимых от секретов потоков управления, шаблонов доступа к памяти и инструкций с переменной задержкой, что предотвращает большинство побочных каналов по времени (см. proofs/hol_light для подробностей). Код на C защищён от побочных каналов по времени, вносимых компилятором (таких как KyberSlash[^KyberSlash] или clangover[^clangover]), с помощью соответствующих барьеров и шаблонов constant-time.

Отсутствие зависимых от секретов ветвлений, шаблонов доступа к памяти и инструкций с переменной задержкой также тестируется с помощью valgrind с различными комбинациями компиляторов и параметров компиляции.

Другие атаки. mlkem-native нацелен на устойчивость только к побочным каналам по времени. Другие классы атак, такие как побочные каналы по питанию и электромагнитному излучению, микроархитектурные побочные каналы (например, спекулятивное выполнение) или атаки с внедрением сбоев, в настоящее время выходят за рамки.

Дизайн

mlkem-native разделён на фронтенд и два бэкенда для арифметики и FIPS202 / SHA3. Фронтенд фиксирован, написан на C и охватывает все процедуры, которые не критичны для производительности. Бэкенды гибкие, отвечают за производительно-критичные процедуры и могут быть реализованы на C или в нативном коде (ассемблер/интринсики); см. mlkem/src/native/api.h для арифметического бэкенда и mlkem/src/fips202/native/api.h для бэкенда FIPS-202.

mlkem-native в настоящее время предлагает следующие бэкенды:

• Бэкенд на переносимом C по умолчанию
• 64-битный бэкенд Arm (с использованием Neon)
• 64-битный бэкенд Intel/AMD (с использованием AVX2)
• 64-битный бэкенд RISC-V (с использованием RVV)
• 64-битный бэкенд POWER (ppc64le, с использованием VSX; поддерживает POWER8 и выше)
• 32-битный бэкенд Armv8.1-M (с использованием Helium/MVE) — см. #1501. Он всё ещё экспериментальный и отключён по умолчанию.

Если вы хотите внести вклад в новые бэкенды, пожалуйста, свяжитесь с нами или просто откройте PR.

Наш ассемблер для AArch64 разработан с использованием супероптимизатора SLOTHY, следуя подходу, описанному в статье о SLOTHY[^SLOTHY_Paper]: Мы пишем «чистый» ассемблер вручную и автоматизируем микрооптимизации (например, см. clean против optimized NTT для AArch64). См. dev/README.md для более подробной информации.

Тестовые векторы

mlkem-native тестируется на всех официальных ACVP ML-KEM тестовых векторах[^ACVP] и тестовых векторах ML-KEM Wycheproof[^wycheproof].

ACVP

Вы можете запустить тесты ACVP с помощью скрипта tests или напрямую ACVP-клиента: