Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

1. Declaração do Problema

O artigo aborda uma lacuna crítica na verificação formal de segurança de hardware de Criptografia Pós-Quântica (PQC), especificamente para implementações de Transformada Numérica Teórica (NTT) usadas nos padrões do NIST (ML-KEM e ML-DSA).

• O Contexto: Implementações de hardware de NTT dependem de mascaramento aritmético sobre corpos primos ($\mathbb{Z}_q$) para resistir a ataques de canal lateral, como Análise de Potência Diferencial (DPA).
• A Lacuna: Embora o mascaramento booleano (sobre $GF(2^n)$) possua uma teoria de composição madura (NI, SNI, PINI) com provas verificadas por máquina, o mascaramento aritmético sobre corpos primos carece de teoremas de composição análogos.
• O Problema Específico: No mascaramento aritmético, operações como redução modular (por exemplo, redução de Barrett) interagem com máscaras de maneiras não triviais. Diferentemente do XOR booleano, onde o mascaramento preserva a uniformidade perfeitamente, o mascaramento aritmético pode resultar em distribuições de saída não uniformes (multiplicidade > 1).
• A Vulnerabilidade: Análises empíricas e estudos estruturais anteriores identificaram vulnerabilidades no acelerador PQC "Adams Bridge" da Microsoft, onde fios intermediários entre estágios do pipeline eram não uniformes, permitindo ataques DPA. No entanto, faltava uma explicação teórica formal sobre por que isso acontece e como corrigi-lo por meio de teoremas de composição.

2. Metodologia

Os autores empregam verificação formal utilizando o assistente de provas Lean 4 para derivar e provar teoremas de composição para mascaramento aritmético.

• Modelo Formal: Eles definem uma métrica de segurança quantitativa chamada PF-PINI(k) (Prime-Field Probe Isolating Non-Interference).
  • Diferentemente de noções de segurança binárias (seguro/inseguro), o PF-PINI mede a multiplicidade dos valores de saída em relação ao espaço de máscaras.
  • $k=1$ implica uma distribuição perfeitamente uniforme.
  • $k=2$ implica uma multiplicidade máxima de 2, vazando até 1 bit de informação por fio.
• O "Argumento de Renovação": A principal insight teórica é que aplicar uma máscara aleatória fresca entre dois estágios do pipeline "apaga" completamente o parâmetro de segurança ($k_1$) do primeiro estágio do fio intermediário, independentemente de quão não uniforme tenha sido a saída do primeiro estágio.
• Ponte de Hardware: Os autores conectam formalmente a lacuna entre modelos algébricos abstratos ($\mathbb{Z}_q$) e aritmética de números naturais fiel ao hardware (Nat) usada em projetos RTL, especificamente para redução de Barrett.
• Escopo de Verificação: Todo o trabalho consiste em 18 teoremas verificados por máquina com zero stubs sorry (nenhuma suposição não provada), garantindo níveis de confiança elevados.

3. Contribuições Principais

O artigo apresenta seis contribuições primárias:

1. O Teorema de Renovação (Teorema 4.1): Prova que, se uma máscara aleatória fresca for aplicada entre dois estágios ($G_1 \to G_2$), o fio intermediário torna-se perfeitamente uniforme. O conjunto de pares de máscaras que produzem qualquer valor intermediário específico tem cardinalidade exatamente $q$, independente do parâmetro de segurança de $G_1$.
2. Teorema de Composição Positiva (Teorema 4.4): Demonstra que um pipeline de dois estágios com mascaramento fresco satisfaz PF-PINI($k_2$). A segurança da saída composta depende apenas do parâmetro do segundo estágio ($k_2$); a fraqueza do primeiro estágio ($k_1$) é completamente apagada.
3. Teoremas de Composição Negativa (Teoremas 5.1–5.3): Prova que sem mascaramento fresco, o fio intermediário retém a multiplicidade do primeiro estágio ($k_1$). Se $k_1 > 1$, o fio é não uniforme, criando uma condição necessária para ataques DPA.
4. Ponte Algébrica-Hardware (Teorema 6.1): Prova formalmente que o mapa de redução algébrica de Barrett é equivalente ao mapa de aritmética Nat fiel ao hardware sob condições de escopo padrão ($q \le 2^s$). Isso valida que os limites teóricos se aplicam diretamente a implementações em silício.
5. Diagnóstico do Adams Bridge: Instancia formalmente os teoremas para diagnosticar o acelerador Adams Bridge da Microsoft. A prova confirma que a falta de mascaramento inter-estágio fresco deixa os fios de saída de Barrett não uniformes (PF-PINI(2)), explicando o sucesso de ataques DPA empíricos anteriores.
6. Barreira Universal de 1 Bit: Fornece evidência computacional de que o limite PF-PINI(2) é universal para reduções modulares (tanto Barrett quanto Montgomery), sugerindo uma "Barreira de 1 Bit" fundamental para essas operações.

4. Resultados Principais

• Prova Formal de Composição: O artigo estabelece que o mascaramento inter-estágio fresco é a condição necessária e suficiente para compor gadgets aritméticos com segurança.
• Segurança Quantitativa:
  • Com Mascaramento Fresco: O fio intermediário é uniforme ($k=1$). A saída final é limitada pelo parâmetro do segundo estágio ($k_2$).
  • Sem Mascaramento Fresco: O fio intermediário é não uniforme (até $k_1$). Essa não uniformidade é a causa raiz do vazamento de canal lateral observado em ataques empíricos.
• Correção do Adams Bridge: O diagnóstico confirma que adicionar um único registrador de máscara aleatória fresca e uma operação de subtração entre os estágios Butterfly e Barrett no pipeline do Adams Bridge eliminaria a vulnerabilidade DPA nos fios intermediários sem alterar o parâmetro de segurança da saída final.
• Disponibilidade do Artefato: O código-fonte completo do Lean 4, incluindo 18 teoremas e um script de reprodução, está publicamente disponível, permitindo a verificação independente das provas.

5. Significado

• Primeira Composição Aritmética Verificada por Máquina: Este é o primeiro trabalho a fornecer teoremas de composição verificados por máquina para mascaramento aritmético sobre corpos primos, preenchendo uma grande lacuna teórica na segurança de hardware PQC.
• Conectando Teoria e Prática: Ao vincular formalmente provas algébricas abstratas à aritmética fiel ao hardware, o artigo fornece uma base rigorosa para verificar projetos reais de silício, indo além do teste empírico.
• Diretriz de Projeto: Estabelece uma regra de projeto clara e provável para hardware PQC: Sempre insira mascaramento fresco entre estágios do pipeline. Essa simples mudança arquitetural garante que a segurança do pipeline composto seja determinada exclusivamente pelo elo mais fraco no estágio final, e não nos intermediários.
• Convergência de Evidências: A prova formal alinha-se perfeitamente com três análises independentes anteriores (análise de potência empírica, revisão de código e análise de dependência estrutural), confirmando que a falha arquitetural identificada no acelerador Adams Bridge é de fato a causa raiz de sua vulnerabilidade.

Em resumo, este artigo fornece a espinha dorsal matemática e de verificação formal necessária para projetar aceleradores de hardware seguros, composáveis e resistentes a canais laterais para a nova era da Criptografia Pós-Quântica.