💻 computer science

Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

Este artigo apresenta três resultados verificados mecanicamente em Lean 4 que demonstram que o mascaramento aritmético fresco em cada estágio de um pipeline de Transformada Numérica Teórica (NTT) garante segurança de nível de pipeline sob o modelo de sondagem ISW, preenchendo uma lacuna crítica na formalização de segurança para aceleradores de criptografia pós-quântica.

Autores originais: Ray Iskander, Khaled Kirah

Publicado 2026-04-23

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Ray Iskander, Khaled Kirah

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está construindo um trem de alta velocidade (o acelerador criptográfico) que precisa transportar segredos valiosos (dados de criptografia pós-quântica) através de uma paisagem cheia de espiões (hackers).

Este trem não viaja em uma única linha reta; ele passa por várias estações de troca de trilhos chamadas NTT (Transformada Numérica Teórica). Em cada estação, o trem precisa ser protegido contra os espiões que tentam espiar uma única janela (o modelo de "sonda" de primeira ordem).

Aqui está a explicação do que este artigo descobriu, usando analogias do dia a dia:

1. O Grande Equívoco: "Se cada carro é seguro, o trem todo é seguro?"

Muitos engenheiros pensavam: "Se eu proteger cada estação de troca de trilhos individualmente com um segredo, o trem inteiro estará seguro."

A Realidade: O artigo diz: "Não necessariamente!"
A Analogia: Imagine que você tem 10 carros blindados. Se você proteger cada carro, mas não trocar os segredos entre eles, um espião pode observar o carro 1, depois o carro 2, e juntar as pistas para descobrir o segredo total.
O Problema Específico: O artigo descobriu que existe uma "armadilha" mental. Os engenheiros tentavam verificar se o segredo mudava a janela do trem. Eles viam que a janela mudava e pensavam: "Oh, o trem é inseguro!". Mas isso era falso. A janela deveria mudar. O que importa é que, quando você olha para a janela através de um filtro aleatório (uma máscara fresca), o segredo original se torna invisível.

2. A Solução Mágica: "Máscaras Frescas" (Fresh Masking)

O artigo prova matematicamente (usando um computador chamado Lean 4 que não erra) que existe uma regra de ouro para tornar esse trem seguro:

Regra de Ouro: Em cada estação do trem, você deve jogar um novo dado aleatório (uma "máscara fresca") e misturá-lo com o segredo.

A Analogia do Camaleão: Imagine que o segredo é uma cor. Em cada estação, você joga tinta de uma cor aleatória sobre o segredo.
- Se você usar a mesma tinta em todas as estações, o espião pode ver o padrão.
- Se você usar uma tinta nova e aleatória em cada estação, o espião nunca consegue adivinhar a cor original, não importa em qual estação ele espione.
A Prova: O artigo diz: "Se você fizer isso (usar tinta nova em cada estação), garantimos matematicamente que o segredo permanece invisível, não importa o tamanho do trem ou a cor da tinta."

3. O Vilão: O Trem "Adams Bridge"

O artigo aponta para um trem real chamado Adams Bridge (usado em chips de segurança modernos).

O Erro: Esse trem usa tinta nova apenas na primeira estação. Nas estações seguintes, ele continua a viajar sem a tinta nova.
A Consequência: É como se o trem saísse da primeira estação blindado, mas nas estações seguintes, as janelas ficassem transparentes. O artigo explica por que isso é inseguro: porque a regra de "máscara fresca" foi quebrada. O trem não é seguro porque a proteção parou de ser renovada.

4. Por que isso é importante? (A Prova do Computador)

Antes, os engenheiros tinham que confiar na intuição ou em testes manuais.

O que este artigo faz: Ele escreveu um "livro de regras" para um computador super-inteligente (Lean 4) e pediu para ele provar que a regra da "máscara fresca" funciona para qualquer tamanho de trem e qualquer tipo de segredo.
O Resultado: O computador verificou cada linha da matemática e disse: "Sim, está tudo correto. Zero erros."
Isso é crucial para a certificação de segurança (como o selo FIPS), pois dá aos engenheiros uma prova incontestável de que o design deles é seguro, em vez de apenas "parecer" seguro.

Resumo em uma frase:

Este artigo provou com um computador que, para proteger segredos em chips de criptografia, você precisa jogar um novo segredo aleatório em cada etapa do processo; se você parar de fazer isso (como o trem Adams Bridge), o segredo fica vulnerável, e agora temos uma prova matemática irrefutável disso.

O que não é coberto:
O artigo foca nas partes "fáceis" e lineares do trem (como somar números). As partes "difíceis" e não-lineares (como multiplicar números complexos) são tratadas em outros artigos futuros, mas a lição principal sobre "renovar o segredo a cada passo" é o pilar fundamental.

Resumo Técnico: Fresh Masking Makes NTT Pipelines Composable

1. O Problema

Os aceleradores de hardware para Criptografia Pós-Quantum (PQC), especificamente para os padrões ML-KEM (FIPS 203) e ML-DSA (FIPS 204), dependem da Transformada Numérica Teórica (NTT) implementada como um pipeline de estágios de "borboleta" (butterfly) de Cooley-Tukey sobre o anel $\mathbb{Z}_q$ .

Existe uma lacuna crítica na segurança formal desses sistemas:

Falta de Composição Formal: Embora frameworks de composição de mascaramento (como ISW, t-SNI, PINI, DOM) tenham sido formalizados para circuitos booleanos sobre $GF(2)$, não havia nenhuma prova verificada por máquina para a composição de estágios de mascaramento aritmético em pipelines de NTT sobre $\mathbb{Z}_q$ .
A Armadilha da Intuição: Engenheiros frequentemente assumem que, se cada estágio individual é seguro, o pipeline inteiro é seguro. No entanto, a propriedade de segurança intuitiva ("independência de valor pontual") é falsa para saídas de borboletas aritméticas.
Caso Real (Adams Bridge): A implementação de referência "Adams Bridge" (usada no Caliptra) falha em injetar mascaramento fresco entre os estágios do pipeline (o mascaramento é ativo apenas no round 0). Isso viola as hipóteses de segurança, resultando em uma margem de segurança reduzida, conforme detectado empiricamente em trabalhos anteriores, mas sem uma explicação algébrica formal até este momento.

2. Metodologia

Os autores utilizaram o assistente de prova Lean 4 com a biblioteca Mathlib para formalizar e verificar matematicamente as propriedades de segurança.

Abordagem: Prova formal de teoremas com "zero sorry" (sem lacunas não provadas) e zero axiomas não verificados.
Modelo de Ameaça: Modelo de sondagem (probing model) de primeira ordem (ISW), onde um adversário pode observar um único fio por ciclo de relógio.
Escopo: Os resultados são universais, válidos para qualquer módulo $q > 0$ (incluindo primos como 3329 e 8380417, e compostos), todos os fatores de torção (twiddle factors) e qualquer profundidade de pipeline.
Artefato: O código fonte consiste em 3 arquivos Lean (~580 linhas), gerando 1.738 tarefas de compilação, todos passando com sucesso.

3. Principais Contribuições

O artigo apresenta três resultados principais formalizados:

A. A Ponte "r-bearing" (r-bearing Bridge)

Objetivo: Fechar uma limitação declarada em trabalhos anteriores (Paper 3).
Resultado: Prova que a "independência de valor" (value-independence) implica em uma distribuição marginal constante sob aleatoriedade fresca (fresh randomness).
Mecanismo: Formaliza isso através de um proxy algébrico chamado MutualInfoZero, estabelecendo que a informação mútua entre o segredo e o fio é zero quando a aleatoriedade é fresca.

B. Uniformidade Per-Contexto da Borboleta (Butterfly Per-Context Uniformity)

A Armadilha (The Trap): O artigo prova formalmente que a "independência de valor pontual" (onde o valor do fio não muda se o segredo mudar, mantendo as máscaras fixas) é falsa para saídas de borboletas. Um projetista que verifica essa propriedade incorretamente concluiria que o design é inseguro.
A Propriedade Correta: A segurança real reside na uniformidade marginal sobre a máscara fresca. Para qualquer saída da borboleta, existe exatamente um valor de máscara fresca que produz um determinado valor de saída, independentemente dos segredos de entrada.
Universalidade: Esta propriedade é provada para todos os $q > 0$ , tornando-a aplicável a qualquer padrão PQC futuro.

C. Composição de Pipeline (Pipeline Composition)

Teorema Principal: Um pipeline de NTT com $k$ estágios, onde cada estágio utiliza uma máscara de saída fresca e independente, satisfaz a uniformidade per-contexto em cada estágio.
Implicação: Isso valida o princípio de design de que o mascaramento fresco por estágio garante a segurança do pipeline inteiro sob o modelo de sondagem de primeira ordem.
Análise do Adams Bridge: O teorema explica a falha do acelerador Adams Bridge: como ele não injeta máscaras frescas entre os estágios (rounds 1 a 3), a hipótese do teorema de composição é violada, e a garantia de segurança não se aplica.

4. Resultados Chave

Prova Formal de Composição: Primeira prova verificada por máquina de que estágios de borboleta aritmética individualmente seguros compõem um pipeline seguro, desde que haja renovação de máscara fresca.
Refutação de Propriedade Intuitiva: Demonstração formal de que a verificação de "independência de valor pontual" é um falso positivo para borboletas, prevenindo que engenheiros rejeitem designs corretos ou ignorem falhas reais em gadgets não lineares.
Validação Universal: As provas não dependem de $q$ ser primo, cobrindo ML-KEM, ML-DSA e potenciais futuros padrões.
Explicação Arquitetural: Identificação clara de que a insegurança do Adams Bridge é devido à violação do "Princípio de Mascaramento Fresco", e não apenas a falhas de implementação de baixo nível.

5. Significado e Impacto

Para Certificação FIPS: O trabalho fornece evidências verificadas por máquina que engenheiros de hardware podem citar diretamente na documentação de certificação FIPS 140-3 para aceleradores PQC.
Preenchimento de Lacuna Teórica: Preenche a lacuna entre a teoria abstrata de composição (ISW) e a implementação prática de NTT aritmético, que anteriormente não tinha formalização específica.
Distinção entre Linear e Não-Linear: O artigo destaca que a composição para a borboleta (operacão afim/linear) é "fácil" e direta, enquanto a composição para gadgets não lineares (como redução de Barrett e multiplicadores mascarados) permanece um desafio aberto (abordado em trabalhos futuros e no Paper 3/5 da série).
Guia de Design: Estabelece o "Princípio de Mascaramento Fresco" como uma regra obrigatória para implementações seguras de pipelines de NTT, explicando por que otimizações que reutilizam máscaras entre estágios (como no Adams Bridge) comprometem a segurança.

Em resumo, este artigo transforma a segurança de pipelines de NTT de uma questão de intuição e análise empírica para uma propriedade matematicamente provada e verificada por computador, fornecendo a base formal necessária para a implementação segura de criptografia pós-quântica em hardware.