Vitalik Buterin rejeita alegação de que IA condena cibersegurança

Buterin escreveu na sua publicação de 17 de setembro no X que discorda da visão cada vez mais comum de que “o hacking com IA significa que a cibersegurança está condenada”. Afirmou que as pessoas que continuam a deter criptomoedas estão implicitamente a apostar que os sistemas digitais seguros conseguem sobreviver a ataques automatizados mais fortes, acrescentando que cerca de 90% do seu próprio património líquido permanece em cripto.

O seu argumento centra-se na verificação formal, uma técnica que utiliza especificações matemáticas e provas para determinar se o software se comporta de acordo com propriedades predefinidas. Buterin usou a prova avançada de teoremas matemáticos como analogia, afirmando que uma IA suficientemente capaz poderia ajudar a provar que “este programa é seguro”, mesmo quando o próprio software é complexo.

Buterin afirma que a verificação formal pode favorecer os defensores

O argumento de Buterin não trata a segurança da IA como uma corrida em que os investigadores defensivos simplesmente encontram erros antes dos atacantes. A sua publicação descreve, em vez disso, um modelo em que os programadores definem as propriedades que um sistema deve satisfazer e depois usam ferramentas de prova automatizadas para estabelecer que a implementação as cumpre.

A própria documentação de verificação formal da Ethereum descreve a técnica em termos mais restritos. Refere que a verificação formal pode provar matematicamente que um contrato inteligente cumpre uma especificação formal, oferecendo garantias mais fortes do que os testes comuns para as propriedades incluídas nessa especificação.

A mesma documentação da Ethereum identifica uma limitação importante por trás dos comentários de Buterin. Uma prova estabelece que o software satisfaz a especificação que está a ser verificada; não prova automaticamente que os programadores definiram corretamente todas as propriedades de segurança. Especificações mal escolhidas ou incompletas podem deixar comportamentos fora da prova.

Buterin fez a mesma distinção na sua publicação. Argumentou que definir “segurança” de forma demasiado restrita pode omitir vetores de ataque que envolvem áreas como protocolos, servidores, bases de dados, camadas de rede, caches ou outros componentes de suporte. A sua direção proposta é, portanto, verificar mais do sistema completo em vez de rotular um pequeno grupo de módulos como críticos para a segurança.

Buterin já tinha descrito a verificação formal assistida por IA como uma possível “forma final” do desenvolvimento de software. Os seus comentários anteriores aplicavam a abordagem a áreas como o consenso da Ethereum, sistemas de conhecimento zero e criptografia resistente a computadores quânticos.

A Ethereum já está a testar segurança assistida por IA

Os investigadores da Ethereum já estão a usar IA no trabalho de segurança, embora os sistemas atuais ainda estejam longe da prova automática da segurança de todo o sistema.

A equipa de Segurança de Protocolo da Ethereum Foundation relatou em julho que agentes de IA coordenados encontraram defeitos reais em sistemas usados pela Ethereum. Uma descoberta confirmada envolveu uma falha remotamente acionável na implementação de rede Gossipsub do Rust libp2p.

A falha tornou-se a CVE-2026-34219. O registo da Base de Dados Nacional de Vulnerabilidades dos EUA indica que as versões anteriores à 0.49.4 podiam ser bloqueadas remotamente através de uma mensagem PRUNE criada que provocava um overflow aritmético durante o tratamento de backoff do Gossipsub. A versão 0.49.4 corrigiu o problema.

A equipa de segurança da Foundation afirmou que a descoberta de vulnerabilidades não era a parte mais difícil do fluxo de trabalho de IA. Os investigadores descobriram que os agentes de IA geravam frequentemente relatórios convincentes envolvendo caminhos de execução inalcançáveis, falhas apenas em modo de depuração ou provas formais que tecnicamente passavam, mas provavam uma propriedade mais fraca do que a pretendida.

A reprodução independente continuou a ser um requisito antes de a equipa aceitar uma descoberta. A Foundation afirmou que eram necessárias verificações automatizadas e revisão humana porque um agente podia produzir uma prova de aspeto válido que não conseguia restringir o comportamento do software que os investigadores realmente queriam testar.

A experiência da Foundation foi descrita como um problema de triagem: a IA podia gerar um grande número de vulnerabilidades candidatas, mas os investigadores ainda tinham de determinar se cada problema era alcançável e relevante em produção.

A verificação formal está a entrar no roteiro do protocolo da Ethereum

A Ethereum Foundation tornou separadamente a verificação formal parte do seu atual programa de investigação de protocolo. Na sua atualização de prioridades de protocolo de 7 de setembro, a Foundation afirmou que a verificação formal serviria como ferramenta transversal nas suas restantes áreas de investigação plurianuais. O documento cobre trabalho em privacidade, estado, desenvolvimento de zkEVM, segurança pós-quântica e outros componentes do protocolo até 2029.

O mesmo roteiro refere que se espera que o desenvolvimento de um zkEVM de L1 avance as ferramentas de verificação formal, os fluxos de trabalho e os componentes criptográficos verificados. Os investigadores da Ethereum estão a trabalhar para um sistema em que os validadores eventualmente verifiquem provas de execução sucintas em vez de reexecutarem independentemente cada bloco.

Um projeto separado da Ethereum Foundation lançado em agosto já está a combinar agentes de IA com provas verificadas por máquina. O projeto better.codes permite que os investigadores direcionem sistemas de IA para um problema de solidez criptográfica formalizado em Lean, enquanto o núcleo Lean verifica se as provas submetidas satisfazem uma declaração de teorema fixa.

O relatório de financiamento do segundo trimestre da Foundation lista mais trabalho que combina modelos de linguagem de grande dimensão com métodos formais. Os projetos incluem o ETHeorem para verificar implementações de clientes Ethereum em relação a especificações, o SPECA e o LeanAgent para trabalho automatizado de conformidade de protocolo, e verificação formal envolvendo infraestrutura zkVM RISC-V.

O roteiro técnico atualizado da Ethereum atribui à verificação formal um papel a par da privacidade, das provas de conhecimento zero e da proteção pós-quântica. Os comentários de Buterin de 17 de setembro continuam, portanto, uma direção de investigação existente, em vez de anunciarem uma nova atualização ou fork agendado. A sua publicação não nomeou um novo EIP, data de implementação ou regra obrigatória que exija que todos os programas Ethereum sejam submetidos a verificação formal.

As evidências atuais de IA mostram também uma capacidade ofensiva mais forte

Investigações recentes em cibersegurança apoiam a preocupação de que a IA está a tornar os atacantes mais capazes, mesmo à medida que o uso defensivo se expande. A Anthropic afirmou no seu relatório de inteligência de ameaças de setembro que observou agentes maliciosos a usar IA para automatizar a investigação de vulnerabilidades, o desenvolvimento de exploits e campanhas contra múltiplos alvos. A empresa afirmou que alguns operadores mantinham fluxos de trabalho automatizados capazes de realizar investigação de vulnerabilidades continuamente.

Investigações anteriores da Anthropic encontraram evidências semelhantes em grande escala. O seu painel de divulgação coordenada indicava que, até 26 de agosto, a empresa tinha divulgado 2.300 vulnerabilidades descobertas por IA em 392 projetos de código aberto, com 421 corrigidas a montante nessa altura.

A Anthropic descreveu a mesma tecnologia como útil para a defesa. A sua iniciativa Project Glasswing relatou o uso de modelos de fronteira com empresas de segurança e fornecedores de software para localizar falhas de gravidade alta e crítica antes de os agentes maliciosos as poderem explorar.

O lado ofensivo permanece mensurável. O estudo de junho da Anthropic examinou 832 contas associadas a atividade cibernética maliciosa de março de 2025 a março de 2026 e descobriu que os agentes de ameaças usavam IA em várias fases das operações cibernéticas. Buterin já tinha rejeitado um argumento separado de que os riscos de segurança impulsionados pela IA poderiam prejudicar gravemente a confiança no Bitcoin. Afirmou que os problemas ao nível da rede podiam muitas vezes ser resolvidos através de atualizações de software e da infraestrutura de mineração, ao mesmo tempo que descreveu quebras reais dos hashes do Bitcoin ou do mecanismo de prova de trabalho como altamente improváveis.

O relatório de setembro da Anthropic afirmou que os seus investigadores identificaram operadores que usavam pipelines de exploits criados por IA contra appliances de segurança e alvos governamentais, com algumas campanhas a produzirem vulnerabilidades anteriormente desconhecidas que os atacantes validaram nos seus próprios ambientes de teste.