The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

Resumo Técnico: A Barreira de 1 Bit é Universal

Declaração do Problema
A Transformada Numérica Teórica (NTT) serve como a espinha dorsal computacional para os padrões de criptografia pós-quântica (PQC) do NIST ML-DSA (FIPS 204) e ML-KEM (FIPS 203). As implementações em hardware desses padrões dependem de mascaramento aritmético para resistir a ataques de canal lateral, especificamente Análise de Potência Diferencial (DPA). Embora o mascaramento booleano sobre $GF(2^n)$ tenha estabelecido frameworks de composabilidade (por exemplo, PINI), o mascaramento aritmético sobre $\mathbb{Z}_q$ para primo $q$ apresenta desafios únicos.

Trabalhos anteriores no programa QANARY (Papers 1–6) estabeleceram análises de dependência estrutural e quantificaram margens de segurança para componentes específicos, provando notavelmente que a redução de Barrett satisfaz uma "Barreira de 1 Bit" (PF-PINI(2)). No entanto, duas lacunas críticas permaneceram:

1. Profundidade de Pipeline Arbitrária: Os teoremas de composição anteriores eram limitados a dois estágios. Não havia garantia formal para pipelines de $k$ estágios arbitrários com mascaramento fresco entre estágios.
2. Redução de Montgomery: Embora a redução de Barrett tivesse sido caracterizada, a redução de Montgomery — a segunda redução modular padrão usada em hardware NTT (dominante em ML-DSA e algumas implementações de ML-KEM) — carecia de uma caracterização formal PF-PINI.
3. Limites Unificados de Ponta a Ponta: Não havia um único limite de cardinalidade verificado por máquina que reunisse os resultados para pipelines arbitrários compostos por borboletas, reduções de Barrett e reduções de Montgomery.

Metodologia
O artigo emprega verificação formal usando o assistente de prova Lean 4. A abordagem é estritamente construtiva, com zero sorry (pressupostos não provados) e zero axiomas não padrão. A metodologia baseia-se em:

• Definição PF-PINI: Uso do parâmetro de Não-Interferência de Isolamento de Sonda de Campo Primo (PF-PINI), que quantifica o vazamento de um gadget de fio único sob uma única máscara aritmética. Um gadget é PF-PINI($M$) se a cardinalidade do pré-imagem de qualquer valor de saída for no máximo $M$.
• Modelagem de Pipeline: Definição de um pipeline de $k$ estágios onde cada estágio $G_i$ é um gadget PF-PINI, separado por máscaras aleatórias frescas. A saída do pipeline é computada recursivamente.
• Análise Combinatória: Prova de que o mascaramento fresco entre estágios "apaga" os parâmetros de vazamento dos estágios intermediários, deixando o limite final dependente apenas do parâmetro do último estágio.
• Modelagem Fiel ao Hardware: Modelagem da redução de Montgomery para levar em conta as larguras de registradores de hardware e o comportamento de estouro (wraparound), analisando especificamente o deslocamento de colisão $2^{w-s}$.

Principais Contribuições
O artigo faz quatro contribuições primárias, todas formalizadas em Lean 4:

1. O Teorema de Composição de $k$ Estágios (Teorema 3.1):
   Este teorema generaliza o resultado anterior de composição de 2 estágios para profundidade arbitrária $k \ge 1$. Ele prova que, para um pipeline de gadgets $G_0, \dots, G_{k-1}$ com mascaramento fresco entre estágios, a cardinalidade do pré-imagem da saída é limitada por:
   $$| \{ (m, f) : \text{saída do pipeline} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   Crucialmente, o limite é determinado pelo último estágio; os parâmetros de todos os estágios intermediários são apagados pelas máscaras frescas.

2. Redução de Montgomery é PF-PINI(2) (Teorema 4.3):
   O artigo prova formalmente que a redução de Montgomery satisfaz a propriedade PF-PINI(2), espelhando a estrutura da redução de Barrett. Ele demonstra que o mapa de Montgomery fiel ao hardware possui uma estrutura de "dois ramos" (dependente de se ocorre um estouro), resultando em uma cardinalidade de pré-imagem de no máximo 2. O Teorema 4.7 estabelece ainda a justeza deste limite, mostrando que, para parâmetros padrão (ML-KEM e ML-DSA), a multiplicidade é exatamente 2.

3. Limite de Multiplicidade de Ponta a Ponta (Teorema 5.1):
   Ao combinar o teorema de composição de $k$ estágios com os resultados específicos PF-PINI(2) para Barrett (Paper 5), Montgomery (este artigo) e borboletas (Paper 4), o artigo estabelece um limite unificado. Para qualquer pipeline de $k$ estágios onde cada estágio satisfaz $\text{maxMult} \le 2$, a cardinalidade do pré-imagem da saída é limitada por:
   $$2 \cdot q^{2k-2}$$
   Sob o modelo de sondagem de primeira ordem com máscaras uniformes, isso corresponde a um limite de probabilidade condicional por observação de $2/q$, independente da profundidade do pipeline $k$.

4. Ancoragem Formal de Achados Empíricos (Teorema 5.4):
   O artigo fornece uma condição verificada em Lean afirmando que, se qualquer estágio em um pipeline tiver $\text{maxMult} \ge 3$ (por exemplo, um estágio não mascarado), a hipótese do limite de ponta a ponta falha. Isso ancora formalmente análises empíricas e estruturais anteriores do acelerador PQC "Adams Bridge" (Papers 1, 2 e trabalhos externos), confirmando que configurações específicas não mascaradas nesse projeto ficam fora das condições suficientes para o limite independente de profundidade.

Resultados

• Universalidade da Barreira de 1 Bit: O artigo confirma que a "Barreira de 1 Bit" (uma cardinalidade de pré-imagem de 2) aplica-se a ambas as reduções modulares padrão (Barrett e Montgomery) usadas em hardware PQC do NIST.
• Independência de Profundidade: As provas formais demonstram que adicionar estágios a um pipeline não degrada o limite de vazamento por observação, desde que seja usado mascaramento fresco entre estágios e cada estágio satisfaça PF-PINI($\le 2$).
• Status de Verificação: Todo o artefato consiste em 20 declarações em três módulos de teoremas, compilando em 1.753 trabalhos com zero erros, zero sorry e sem procedimentos decisórios nativos.

Significado e Alegações
O artigo posiciona-se como a conclusão de um programa de verificação formal para hardware NTT mascarado. Seu significado reside em fornecer uma fundação composicional quantitativa e verificada por máquina para designers de hardware.

• Para Certificação: O limite de cardinalidade derivado ($2 \cdot q^{2k-2}$) fornece a evidência específica necessária para argumentos de resistência a DPA no nível de arquitetura, complementando ferramentas de nível de porta como SILVER e maskVerif.
• Para Designers: Oferece um caminho prescritivo de remediação: para alcançar um limite independente de profundidade, os designers devem garantir que cada estágio seja PF-PINI($\le 2$) e inserir máscaras frescas entre os estágios.
• Modéstia das Alegações: Os autores afirmam explicitamente que as interpretações de probabilidade e entropia mínima (por exemplo, $2/q$) são consequências semânticas informais dos limites de cardinalidade e não são formalizadas mecanicamente no Lean. Além disso, em relação à análise do Adams Bridge, o artigo alega apenas que configurações específicas falham nas condições suficientes do Teorema 5.1; não alega que o hardware está "quebrado" ou "inseguro", reconhecendo que frameworks alternativos ou modelos mais fortes podem produzir conclusões diferentes. O trabalho é enquadrado como uma ferramenta para análise composicional, em vez de um veredito de segurança definitivo sobre implementações específicas.