mlkem-native

mlkem-native é uma implementação segura, rápida e portável em C90[^C90] do ML-KEM[^FIPS203]. É um fork da implementação de referência do ML-KEM[^REF].

Todo o código C em mlkem/src/* e mlkem/src/fips202/* é comprovadamente seguro em relação à memória (sem estouro de memória) e seguro em relação a tipos (sem estouro de inteiros) usando CBMC[^CBMC]. Todo o assembly AArch64 e x86_64 é comprovadamente correto funcionalmente, seguro em relação à memória e de temporização independente de segredos (tempo constante), usando HOL-Light[^HOL-Light].

mlkem-native inclui backends nativos para Arm (64 bits, Neon), Intel/AMD (64 bits, AVX2), RISC-V (64 bits, RVV) e POWER (ppc64le, VSX). Consulte benchmarks para dados de desempenho.

mlkem-native é apoiado pela Post-Quantum Cryptography Alliance como parte da Linux Foundation.

Início rápido para Ubuntu

# Instalar pacotes base
sudo apt-get update
sudo apt-get install make gcc python3 git

# Clonar mlkem-native
git clone https://github.com/pq-code-package/mlkem-native.git
cd mlkem-native

# Compilar e executar testes
make build
make test

# O mesmo usando `tests`, um wrapper conveniente em torno de `make`
./scripts/tests all
# Mostrar todas as opções
./scripts/tests --help

Consulte BUILDING.md para mais informações.

Aplicações

mlkem-native é usado em

• libOQS do projeto Open Quantum Safe desde 0.13.0 (como a implementação padrão de ML-KEM)
• A biblioteca de criptografia da AWS AWS-LC desde v1.50.0
• A biblioteca TLS rustls escrita em Rust desde 0.23.28 (através da AWS-LC como o provedor de criptografia padrão)
• Pavona - uma biblioteca de blocos de silício abertos modulares, comprovados em tapeout e seguros por padrão

Verificação Formal

Todo o código C em mlkem/src/* e mlkem/src/fips202/* é comprovadamente seguro em relação à memória (sem estouro de memória) e seguro em relação a tipos (sem estouro de inteiros). Isso usa o C Bounded Model Checker (CBMC) e se baseia em contratos de função e anotações de invariantes de loop no código-fonte. Consulte proofs/cbmc para detalhes.

Todo o assembly AArch64 e x86_64 é comprovadamente correto funcionalmente, seguro em relação à memória e com temporização independente de segredos (tempo constante), no nível do código-objeto. Isso usa o provador de teoremas interativo HOL-Light e a infraestrutura de verificação s2n-bignum (que inclui modelos das partes relevantes das arquiteturas Arm e x86). Consulte proofs/hol_light para detalhes.

NOTA: A Verificação Formal nunca é absoluta. Consulte SOUNDNESS.md para uma análise detalhada do escopo, suposições e riscos dos esforços de verificação formal em torno do mlkem-native.

Segurança

Todo o assembly AArch64 e x86_64 em mlkem-native é formalmente comprovado em HOL Light como livre de fluxo de controle dependente de segredos, padrões de acesso à memória e instruções de latência variável, frustrando a maioria dos canais laterais de temporização (consulte proofs/hol_light para detalhes). O código C é endurecido contra canais laterais de temporização introduzidos pelo compilador (como KyberSlash[^KyberSlash] ou clangover[^clangover]) através de barreiras adequadas e padrões de tempo constante.

A ausência de ramificações dependentes de segredos, padrões de acesso à memória e instruções de latência variável também é testada usando valgrind com várias combinações de compiladores e opções de compilação.

Outros ataques. mlkem-native visa resistência apenas contra canais laterais de temporização. Outras classes de ataque, como canais laterais de potência e eletromagnéticos, canais laterais microarquiteturais (por exemplo, execução especulativa) ou ataques de injeção de falhas, estão atualmente fora do escopo.

Design

mlkem-native é dividido em um frontend e dois backends para aritmética e FIPS202 / SHA3. O frontend é fixo, escrito em C, e cobre todas as rotinas que não são críticas para o desempenho. Os backends são flexíveis, cuidam de rotinas sensíveis ao desempenho e podem ser implementados em C ou código nativo (assembly/intrínsecos); consulte mlkem/src/native/api.h para o backend aritmético e mlkem/src/fips202/native/api.h para o backend FIPS-202.

mlkem-native atualmente oferece os seguintes backends:

• Backend C portável padrão
• Backend Arm de 64 bits (usando Neon)
• Backend Intel/AMD de 64 bits (usando AVX2)
• Backend RISC-V de 64 bits (usando RVV)
• Backend POWER de 64 bits (ppc64le, usando VSX; suporta POWER8 e superior)
• Backend Armv8.1-M de 32 bits (usando Helium/MVE) -- consulte #1501. Isso ainda é experimental e desabilitado por padrão.

Se você quiser contribuir com novos backends, entre em contato ou apenas abra um PR.

Nosso assembly AArch64 é desenvolvido usando o superotimizador SLOTHY, seguindo a abordagem descrita no artigo SLOTHY[^SLOTHY_Paper]: Escrevemos assembly 'limpo' à mão e automatizamos micro-otimizações (por exemplo, consulte o NTT AArch64 clean vs otimizado). Consulte dev/README.md para mais detalhes.

Vetores de Teste

mlkem-native é testado contra todos os vetores de teste oficiais ACVP ML-KEM[^ACVP] e os vetores de teste ML-KEM do Wycheproof[^wycheproof].

ACVP

Você pode executar testes ACVP usando o script tests ou o cliente ACVP diretamente: