mlkem-native

mlkem-native é uma implementação segura, rápida e portável em C90¹ do ML-KEM². É um fork da implementação de referência do ML-KEM³.

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⁴. 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⁵.

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⁶ ou 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⁸: 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⁹ e os vetores de teste ML-KEM do Wycheproof¹⁰.

ACVP

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

# Usando o script de testes
./scripts/tests acvp
# Usando uma versão específica do ACVP
./scripts/tests acvp --version v1.1.0.41

# Usando o cliente ACVP diretamente
python3 ./test/acvp/acvp_client.py
python3 ./test/acvp/acvp_client.py --version v1.1.0.41

# Usando arquivos de vetores de teste ACVP específicos (baixados do ACVP-Server)
# python3 ./test/acvp/acvp_client.py -p {PROMPT}.json -e {EXPECTED_RESULT}.json
# Por exemplo, supondo que você tenha executado o acima
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

Você pode executar testes Wycheproof¹⁰ usando o script tests ou o cliente Wycheproof diretamente:

# Usando o script de testes
./scripts/tests wycheproof

# Usando o cliente Wycheproof diretamente
python3 ./test/wycheproof/wycheproof_client.py

Benchmarking

Você pode medir desempenho, uso de memória e tamanho do binário usando o script tests:

# Benchmarks de velocidade (-c seleciona o contador de ciclos: NO, PMU, PERF ou MAC)
# Nota: PERF/MAC pode exigir a flag -r para executar binários de benchmarking usando sudo
./scripts/tests bench -c PMU
./scripts/tests bench -c PERF -r

# Análise de uso de pilha
./scripts/tests stack

# Medição do tamanho do binário
./scripts/tests size

Para resultados de benchmark de CI e dados históricos de desempenho, consulte a página de benchmarking.

Uso

Se você quiser usar mlkem-native, importe mlkem para a árvore de fontes do seu projeto e compile usando seu sistema de build favorito. Consulte mlkem para mais informações, e examples/basic para um exemplo simples. O sistema de build fornecido neste repositório é apenas para fins de desenvolvimento.

Consulte API-CONVENTIONS.md para convenções que se aplicam a todas as funções públicas, como valores de retorno, validade de ponteiros e o estado dos buffers de saída em caso de erro.

Posso trazer meu próprio FIPS-202?

mlkem-native depende e vem com uma implementação de FIPS-202¹¹. Se sua biblioteca tem sua própria implementação de FIPS-202, você pode usá-la em vez da que acompanha o mlkem-native. Consulte FIPS202.md, e examples/bring_your_own_fips202 para um exemplo usando tiny_sha3¹².

Preciso usar os backends de assembly?

Não. Se você quiser um build somente em C, basta omitir os diretórios mlkem/src/native e/ou mlkem/src/fips202/native da sua importação e desdefinir MLK_CONFIG_USE_NATIVE_BACKEND_ARITH e/ou MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 no seu mlkem_native_config.h.

Preciso configurar o CBMC para usar mlkem-native?

Não. Embora recomendemos que você considere usá-lo, mlkem-native compilará e executará bem sem CBMC -- apenas certifique-se de incluir cbmc.h e ter CBMC indefinido. Em particular, você não precisa remover todos os contratos de função e invariantes de loop do código; eles serão ignorados a menos que CBMC esteja definido.

O mlkem-native suporta todos os níveis de segurança do ML-KEM?

Sim. O nível de segurança é um parâmetro de tempo de compilação configurado definindo MLK_CONFIG_PARAMETER_SET=512/768/1024 em mlkem_native_config.h. Se sua biblioteca/aplicação exigir vários níveis de segurança, você pode compilar + vincular três instâncias do mlkem-native enquanto compartilha código comum; isso é chamado de 'build multinível' e é demonstrado em examples/multilevel_build. Consulte também mlkem.

Posso trazer meu próprio backend?

Sim, você pode adicionar mais backends para aritmética nativa ML-KEM e/ou para FIPS-202. Siga os backends existentes como modelos ou consulte examples/custom_backend para um exemplo mínimo de como registrar um backend personalizado.

Tem uma Pergunta?

Se você acha que encontrou uma falha de segurança no mlkem-native, por favor relate a vulnerabilidade através do relatório privado de vulnerabilidades do Github. Por favor, não crie uma issue pública no GitHub.

Se você tiver qualquer outra pergunta / problema não relacionado à segurança / solicitação de recurso, por favor abra uma issue no GitHub.

Contribuindo

Se você quiser nos ajudar a construir o mlkem-native, entre em contato. Você pode contatar a equipe do mlkem-native através do Discord da PQCA. Consulte também CONTRIBUTING.md.