Resumo Técnico: Testes de Desencapsulamento Verificáveis para KEMs Baseados em FO

Declaração do Problema

Os Mecanismos de Encapsulamento de Chave (KEMs) pós-quânticos baseados na transformação Fujisaki–Okamoto (FO) dependem de uma verificação de desencapsulamento crítica: o algoritmo deve descriptografar um texto cifrado, rederivar a aleatoriedade da criptografia, recomputar o texto cifrado e compará-lo ao recebido antes de derivar a chave compartilhada. Embora essa verificação seja crítica para a segurança, testes padrão de entrada-saída de caixa-preta (black-box) frequentemente falham em detectar falhas específicas de implementação. Uma implementação pode omitir partes da computação de reencriptação ou alterar a lógica de seleção de ramos e, ainda assim, retornar a chave compartilhada esperada em textos cifrados gerados honestamente, efetivamente contornando a verificação de segurança sem disparar uma falha em um ambiente de teste padrão.

O artigo aborda a questão do que pode ser formalmente certificado sobre a execução dessas verificações de desencapsulamento usando testes de caixa-preta, especificamente quando o KEM é aumentado com códigos de confirmação.

Metodologia e Modelo

Os autores propõem uma teoria formal de desencapsulamento FO aumentado por código de confirmação testado sob um harness de referência honesta.

A Construção Aumentada

O modelo estende os KEMs baseados em FO padrão introduzindo uma testemunha de confirmação oculta $W$ na derivação da chave final.

1. Encapsulamento: Gera um texto cifrado e um valor de confirmação interno $W$. A chave final $K$ é derivada como $K = G_K(\langle \text{good}, B, W \rangle)$, onde $B$ é um prefixo de transcrição localizado e $G_K$ é um oráculo aleatório.
2. Desencapsulamento: Recomputa o texto cifrado e a testemunha de confirmação $W'$. A chave final é derivada apenas se $W' = W$.
3. Harness de Referência Honesta: O harness de teste fornece a entrada de desencapsulamento (texto cifrado, chaves), mas retém a testemunha oculta $W$ e a chave final $K$. O SUT (Sistema Sob Teste) deve consultar o oráculo aleatório $G_K$ com a tupla correta $\langle \text{good}, B, W \rangle$ para produzir a chave correta.

Estrutura Teórica

O artigo define uma lista de consultas de chave final localizada $Q_G(B)$, representando o conjunto de testemunhas candidatas que o SUT consulta contra o oráculo aleatório. O núcleo da metodologia é limitar a probabilidade de um SUT defeituoso passar no teste (ou seja, produzir a chave correta) analisando a probabilidade de um "acerto de lista" (list-hit)—o evento em que a testemunha oculta $W$ está em $Q_G(B)$.

A análise distingue entre:

• Teste de Referência Honesta: Comparando o SUT contra um par íntegro e gerado por referência.
• Teste de Si Mesmo Honesto: Comparando o SUT contra si mesmo (encapsulamento e desencapsulamento ambos provenientes do SUT).
• Cones de Dependência: Identificando o conjunto de operações que realmente influenciam o vetor alvo observável (a transcrição e a chave final).

Principais Contribuições

1. Teorema de Detectabilidade de Acerto de Lista Estrito

O resultado central (Teorema 5.1) estabelece que, para qualquer SUT $q$-localizado, a probabilidade de aprovação sob um harness de referência honesta é limitada por:
$$\text{Pass} \leq \delta_{\Pi_C} + \epsilon_{\text{alias}} + \epsilon_{\text{fresh}} + \Pr[W \in Q_G(B)] + 2^{-\kappa}$$
Onde:

• $\delta_{\Pi_C}$ é o erro de correção honesta.
• $\epsilon_{\text{alias}}$ contabiliza o aliasing adversário (colisões na codificação da chave final).
• $\epsilon_{\text{fresh}}$ contabiliza defeitos de frescor da chave final (vazamento do ponto oculto).
• $\Pr[W \in Q_G(B)]$ é o termo de acerto de lista, representando a probabilidade de o SUT adivinhar a testemunha oculta.
• $2^{-\kappa}$ é o termo de coincidência do oráculo aleatório.

O artigo prova que este limite é estrito (Teorema 5.2): qualquer preditor de $W$ a partir da visão do SUT induz um SUT de uma única consulta com uma probabilidade de aprovação que corresponde à taxa de sucesso do preditor. Assim, o termo de acerto de lista é a obstrução fundamental medida pelo harness.

2. Duas Rotas para Limitar o Termo de Acerto de Lista

O artigo fornece dois métodos distintos para limitar o termo de acerto de lista inevitável:

• Rota de Segurança de Fonte (cUP-fiel): Se o harness for "cUP-fiel" (fiel ao jogo de imprevisibilidade do código de confirmação da fonte), a probabilidade de acerto de lista é limitada por $q \cdot \epsilon_{\text{cUP}}$, onde $\epsilon_{\text{cUP}}$ é a vantagem de um adversário de candidato único no jogo da fonte. Isso transfere as provas de segurança da fonte para o contexto de teste com uma perda linear no número de consultas.
• Rota Entrópica: Se a testemunha $W$ possui entropia mínima condicional média $\lambda$ dada a visão do SUT, a probabilidade de acerto de lista é limitada por $q \cdot 2^{-\lambda}$. Esta rota acomoda códigos de diagnóstico (ex: hashes truncados) onde os limites de cUP da fonte podem não se aplicar diretamente.

3. Limite Inferior do Cone de Dependência (Resultado Negativo)

O artigo prova uma limitação fundamental na certificação de caixa-preta (Teorema 5.37). Se uma operação reside fora do cone de dependência de suporte ativo do alvo observável de confirmação (ou seja, mudar essa operação não altera a transcrição observável ou a chave final sob suporte honesto), então nenhum teste de referência honesta de caixa-preta pode certificar sua execução sobre uma classe de implementação contendo a correspondente "supressão" (uma versão do código que pula a operação).

• Para tais operações, os erros de integridade ($\alpha$) e completude ($\beta$) de qualquer certificador satisfazem $\alpha + \beta \geq 1$.
• Isso implica que, sem instrumentação adicional, entradas malformadas ou um conjunto de alvos maior, testes de caixa-preta não podem distinguir entre a execução correta e a supressão de operações fora do cone.

4. Instanciações e Artefato

A teoria é instanciada em duas famílias:

• ML-KEM (FIPS 203): Analisa a linha de código de confirmação da fonte (usando coeficientes não comprimidos selecionados) e uma variante de artefato de diagnóstico (ML-KEM-CD1) usando um código de hash de um byte.
• HQC (Especificação de Agosto de 2025): Analisa variantes de FO com sal que derivam o código de confirmação a partir da cauda de truncamento do texto cifrado. O artigo define HQC-TailEnt, uma suposição necessária para limitar o termo de acerto de lista para esses códigos derivados de cauda.

Os autores fornecem o FO-FaultBench, um artefato reproduzível contendo:

• Baselines fixos (mlkem-native, HQC Agosto 2025).
• Variantes transformadas (VSFO/CD1, CD*).
• Catálogos de mutantes (falhas de vinculação, falhas de decisão, falhas simétricas).
• Registros JSONL congelados de execuções experimentais.

Resultados Experimentais

As campanhas do artefato validam as afirmações teóricas:

• Falhas de Vinculação (Binding Faults): Falhas que omitem ou sobrescrevem o código de confirmação são detectadas sob teste de referência honesta, pois alteram a entrada da chave final.
• Falhas de Apenas Decisão (Decision-Only Faults): Falhas que afetam apenas a seleção de ramos (ex: sempre selecionando a chave boa) não são detectadas em textos cifrados honestos, mas são detectadas sob harnesses malformados ou diferenciais. Isso confirma a limitação de coincidência de suporte.
• Falhas Simétricas: Falhas aplicadas tanto ao encapsulamento quanto ao desencapsulamento passam em autotestes, mas falham em testes de referência honesta, demonstrando a necessidade do modelo de par.
• Adivinhação Probabilística: Mutantes que adivinham o código de confirmação passam com uma probabilidade que escala com o comprimento do código retido ($2^{-L}$), correspondendo aos limites teóricos de entropia.
• Orçamentos de Intervalo (Range Budgets): Experimentos em variantes HQC (CD1 vs. CD*) mostram que aumentar os bits da cauda retida (de 5 para 37 bits) reduz significamente a probabilidade de aprovação de mutantes de adivinhação, validando a rota entrópica.

Significância e Alegações

O artigo alega fornecer uma teoria formal de teste de código de confirmação que delineia precisamente o que os testes de caixa-preta podem e não podem certificar para KEMs baseados em FO.

• Alegações Positivas: O artigo estabelece que o vínculo do código de confirmação cria um sinal detectável para falhas de reencriptação, desde que o termo de acerto de lista seja limitado pela cUP da fonte ou pela entropia condicional. Oferece um framework rigoroso para interpretar resultados de testes como evidência para classes específicas de falhas.
• Alegações Negativas: O artigo afirma explicitamente que o teste de referência honesta de caixa-preta possui limites inerentes. Ele não pode certificar operações fora do cone de dependência (ex: execução completa da reencriptação se apenas um subconjunto de coeficientes for vinculado) sem alterar o alvo do harness ou adicionar instrumentação.
• Modéstia: Os autores enfatizam que os teoremas de teste são afirmações clássicas do Modelo de Oráculo Aleatório (ROM). Eles não reprovam a segurança IND-CCA dos KEMs subjacentes, mas baseiam-se em análises de fonte citadas para a segurança da construção. A "segurança" das linhas aumentadas é herdada da fonte; a contribuição do artigo é o sinal de teste e a interpretação das probabilidades de aprovação sob configurações específicas de harness.

O trabalho serve como uma ponte entre jogos de segurança teóricos (cUP, fCOR) e o teste de implementação prática, fornecendo uma "gramática de alegação" para interpretar resultados experimentais em implementações de KEM pós-quânticos.