Proof-Gated Signing usa solver SMT para blindar agentes de IA com carteiras cripto contra 'state drift'
O artigo ataca um problema especifico de agentes de IA que controlam carteiras on-chain: como eles leem conteudo potencialmente controlado por atacantes, podem ser induzidos a propor transacoes danosas, e as verificacoes usuais checam o estado da blockchain no momento da checagem, nao no momento da execucao -- uma janela que um atacante pode explorar via front-running ou mudancas de contrato. A defesa proposta, Proof-Gated Signing, simula a transacao, extrai seus efeitos e usa um solver SMT para provar que uma politica declarativa se mantem valida sob toda uma faixa de incerteza de preco, bloqueando no proprio contrato de carteira qualquer execucao que viole as pos-condicoes provadas; em 260 cenarios de teste, preveniu 93,6% dos ataques, contra 57,9% da simulacao isolada e 71,4% da allowlist estatica.
Agentes de IA que controlam carteiras on-chain leem conteudo potencialmente alcancavel por atacantes (sites, metadados de token, mensagens) e podem ser induzidos, via prompt injection, a propor transacoes danosas. As defesas usuais de pre-assinatura -- allowlist estatica, revisao por LLM, simulacao de transacao -- compartilham uma mesma falha estrutural: todas descrevem o estado da blockchain no momento da checagem, mas a transacao so executa depois, em um estado que um atacante pode moldar via front-running, upgrade de contrato ou mudanca de parametros de token. Os autores chamam essa janela de 'state drift'.
O Proof-Gated Signing (PGS) simula a transacao proposta, extrai seus efeitos, e usa um solver SMT para verificar se uma politica declarativa de valor e permissao se mantem valida em toda uma faixa de incerteza de oraculo de preco -- nao apenas no unico preco observado no momento da checagem. Essa garantia provada e entao compilada em pos-condicoes on-chain (limites de saldo da carteira, recebimento correto pelo beneficiario, limites de allowance, propriedade), que o proprio contrato inteligente da carteira do agente aplica de forma atomica -- de modo que a garantia sobrevive ao drift de estado, em vez de depender de a checagem ainda ser valida mais tarde.
Em um ambiente de teste aberto com 260 cenarios (14 familias de ataque, incluindo cinco de drift e duas adaptativas, e 12 familias benignas), com dano medido a partir do saldo obtido pelo atacante, o PGS preveniu 93,6% dos 140 cenarios danosos e aprovou 97,5% dos cenarios benignos, contra 57,9% de prevencao so com simulacao e 71,4% com allowlist estatica. Nenhum dos 50 cenarios de drift gerou ganho para o atacante sob PGS. Um dado particularmente relevante: dar a um revisor LLM uma simulacao limpa, mas anterior ao drift, tornou-o mais propenso a aprovar um ataque de drift -- ou seja, o revisor baseado em LLM piorou especificamente quando recebeu um estado convincente, porem obsoleto.
Esse ultimo achado e uma resposta concreta e mensuravel a pergunta 'um revisor LLM consegue pegar uma transacao maliciosa' para carteiras agenticas: a resposta aqui e nao, de forma confiavel, quando o atacante pode moldar o estado entre a checagem e a execucao -- e o fato de simulacoes convincentes tornarem o LLM mais confiante e um alerta especifico contra depender do julgamento de um LLM como barreira final para acoes financeiras de agentes. Com overhead de cerca de 41 mil gas e 0,1-0,2 segundos por checagem, a abordagem e viavel para equipes que constroem agentes autonomos on-chain hoje.