A Microsoft está a usar Agentes de IA para Provar Matematicamente que o seu Código de Encriptação Não Tem Falhas

Pontos-chave

• A biblioteca SymCrypt da Microsoft, o motor de criptografia utilizado no Windows e Azure, está a ser formalmente verificada usando uma cadeia de ferramentas que combina Rust, Lean e Aeneas desde meados de 2024.
• Os primeiros algoritmos verificados lançados são SHA-3, um padrão para criar impressões digitais matemáticas de dados, e ML-KEM, um esquema de encriptação pós-quântica concebido para resistir a ataques de futuros computadores quânticos.
• Agentes de IA, software que consegue executar tarefas multi-passos autonomamente, estão a escrever passos de prova matemática que engenheiros humanos revisam e verificam independentemente.
• A Microsoft disponibilizou em código aberto o código verificado, especificações e provas num ramo público do SymCrypt, tornando o trabalho disponível para revisão externa.
• Os algoritmos futuros planeados para o mesmo tratamento incluem AES-GCM, FrodoKEM e ML-DSA, todos os quais protegem dados no Windows e Linux atualmente.

Código criptográfico, o software que encripta e protege dados em todas as aplicações, navegadores e sistemas operativos, é notoriamente implacável. Uma simples verificação de limites omitida, significando uma falha em confirmar que um número se mantém num intervalo seguro, pode quebrar segurança que aparenta ser sólida à primeira vista. Testes apanham muitos erros. Não apanham todos.

A Microsoft Research tem estado a trabalhar numa abordagem diferente: provar que o código está correto, matematicamente, antes de ser lançado.

O projeto centra-se na SymCrypt, a biblioteca criptográfica de código aberto da Microsoft que funciona dentro do Windows e Azure Linux. Os engenheiros estão agora a escrever novos algoritmos criptográficos em Rust, uma linguagem de programação que exclui famílias inteiras de erros de segurança de memória por design. Depois executam esses programas Rust através de uma ferramenta chamada Aeneas, que traduz o código numa forma que um assistente de prova chamado Lean consegue analisar.

Lean não é um chatbot. É um framework de prova formal, software que verifica argumentos matemáticos da forma como uma calculadora verifica aritmética, exceto que verifica provas, e nunca comete erros aritméticos.

O objetivo é produzir um teorema: para cada entrada válida, esta implementação retorna exatamente o resultado que o padrão publicado diz que deve retornar. Não habitualmente. Sempre.

O primeiro lançamento público abrange SHA-3, um algoritmo padrão para criar uma impressão digital única de qualquer peça de dados, e ML-KEM, um esquema de troca de chaves pós-quântica. Criptografia pós-quântica significa algoritmos construídos para permanecer seguros mesmo contra computadores quânticos, máquinas que poderiam quebrar muitos dos métodos de encriptação atuais.

Como é que a IA se encaixa numa prova matemática?

Escrever provas formais é lento. É aqui que entram os agentes de IA.

Os agentes lidam com os passos intermediários repetitivos, redigindo fragmentos de prova que ligam resultados intermédios. Engenheiros humanos focam-se nas partes que requerem julgamento real: verificar que a especificação formal realmente corresponde ao que o padrão publicado diz, e revisar as propriedades de alto nível que o código deve satisfazer. A verificação de prova em si é totalmente automatizada e determinística, o que significa que a máquina aceita ou rejeita a prova. Não há espaço para o agente inventar.

A Microsoft descreve isto como uma divisão clara: agentes escrevem, humanos revisam, o verificador de provas decide.

Para pessoas que usam Windows, Azure, ou qualquer serviço que dependa da pilha de segurança da Microsoft, o significado prático é direto. A encriptação que protege seus ficheiros, seus dados em nuvem e seus inícios de sessão está a ser mantida a um padrão mais elevado do que apenas testes conseguem fornecer. Se as provas passarem, o código faz exatamente aquilo que o padrão exige.

O ramo disponibilizado em código aberto permite que investigadores externos inspecionem tanto o código Rust como as provas lado a lado, por isso as afirmações não são apenas a palavra da Microsoft.

Fique atento a: anúncios de construções formalmente verificadas chegando aos lançamentos estáveis do Windows, e se outras bibliotecas de criptografia adotam fluxos de trabalho de prova assistidos por IA semelhantes. Isso marcaria uma mudança real em como a indústria pensa sobre correção de software.