💻 computer science

Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

O artigo apresenta uma hierarquia de verificação de quatro estágios que estende a análise de mascaramento de primeira ordem a módulos aritméticos de produção, permitindo a validação pré-silício de aceleradores criptográficos pós-quânticos em larga escala (como o módulo ML-KEM de 1,17 milhão de células) ao reduzir drasticamente o escopo da revisão manual para um conjunto gerenciável de candidatos inseguros com certificação matemática.

Autores originais: Ray Iskander, Khaled Kirah

Publicado 2026-04-17

📖 5 min de leitura🧠 Leitura aprofundada

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 cofre digital ultra-seguro para proteger segredos contra futuros computadores quânticos. Esse cofre é feito de milhões de peças de metal (circuitos eletrônicos). O problema é que, mesmo que o cofre pareça forte, um espião pode tentar roubá-lo não quebrando a porta, mas ouvindo o som que as peças fazem quando se movem (o consumo de energia).

Para evitar isso, os engenheiros usam uma técnica chamada "Mascaramento". É como se, em vez de usar uma única chave para abrir o cofre, eles dividissem a chave em duas metades aleatórias. Nenhuma metade sozinha revela nada; apenas juntas elas formam a chave. Se o espião ouvir apenas uma metade, ele não aprende nada.

O artigo que você pediu para explicar trata de um novo "super-detetive" chamado QANARY (inspirado nos pássaros canários que mineradores usavam para detectar gás venenoso). Esse detetive verifica, antes mesmo de o cofre ser fabricado, se as metades da chave estão realmente separadas ou se, por algum erro de projeto, elas se encontram e se misturam, permitindo que o espião as ouça juntas.

Aqui está a explicação passo a passo, usando analogias do dia a dia:

1. O Problema: O Labirinto Gigante

O projeto analisado (Adams Bridge) é um acelerador de criptografia com 1,17 milhão de peças (células).

A analogia: Imagine tentar encontrar se duas pessoas que estão separadas em um estádio de futebol gigante se encontraram em algum lugar.
O desafio: As ferramentas antigas de verificação eram como lupas muito precisas, mas que só conseguiam olhar para um pequeno grupo de 5.000 pessoas de cada vez. Elas eram excelentes, mas não conseguiam escanear o estádio inteiro. Se você tentasse usar a lupa no estádio inteiro, ela quebraria ou levaria anos.

2. A Solução: O Detetive QANARY

Os autores criaram um sistema de quatro etapas para escanear o estádio inteiro rapidamente e com segurança.

Etapa 1: O Rastreador de Estradas (Análise Estrutural D0/D1)

Como funciona: Em vez de olhar para cada pessoa, o detetive olha apenas para o mapa das estradas. Ele pergunta: "Existe algum caminho que conecta a 'Metade A' da chave com a 'Metade B'?"
A analogia: Se você vê uma estrada que liga o setor norte ao setor sul, o detetive levanta a mão e grita: "ALERTA! Elas podem se encontrar aqui!"
O resultado: Isso é muito rápido (segundos para o estádio todo). Mas é um pouco "paranoico". Às vezes, ele grita alerta porque há uma estrada, mesmo que ninguém esteja realmente usando essa estrada naquele momento. Isso gera muitos "falsos positivos" (avisos desnecessários).

Etapa 2: O Relógio de Multi-Ciclo (MC-D1)

O problema: Às vezes, as metades da chave se separam em um momento, cruzam um registro (como um portão de segurança) e se encontram no próximo momento. O rastreador de estradas simples não vê isso.
A solução: O QANARY agora olha para o tempo. Ele simula o movimento das peças ao longo de vários segundos.
O resultado: Ele descobre que 12 módulos que pareciam seguros na verdade tinham "armadilhas" onde as metades se encontravam após cruzarem o portão. Ele reclassifica esses módulos como "suspeitos".

Etapa 3 e 4: O Detetive Matemático (SADC)

Aqui está a mágica. O QANARY pega os milhares de alertas da Etapa 1 e 2 e usa matemática avançada para dizer: "Espera aí, essa estrada existe, mas ninguém está usando porque a chave foi trocada por uma nova aleatória antes de chegar lá."

A analogia: Imagine que o detetive vê duas pessoas caminhando em direção uma à outra. Ele grita "ALERTA!". Mas, ao olhar mais de perto, ele vê que uma delas trocou de roupa e de nome no meio do caminho, tornando impossível saber quem elas são.
O que acontece:
- Ele verifica cada alerta matematicamente.
- No módulo de teste (Barrett Reduction), havia 363 alertas.
- O QANARY conseguiu provar matematicamente que 198 deles eram falsos alarmes (seguros).
- Ele isolou 165 que realmente precisavam de atenção do engenheiro.
- 0 ficaram sem resposta. Tudo foi classificado.

3. Por que isso é importante?

Antes dessa ferramenta, um engenheiro teria que olhar manualmente para 363 fios suspeitos em um chip gigante, o que levaria semanas e seria propenso a erros.

Com o QANARY: O engenheiro recebe um relatório em 3 minutos que diz: "Aqui estão 198 certificados de segurança (pode ignorar) e aqui estão 165 locais que você precisa verificar com cuidado".
Validação Dupla: Para ter certeza absoluta de que o detetive não está alucinando, eles usaram dois "juízes" de computador diferentes (Z3 e CVC5). Os dois juízes concordaram em todos os 363 casos. Zero erros.

4. Conclusão Simples

Este artigo apresenta uma ferramenta que permite verificar a segurança de chips de criptografia quântica antes de eles serem fabricados.

Velocidade: Faz o trabalho de meses em minutos.
Precisão: Usa uma abordagem de "peneira grossa" (rápida) seguida de "peneira fina" (matemática) para não deixar passar nada e não gastar tempo com falsos alarmes.
Segurança: Garante que, mesmo com computadores quânticos no futuro, nossos segredos digitais não serão roubados por espiões que apenas "ouvem" o consumo de energia dos chips.

Em resumo: O QANARY é o canário moderno que avisa se o gás (a vulnerabilidade) está vazando no cofre, permitindo que os engenheiros consertem o problema antes que o cofre seja construído, economizando tempo, dinheiro e garantindo a segurança do futuro.

Resumo Técnico: Análise de Dependência Estrutural para Hardware NTT Mascaramento

1. O Problema

A certificação de aceleradores de criptografia pós-quântica (PQC), como ML-KEM e ML-DSA (padrões FIPS 203 e 204), exige evidências robustas de resistência a canais laterais (Side-Channel Analysis - SCA). O mascaramento (masking) é a contramedida dominante, dividindo segredos em múltiplas partes aleatórias (shares). A segurança depende da invariância de que nenhum caminho lógico combinacional deve permitir que duas ou mais partes do mesmo segredo converjam, pois tal recombinação cria uma função observável do segredo.

No entanto, existem desafios significativos na verificação em escala:

Limitação de Ferramentas Exatas: Ferramentas de verificação formal existentes (como SILVER, Prover, Coco-Alma) são precisas, mas não escalam além de alguns milhares de células (gadgets). Elas falham em designs de produção com milhões de células.
Complexidade de Hardware PQC: A criptografia baseada em retículos (Lattice-based) utiliza Transformadas Numéricas Teóricas (NTT) com aritmética modular em grandes campos. Isso exige mascaramento aritmético (soma módulo $q$ ) em vez de booleano (XOR), combinado com pipelines profundos.
Caminhos Multiciclo: Mesmo que as partes estejam separadas em um único ciclo de relógio, registros de pipeline e lógica de encaminhamento podem criar caminhos de dependência multiciclo que reúnem partes do segredo após vários estágios, invisíveis para análises de ciclo único.

2. Metodologia: QANARY e a Hierarquia de Verificação

Os autores apresentam o QANARY (Quantum Canary), uma ferramenta de verificação de dependência estrutural projetada para hardware de grande escala. O método baseia-se em uma condição necessária (mas não suficiente) para segurança de primeira ordem: a não convergência estrutural das partes.

A metodologia emprega uma hierarquia de verificação de quatro estágios para refinar os resultados e reduzir falsos positivos:

Análise de Dependência Estrutural (D0/D1):
- Analisa se o "fan-in" combinacional de um fio depende de mais de uma parte do segredo.
- Utiliza um reticulado de rótulos $\{ \bot, S_0, S_1, BOTH \}$ . Se um fio depende de ambas as partes, é marcado como estruturalmente inseguro.
- Extensão Multiciclo (MC-D1): Estende a análise através de limites de registros (DFFs) usando propagação de rótulos em ponto fixo. Isso detecta convergências de partes que ocorrem em diferentes ciclos de relógio, invisíveis à análise de ciclo único.
Refinamento de Mascaramento Fresco (FM):
- Verifica se fios marcados como inseguros são re-mascarados por aleatoriedade fresca (fresh randomness) que atua como um "one-time pad" (bijetor). Se uma variável aleatória inverte o valor do fio independentemente das entradas, o fio é promovido para "seguro".
Verificação de Distância de Autenticação Booleana (Boolean SADC):
- Para fios que permanecem inseguros após o FM, aplica-se uma verificação de independência de valor.
- Reparametriza as partes do segredo ( $s_0, s_1$ ) em termos do segredo original ( $x$ ) e uma máscara independente.
- Usa solucionadores SMT (Z3) para verificar se o valor do fio muda quando o segredo muda, mantendo a máscara fixa.
Verificação de Distância de Autenticação Aritmética (Arithmetic SADC):
- Crucial para PQC, onde o mascaramento é modular ( $s = (s_0 + s_1) \mod q$ ).
- Realiza a reparametrização simbolicamente sobre a semântica modular, tratando as partes como vetores de bits completos e verificando a independência de valor sob aritmética modular.
- Validação Dual: Cada verificação aritmética é cruzada por dois solucionadores independentes (Z3 e CVC5) para garantir a ausência de erros de implementação.

3. Contribuições Principais

Verificação em Escala de Produção: A análise estrutural foi aplicada ao acelerador Adams Bridge (1,17 milhão de células, 30 módulos mascarados), completando a análise de ciclo único em 8,7 segundos.
Reclassificação Multiciclo (MC-D1): A extensão multiciclo reclassificou 12 módulos que pareciam "limpos" na análise de ciclo único como "marcados estruturalmente", revelando dependências cruzadas entre registros.
Hierarquia com SADC Aritmético: Na aplicação ao módulo de redução Barrett (5.543 células) do ML-KEM:
- A hierarquia verificou mecanicamente 198 dos 363 fios marcados (54,5%) como seguros de primeira ordem.
- Isolou 165 fios candidatos inseguros como um limite superior seguro para triagem do projetista.
- Não deixou nenhum fio indeterminado.
- Todas as 363 verificações foram validadas por Z3 e CVC5 com 0 discordâncias.
Infraestrutura de Reprodutibilidade: O pipeline é determinístico, com validação cruzada de solucionadores e um conjunto de provas formais (machine-checked) para a base algébrica do método.

4. Resultados Experimentais

Adams Bridge (1,17M células):
- A análise de ciclo único (SC-D1) identificou 59.061 fios inseguros em 8,7 segundos.
- A análise multiciclo (MC-D1) aumentou para 614.126 fios inseguros, mas comprimiu a triagem para 8.487 pontos de convergência reais (raiz do problema), eliminando 98,6% de artefatos de propagação.
- 12 módulos mudaram de "Limpo" para "Inseguro" devido à propagação multiciclo.
Módulo Barrett (ML-KEM):
- O pipeline de quatro estágios reduziu a carga de trabalho manual de 363 verificações para apenas 165 candidatos prioritários, fornecendo certificados de segurança matemática para a maioria dos fios.
- Tempo de execução: ~3 minutos em um único núcleo.
Benchmarks: No gadget de referência DOM AND (16 células), o pipeline eliminou 100% dos falsos positivos estruturais, confirmando a segurança conhecida do gadget.
Comparação com Ferramentas Existentes:
- Ferramentas exatas (Coco-Alma) não conseguem escalar para módulos completos de PQC (limitadas a ~2.300 células).
- O QANARY oferece cobertura exaustiva pré-silício, identificando padrões de recombinação de partes que foram confirmados por ataques de análise de potência em hardware real.

5. Significado e Impacto

Este trabalho preenche uma lacuna crítica na segurança de hardware pós-quântico:

Escalabilidade: Demonstra que é possível realizar verificação de segurança de primeira ordem em designs de hardware de produção (milhões de células) onde ferramentas formais exatas falham.
Pré-Silício: Permite a geração de evidências de segurança antes da fabricação do chip, essencial para a certificação FIPS 140-3.
Triagem Eficiente: Transforma uma revisão manual massiva (centenas de milhares de fios) em uma lista acionável e pequena de candidatos inseguros, com certificados matemáticos para os fios seguros.
Complementaridade: O método não substitui a verificação exata ou a análise empírica, mas atua como um filtro escalável que torna a verificação exata viável ao reduzir o espaço de busca para os componentes críticos.

Em suma, o artigo apresenta uma abordagem prática e matematicamente fundamentada para garantir a segurança de canais laterais em aceleradores de criptografia pós-quântica de grande escala, permitindo que a indústria avance na implementação de hardware seguro contra computadores quânticos.