Dependency-Aware ROM/CBD Correctness Bounds for ML-KEM-768 at the Heuristic Failure Scale

No mundo digital, a segurança muitas vezes depende de problemas matemáticos que são fáceis de usar em uma direção, mas extremamente difíceis de inverter sem a informação secreta correta. O ML-KEM é um mecanismo de estabelecimento de chaves pós-quânticas projetado para permanecer seguro mesmo contra futuros computadores quânticos. Como outros sistemas criptográficos baseados em redes (lattice-based), ele possui uma probabilidade extremamente pequena do que é chamado de falha de encapsulamento honesto: mesmo quando ambas as partes se comportam corretamente, os dois lados poderiam, em princípio, derivar chaves diferentes. Estimar a raridade com que isso pode acontecer é uma questão importante de correção. Análises anteriores basearam-se amplamente em estimativas heurísticas da escala de falha, enquanto a obtenção de um limite rigoroso que preserve as dependências matemáticas relevantes entre os diferentes termos de erro é substancialmente mais difícil.

Um novo estudo de Aurélie Duriez e Christophe Tommasini aborda este problema desenvolvendo uma análise matemática rigorosa do ML-KEM-768 dentro de uma abstração explícita de função aleatória idealizada / binomial centrada, ou ROM/CBD. O trabalho não é uma simulação e não tenta calcular a taxa de falha exata. Em vez disso, os autores derivam um limite superior certificado para a probabilidade de uma falha de encapsulamento honesto, preservando as dependências importantes entre os diferentes termos de erro. Em particular, a análise rastreia as dependências induzidas pela matriz pública e por ambos os termos de compressão de texto cifrado, em vez de simplesmente tratá-los como independentes. O limite superior certificado resultante é menor que um em 2 elevado à potência de 164,81.

Esta descoberta é significativa porque substitui uma estimativa heurística da escala de falha, dentro do modelo explícito estudado, por um limite superior certificado que considera as dependências. A análise não assume simplesmente que os erros relevantes são independentes; ela preserva as dependências matemáticas que surgem entre eles. O limite certificado atinge essencialmente a mesma escala que as estimativas heurísticas anteriores, mas isso não deve ser interpretado como uma prova de que essas estimativas são a probabilidade de falha exata. O resultado é deliberadamente mais restrito: dentro da abstração ROM/CBD explícita estudada no artigo, a probabilidade de uma falha de encapsulamento honesto é rigorosamente limitada por um valor extremamente pequeno. O artigo também deixa claro que esta não é uma taxa de falha de encapsulamento exata e não é uma afirmação de teoria da informação sobre a instanciação fixa de SHAKE do FIPS 203.

O trabalho exigiu uma abordagem diferente para o problema. Análises heurísticas simplificadas podem se tornar muito mais fáceis se alguns termos de erro forem tratados como independentes, mas a estrutura algébrica real cria dependências que uma análise rigorosa deve preservar. Os autores, portanto, desenvolveram um método que segue essas dependências através do cálculo em vez de descartá-las. O processo de pesquisa também utilizou uma metodologia assistida por IA para explorar abordagens candidatas, identificar casos críticos e estruturar a análise. Este uso exploratório de IA foi combinado com verificações exaustivas verificadas por computador, aritmética exata ou certificada e computações verificáveis de forma independente para fechar as partes mais difíceis do argumento. As afirmações matemáticas finais, portanto, baseiam-se em evidências explícitas e reproduzíveis, em vez de no próprio resultado da IA.

O resultado é um limite de correção certificado, rigoroso e transparente dentro da abstração declarada. Os pesquisadores disponibilizaram seu código, dados e artefatos de suporte para que os cálculos possam ser verificados de forma independente. Este nível de reprodutibilidade é particularmente importante na criptografia, onde as afirmações matemáticas devem estar abertas à verificação independente. O estudo mostra que, dentro da abstração ROM/CBD explícita considerada, a probabilidade de uma falha de encapsulamento honesto é limitada em um nível extremamente pequeno. No entanto, isso não deve ser interpretado como um certificado geral de segurança para o ML-KEM-768, como uma prova de todas as propriedades de segurança do esquema padronizado, ou como uma afirmação que cubra cada implementação de hardware ou software.

Este resultado avança a compreensão rigorosa de um aspecto específico da correção do ML-KEM-768, passando de uma estimativa heurística da escala de falha para um limite superior certificado que considera as dependências dentro de uma abstração claramente definida. Ele mostra que um limite na escala heurística ainda pode ser estabelecido enquanto se preservam dependências importantes entre os termos de erro relevantes. O número 164,81 é o expoente certificado deste limite superior: dentro da abstração ROM/CBD declarada, a probabilidade de falha de encapsulamento honesto é limitada acima por 2 elevado à potência de -164,81. Este número deve, portanto, ser entendido como uma propriedade precisa do limite certificado provado no artigo, em vez de uma medida geral da segurança ou robustez do ML-KEM-768 como um todo.

Os pesquisadores também tiveram o cuidado de explicar os limites de seu trabalho. Eles observaram que sua prova se aplica a uma abstração específica do sistema, não necessariamente a todas as implementações possíveis do software. Eles não alegaram ter resolvido o problema para todas as variações do padrão de criptografia, nem sugeriram que o sistema seja imune a todos os tipos de ataques. O foco deles foi estritamente a correção do processo de descriptografia sob condições honestas. Ao serem claros sobre o que provaram e o que não provaram, garantiram que suas descobertas não fossem interpretadas erroneamente. O estudo serve como um testemunho do poder da análise cuidadosa e detalhada em um campo onde pequenos erros podem ter consequências enormes. Mostra que, com rigor suficiente e as ferramentas certas, até os sistemas matemáticos mais complexos podem ser compreendidos e verificados.

No fim, o artigo entrega um resultado preciso, mas deliberadamente delimitado: dentro da abstração ROM/CBD declarada, a probabilidade de falha de encapsulamento honesto é rigorosamente limitada acima por 2 elevado à potência de -164,81. Este é um limite superior certificado extremamente pequeno, mas não é uma taxa de falha exata e não é uma prova abrangente de que o sistema ML-KEM-768 completo implantado funcionará sem falhas sob todas as condições do mundo real. A contribuição reside em substituir uma estimativa heurística da escala de falha por um limite que considera as dependências, que é reproduzível e verificável de forma independente dentro de um modelo claramente definido. Sua força não vem de alegar certeza além desse modelo, mas de ser explícito tanto sobre o que foi provado quanto sobre o que permanece fora do escopo do resultado.