From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

Resumo Técnico: Fundamentos Teórico-Ringuais para Verificação de Mascaramento em Hardware PQC

1. O Problema

Com a padronização de algoritmos de Criptografia Pós-Quântica (PQC) pelo NIST, especificamente ML-KEM (FIPS 203) e ML-DSA (FIPS 204), há uma migração em larga escala para hardware acelerado. A principal defesa contra ataques de canal lateral (como análise de consumo de energia) nesses sistemas é o mascaramento aritmético sobre o anel $\mathbb{Z}_q$ (especialmente dentro de transformadas de número teórico - NTT).

O trabalho anterior dos autores, o framework QANARY, realizou uma análise de dependência estrutural em escala (verificando 1,17 milhão de células), mas sua garantia de correção (Teorema 3.9.1) baseava-se em verificação de domínio finito usando solucionadores SMT (Z3 e CVC5).

• A Lacuna: A prova foi verificada exaustivamente apenas para um módulo pequeno ($q=5$), enumerando 225 funções de fio booleanas.
• O Risco: Solucionadores SMT não realizam indução estrutural. Uma prova válida para $q=5$ não garante matematicamente a segurança para os módulos de produção reais: $q=3.329$ (ML-KEM) ou $q=8.380.417$ (ML-DSA). Além disso, a base de confiança dependia de ferramentas complexas (SMT solvers e scripts Python) que não são formalmente verificadas.

2. Metodologia

Os autores substituíram a abordagem de enumeração finita baseada em SMT por uma prova universal formalizada em Lean 4, utilizando a biblioteca matemática Mathlib.

• Abstração Algébrica: Em vez de tratar os dados como vetores de bits com verificações explícitas de estouro (overflow), a metodologia utiliza as axiomas de anéis comutativos de $\mathbb{Z}/q\mathbb{Z}$.
• Reparametrização: O núcleo da prova baseia-se na reparametrização aritmética $s_0 = x - s_1$. No anel $\mathbb{Z}_q$, esta é uma identidade algébrica, não um procedimento computacional sujeito a erros de representação de bits.
• Verificação Kernel: As provas são verificadas pelo kernel do Lean 4, que é pequeno, especificado formalmente e auditável, reduzindo drasticamente a "base de confiança" (trusted base) em comparação com solucionadores SMT.
• Abordagem "Sorry-Free": Todo o conjunto de provas foi mecanizado sem estubs não verificados (sorry), garantindo que 100% do código foi verificado pelo kernel.

3. Principais Contribuições

O artigo apresenta nove teoremas (T1 a T6, incluindo variantes) que fecham a lacuna metodológica:

1. Teorema Principal (T1/T1'): Prova Universal de Independência de Valor:

   • Demonstra que, para qualquer $q > 0$, qualquer função de fio $w$ e qualquer par de segredos, se a função é "independente de valor" (não depende do segredo $x$), então sua distribuição marginal é constante.
   • Impacto: Isso implica que a informação mútua entre o segredo e o fio é zero ($I(x; w) = 0$).
   • Eficiência: A prova requer apenas 5 linhas de script em Lean 4, substituindo as 225 avaliações booleanas anteriores.

2. Teoremas de Suporte:

   • T2 e T3 (Reparametrização): Provas universais de que a reparametrização (XOR para booleanos, subtração para aritmética) é um "round-trip" válido para qualquer tamanho de chave ou módulo.
   • T3' (Bijetividade): Garante que o mapeamento de segredos para máscaras é bijetivo, essencial para a contagem de histogramas.
   • T4 (Limites de Estouro): Estabelece limites que garantem que a implementação em vetores de bits (hardware real) não sofre estouro, conectando a abstração algébrica à implementação física.
   • T5 (Viés de RNG): Caracteriza o viés quando geradores de números aleatórios (RNG) de $k$-bits são reduzidos módulo $q$. Inclui uma verificação nativa para o caso específico do ML-KEM ($q=3.329$) e limites universais.
   • T6 (Contraexemplo de Não-Tightness): Prova que o inverso do teorema principal é falso para todo $q \ge 2$. Ou seja, é possível ter uma distribuição marginal constante sem ser independente de valor. Isso valida que o framework QANARY é conservador (falsos positivos são aceitáveis, falsos negativos não).

4. Resultados

• Validação Universal: A garantia de segurança do QANARY agora se aplica a todos os conjuntos de parâmetros PQC do NIST (atuais e futuros), não apenas a instâncias específicas.
• Redução da Base de Confiança: A verificação migrou de confiar em Z3/CVC5/Python (sistemas complexos não verificados) para confiar apenas no kernel do Lean 4.
• Eficiência de Prova: O que exigia 33,5 milhões de avaliações booleanas em SMT foi reduzido a uma prova de 5 linhas baseada em axiomas de anéis.
• Construção Verificada: O conjunto de provas contém 1.739 tarefas de construção, 0 erros e 0 sorry, rodando em Lean 4.30.0-rc1.

5. Significado e Implicações

• Certificação FIPS 140-3: A prova universal elimina a necessidade de re-verificação exaustiva para cada novo conjunto de parâmetros. Um único teorema cobre ML-KEM, ML-DSA e futuras variantes, reduzindo a carga de trabalho dos laboratórios de validação.
• Mudança de Paradigma: O trabalho demonstra que a teoria dos anéis (e não a lógica de vetores de bits/SAT) é a camada de abstração natural para a verificação de mascaramento aritmético. Isso sugere que outras propriedades complexas (como mascaramento de ordem superior ou conversões mistas) podem admitir provas concisas em um contexto algébrico adequado.
• Confiança em Hardware PQC: Fornece a primeira fundação formal verificada por máquina para a segurança de canais laterais em aceleradores de hardware PQC, garantindo que as proteções contra ataques de energia são matematicamente sólidas independentemente do módulo $q$ utilizado.

Em suma, este artigo transforma a verificação de segurança de PQC de uma abordagem empírica e limitada a casos específicos para uma garantia matemática universal e formalmente verificada, estabelecendo novos padrões para a confiança em implementações de criptografia pós-quântica.