Resumo Técnico: GCD: Garbled, Corrected, Demonstrandum

Declaração do Problema

O artigo aborda a correção e a verificação da implementação do Algoritmo de Euclides Estendido (GCD Estendido) dentro da biblioteca padrão do Go (crypto/internal/fips140/bigmod). Esta implementação é crítica para a geração de pares de chaves RSA, um componente fundamental para TLS, SSH e PGP. A implementação em Go foi introduzida no Go 1.24 para suportar nativamente a conformidade com o FIPS 140-3, substituindo a dependência do BoringSSL.

Os autores identificaram uma discrepância crítica: embora o código Go tenha sido alegado como um port direto da implementação do BoringSSL (que é formalmente verificada via assistente de prova Rocq através do Fiat Cryptography), a versão em Go continha desvios sutis. Esses desvios não foram detectados por três revisões de código distintas. Os desvios quebraram os invariantes matemáticos do algoritmo, potencialmente comprometendo a correção do cálculo do inverso modular necessário para chaves privadas RSA. Além disso, a implementação em Go permitiu um domínio de entrada maior do que a versão comprovada do BoringSSL, invalidando as suposições da prova existente.

Metodologia

Os autores empregaram uma abordagem de verificação de programas dedutiva usando o Gobra, um verificador baseado em lógica de separação para Go. A metodologia envolveu:

1. Especificação Formal: Os autores formalizaram as especificações de linguagem natural das funções Go (extendedGCD, InverseVarTime, GCDVarTime) em especificações Gobra, incluindo pré-condições, pós-condições e invariantes de loop.
2. Análise de Desvio: Ao tentar verificar o código Go existente contra as especificações derivadas da prova do BoringSSL, os autores identificaram duas classes principais de desvios:
   • Subtrações Não Sincronizadas: A implementação em Go atualizava os coeficientes de Bézout ($A, B, C, D$) independentemente com base em condições locais, enquanto a implementação de referência exigia reduções sincronizadas para manter os invariantes de loop.
   • Expansão do Domínio de Entrada: A implementação em Go permitia entradas onde $a \ge n$, violando a pré-condição $a < n$ exigida pela prova original.
3. Construção da Prova:
   • Correção de Código: Os autores propuseram uma correção para as subtrações não sincronizadas para alinhar a lógica do Go com os invariantes matemáticos.
   • Adaptação da Prova: Eles portaram a prova existente do BoringSSL de Rocq para o Gobra. Para o desvio do domínio de entrada, eles relaxaram os invariantes e pós-condições para cobrir o caso onde $a \ge n$, provando que o valor do GCD permanece correto mesmo se a propriedade do inverso modular não se mantiver nesse caso específico.
   • Verificação Híbrida: Para lemas de aritmética não linear que o solver SMT Z3 (usado pelo Gobra) não conseguia lidar, os autores usaram o assistente de prova Lean para provar lemas fundamentais e os importaram para o Gobra como lemas trusted (confiáveis).
4. Verificação Assistida por IA: Os autores utilizaram um agente de IA (Claude Code da Anthropic) para refinar iterativamente invariantes e lemas com base nas mensagens de erro do Gobra, reduzindo significamente o esforço manual no processo de construção da prova.

Principas Contribuições

• Descoberta de Bugs: O artigo revela dois desvios sutis, mas críticos, na implementação do Extended GCD em Go que quebram os invariantes algorítmicos. Esses bugs estavam presentes em um código que passou por múltiplas revisões e que era alegado ser um port direto de uma implementação verificada.
• Otimização de Desempenho: A correção proposta para o desvio de subtração não sincronizada não apenas restaura a correção, mas também resulta em um aceleração média de 24% (média geométrica) ao eliminar alocações de memória desnecessárias e operações redundantes no corpo do loop.
• Verificação Formal de Crypto em Go: Os autores verificaram com sucesso a implementação corrigida, sua terminação e sua correção contra especificações formais usando o Gobra. Esta é a primeira verificação formal deste componente específico na biblioteca padrão do Go.
• Portabilidade e Generalização de Prova: Eles portaram com sucesso uma prova de Rocq (Fiat Cryptography) para o Gobra e a generalizaram para cobrir o domínio de entrada mais amplo permitido pela implementação em Go.
• IA na Verificação: O trabalho demonstra a eficácia dos agentes de IA em facilitar a verificação formal ao iterar autonomamente sobre especificações e identificar as causas raiz das falhas de prova (por exemplo, sugerindo que a redução independente de coeficientes era o problema).

Resultados

• Corretude: A implementação corrigida foi verificada com sucesso em 16,9 segundos em um laptop padrão. A verificação cobre a função extendedGCD e seus clientes InverseVarTime e GCDVarTime.
• Desempenho: Benchmarks em vários tamanhos de limbs (64 a 8192 bits) mostraram que a implementação verificada é consistentemente mais rápida que a original. A aceleração média foi de 23,98%, com melhorias variando de 15,6% a 36% dependendo do tamanho da entrada. A aceleração é atribuída a atualizações in-place e à eliminação de alocações de buffers intermediários.
• Divulgação e Impacto: Os autores divulgaram os desvios aos mantenedores de criptografia do Go. Os mantenedores confirmaram que, embora os desvios pudessem teoricamente levar a inversos modulares incorretos, verificações defensivas no código de geração de chaves RSA capturariam esses erros e retornariam um erro em vez de uma chave incorreta, limitando o impacto à disponibilidade em vez de um comprometimento de segurança. As correções estão sob revisão para inclusão na biblioteca padrão do Go.
• Integração Contínua: Devido ao rápido tempo de verificação, a prova foi integrada ao fluxo de trabalho de Integração Contínua (CI) do projeto para verificar automaticamente quaisquer desvios futuros.

Significância e Alegações

O artigo afirma que seu trabalho destaca três percepções primárias:

1. Bugs Sutis em Código Revisado: Mesmo códigos bem revisados, especialmente quando alegados como um port direto de uma implementação verificada, podem conter bugs sutis que quebram invariantes.
2. Poder da Verificação Formal: A verificação formal é uma ferramenta poderosa para descobrir esses tipos de bugs que testes e revisão manual podem perder.
3. Papel dos Agentes de IA: Agentes de IA podem facilitar efetivamente o processo de verificação ao refinar iterativamente invariantes e lemas com base no feedback do verificador, embora a supervisão humana permaneça necessária para a limpeza final e compreensão estrutural.

Os autores enfatizam que seu trabalho fecha a lacuna entre a implementação e sua prova. Ao verificar o código Go diretamente, em vez de depender da existência de uma prova para uma implementação diferente (BoringSSL), eles garantem que o código específico rodando em produção é matematicamente sólido. Eles também observam que, embora dependam de funções trusted para operações de baixo nível de bits, o argumento de corretude global é decomposto em componentes pequenos e revisáveis, aumentando a confiança na confiabilidade do sistema.