Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

1. Declaração do Problema

Padrões de Criptografia Pós-Quântica (PQC) como ML-KEM (FIPS 203) e ML-DSA (FIPS 204) dependem fortemente de pipelines de Transformada Numérica Teórica (NTT). Essas pipelines consistem em estágios lineares de "borboleta" e estágios não lineares de redução modular, tipicamente implementados usando redução de Barrett.

Embora as estruturas existentes de verificação formal (ISW, t-SNI, PINI, DOM) ofereçam garantias robustas para mascaramento booleano sobre $GF(2)$, elas carecem de caracterizações verificadas por máquina para mascaramento aritmético sobre campos primos ($\mathbb{Z}_q$), especificamente para redução de Barrett.

• A Lacuna: Implementações de hardware (por exemplo, o design "Adams Bridge") frequentemente sofrem de vulnerabilidades de canal lateral porque a subtração condicional não linear na redução de Barrett quebra a estrutura afim assumida pelos teoremas de composição padrão.
• A Questão: Sob mascaramento aritmético de primeira ordem, qual é o limite preciso de vazamento dos fios internos de um circuito de redução de Barrett? Ferramentas anteriores não podiam fornecer uma resposta universal, verificada por máquina, levando a incertezas na certificação FIPS 140-3.

2. Metodologia

Os autores empregam uma abordagem de verificação formal usando o assistente de prova Lean 4 e a biblioteca Mathlib.

• Formalização: Eles definem o mapa de fios interno de Barrett algebricamente sobre $\mathbb{Z}_q$ (onde $q$ é o módulo). O mapa $f_x(m)$ toma um segredo $x$ e uma máscara aleatória $m$, produzindo uma saída baseada em uma estrutura de dois ramos determinada por uma subtração condicional.
• Estratégia de Prova: Em vez de simular instâncias específicas, eles provam teoremas universais que valem para todos $q > 0$ e parâmetros de deslocamento $s$.
• Conceito Chave: Eles analisam a cardinalidade da pré-imagem: para um segredo fixo $x$ e um valor de saída específico $v$, quantas máscaras distintas $m$ poderiam ter produzido $v$?
• Cadeia de Ferramentas: O artefato contém 12 resultados provados com zero sorry (nenhuma prova incompleta), garantindo que cada passo seja verificado pelo kernel pelo Lean.

3. Contribuições Principais

A. O Teorema da Tricotomia

O artigo prova que o mapa de fios interno de Barrett exibe uma estrutura de pré-imagem de três valores. Para qualquer segredo $x$ e qualquer saída $v$, o número de máscaras $m$ tal que $f_x(m) = v$ é exatamente 0, 1 ou 2.

• Mecanismo: A subtração condicional cria dois ramos afins (translações em $\mathbb{Z}_q$). A pré-imagem de qualquer valor é um subconjunto de no máximo dois candidatos: $\{x - v, x - v + r\}$, onde $r = 2^s \mod q$.
• Universalidade: Isso vale para qualquer módulo $q$ e deslocamento $s$, independente de parâmetros específicos de PQC.

B. A Barreira de 1 Bit

Com base na tricotomia, os autores estabelecem um limite universal de vazamento:

• Máxima Multiplicidade: Como o número máximo de máscaras que produzem uma única saída é 2, a probabilidade máxima de observar um valor de saída específico é $2/q$.
• Limite de Entropia Mínima: A entropia mínima condicional $H_\infty(\text{saída} \mid x)$ é limitada inferiormente por $\log_2(q) - 1$.
• Interpretação: A redução de Barrett vaza no máximo 1 bit de entropia mínima por fio interno sob sondagem de primeira ordem. Este é um limite "conservador" porque muitos valores de saída são inatingíveis (contagem de pré-imagem = 0), o que significa que o vazamento real é frequentemente estritamente menor que 1 bit.

C. O Framework PF-PINI

Os autores introduzem o PINO de Campo Primo (PF-PINI), uma nova métrica de segurança para gadgets aritméticos sobre $\mathbb{Z}_q$:

• Definição: Um gadget é PF-PINI($k$) se a cardinalidade da pré-imagem for limitada por $k$.
• Instanciações:
  • Estágios de Borboleta: Satisfazem PF-PINI(1) (bijecção perfeita, vazamento zero além da máscara).
  • Redução de Barrett: Satisfaz PF-PINI(2) (a Barreira de 1 Bit).
• Observação de Composição: Eles observam (embora ainda não provado formalmente) que, se os estágios da pipeline forem separados por mascaramento fresco entre estágios, a máxima multiplicidade da pipeline composta é $\max(k_1, k_2)$. Isso implica que a Barreira de 1 Bit se propaga através de toda a pipeline NTT.

4. Resultados e Análise

• Provas Verificadas por Máquina: O artefato inclui 12 teoremas verificados, incluindo a tricotomia, provas de exatidão (mostrando que a contagem=2 é alcançável) e instanciações PF-PINI.
• Descoberta de Lacuna de Suporte: A análise revela valores de saída "inalcançáveis" (contagem de pré-imagem = 0). Isso é um recurso de segurança, não um defeito, pois reduz a informação efetiva do adversário.
• Estudo de Caso Adams Bridge: O artigo analisa a implementação de hardware "Adams Bridge":
  • Falha intra-estágio: Trabalhos anteriores (Artigos 1 e 2) mostraram vulnerabilidades devido à interação de compartilhamentos sem mascaramento intermediário.
  • Falha inter-estágio: Este artigo identifica que o Adams Bridge falha em aplicar mascaramento fresco entre estágios. Consequentemente, o limite de composição PF-PINI não se aplica, permitindo que o vazamento se multiplique ($k_1 \times k_2$) em vez de permanecer limitado pelo máximo ($\max(k_1, k_2)$). Isso explica por que o design é vulnerável, apesar da existência da Barreira de 1 Bit para portas de Barrett individuais.
• Impacto Quantitativo:
  • Para ML-KEM ($q=3329$): Vazamento $\le 1$ bit (Entropia mínima $\ge 10,70$ bits).
  • Para ML-DSA ($q=8.380.417$): Vazamento $\le 1$ bit (Entropia mínima $\ge 21,99$ bits).

5. Significado

• Prontidão para Certificação: A Barreira de 1 Bit fornece um certificado universal, verificado por máquina para designers de hardware. Permite que avaliadores certifiquem implementações baseadas em Barrett para FIPS 140-3 sem re-verificar conjuntos de parâmetros específicos.
• Orientação de Design: Esclarece que o requisito arquitetônico primário para segurança é o mascaramento fresco entre estágios. Se isso for implementado, a natureza não linear da redução de Barrett não compromete a segurança da pipeline NTT além de uma perda insignificante de 1 bit.
• Mudança Metodológica: O artigo move a análise de canal lateral de simulação empírica e verificação baseada em SAT para provas algébricas verificadas pelo kernel, estabelecendo um novo padrão para verificação de hardware PQC.
• Completando o Programa de Cinco Artigos: Este trabalho fecha a lacuna deixada por artigos anteriores na série, avançando da construção de ferramentas (Artigo 1) e quantificação de ataques (Artigo 2) para fundamentos algébricos (Artigo 3), composição linear (Artigo 4) e, finalmente, caracterização não linear (Artigo 5).

6. Limitações e Trabalhos Futuros

• Prova de Composição: A afirmação de que $\max(k_1, k_2)$ vale para pipelines compostas com mascaramento fresco é atualmente uma observação, não um teorema formal.
• Mascaramento de Ordem Superior: Os resultados são limitados ao mascaramento de primeira ordem ($t=1$). Segurança de ordem superior requer a análise de pré-imagens conjuntas através de múltiplos fios.
• Formalização de Entropia: Embora o limite algébrico seja provado, o limite de entropia mínima teórico da informação depende de definições padrão que ainda não foram totalmente integradas ao Mathlib.
• Outras Reduções: Os resultados são específicos para redução de Barrett; reduções de Montgomery e de livro escolar exigem análise separada.

Em resumo, este artigo estabelece que a redução de Barrett é fundamentalmente segura sob mascaramento aritmético de primeira ordem, vazando não mais que 1 bit de informação por fio, desde que mascaramento fresco seja aplicado entre os estágios da pipeline. Isso fornece uma base matemática rigorosa para a segurança de hardware PQC de próxima geração.