Uso de Ferramentas Verificavelmente Seguro para Agentes de LLM: STPA encontra MCP

Venho acompanhando a literatura sobre guardrails há algum tempo — GuardAgent, ShieldAgent, AGrail — e todos eles melhoram as taxas de detecção enquanto admitem discretamente que não podem realmente garantir nada. Este artigo da ICSE NIER 2026 de Doshi et al., da CMU e NC State, adota um ângulo diferente: em vez de perguntar como detectar o comportamento inadequado do agente de forma mais confiável, eles perguntam como tornar o comportamento inseguro formalmente impossível. É um artigo de posicionamento, não um estudo empírico, mas a estruturação é nítida o suficiente para valer uma leitura atenta.

O artigo

"Towards Verifiably Safe Tool Use for LLM Agents" (arXiv:2601.08012), de Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos e Christian Kästner, propõe uma metodologia para derivar e aplicar especificações de segurança sobre o uso de ferramentas por agentes de LLM. A observação central é que os riscos em sistemas de agentes surgem principalmente da composição de ferramentas — e não de falhas individuais de ferramentas — portanto, as proteções no nível de componente não conseguem capturá-los. Um agente que resolve um conflito de calendário pode consultar corretamente um registro de saúde privado e enviar um e-mail corretamente, enquanto ainda faz algo catastrófico: vazar o conteúdo desse registro para os colegas de um paciente.

A solução proposta tem duas partes. Primeiro, os autores aplicam a Análise de Processos Teórico-Sistêmica (STPA), um método de engenharia de segurança de sistemas de aviação e nucleares, para identificar perigos no nível do agente, derivar requisitos de segurança e formalizá-los como especificações em fluxos de dados e sequências de ferramentas. Em segundo lugar, eles introduzem um framework de Model Context Protocol (MCP) aprimorado por recursos, onde cada ferramenta deve declarar metadados estruturados: nível de recurso (somente leitura, somente gravação, leitura-gravação, execução), classificação de confidencialidade e nível de confiança. A aplicação é então estruturada em quatro níveis: blocklist automática para fluxos comprovadamente inseguros, mustlist para sequências obrigatórias, allowlist para operações pré-aprovadas e escalonamento de confirmação para casos ambíguos.

A etapa de verificação formal usa o Alloy, uma ferramenta de lógica relacional de primeira ordem, para modelar o espaço de execução e verificar exaustivamente se, sob as políticas declaradas, as violações de segurança não podem ocorrer enquanto os rastros seguros permanecem alcançáveis. Este é o principal "resultado" do artigo — não há números de precisão de benchmark, o que é esperado para um artigo curto da NIER.

Ideias principais

• A STPA reformula a segurança do agente como um problema de engenharia de sistemas: identificar perdas, rastrear interações perigosas, derivar requisitos — antes de escrever qualquer código de aplicação.
• As especificações se dividem em dois tipos: restrições de fluxo de informações ("e-mails de eventos não devem incluir dados privados que não pertencem ao destinatário") e restrições de lógica temporal ("cada update_event deve ser seguido por send_email para cada participante").
• A aplicação em quatro níveis (blocklist / mustlist / allowlist / confirmação) foi projetada para reduzir a fadiga de segurança — a maioria dos fluxos seguros é pré-aprovada, de modo que o agente não fica constantemente pedindo permissão.
• A análise exaustiva de rastros do Alloy confirmou a ausência de fluxos inseguros no estudo de caso do calendário, preservando a funcionalidade da tarefa.
• Toda a abordagem é explicitamente voltada para agentes específicos para tarefas, não para assistentes de uso geral — os autores reconhecem que agentes restritos são mais viáveis de serem protegidos.

O que se sustenta — e o que não

O movimento intelectual é sólido: tomar emprestado a STPA da engenharia de segurança crítica é o instinto certo. Ao contrário dos guardrails probabilísticos, esta abordagem converte requisitos em predicados sobre rastros do sistema, que podem ser verificados em vez de estimados. A hierarquia de aplicação de quatro níveis foi cuidadosamente projetada — a distinção entre blocklist e confirmação é especialmente importante, porque as solicitações de confirmação permanentes corroem a confiança do usuário e acabam sendo ignoradas.

Dito isso, as limitações do artigo são significativas e, em sua maioria, não são abordadas. O problema da confiança nos metadados é reconhecido, mas não resolvido: todo o framework depende de os desenvolvedores de ferramentas rotularem suas ferramentas com precisão. Em um mercado MCP aberto, onde ferramentas de terceiros são comuns, não há mecanismo de aplicação para a correção dos rótulos. A verificação formal também é feita em um modelo Alloy simplificado e construído manualmente — ela demonstra a viabilidade da abordagem, não que a abordagem possa ser aplicada a sistemas reais em escala.

Também não vejo um argumento convincente de por que a STPA é o método de análise de risco certo em comparação com, digamos, modelagem de ameaças ou HAZOP. O estudo de caso do calendário é ilustrativo, mas trivialmente pequeno. E não há discussão sobre provedores de ferramentas adversários que rotulam deliberadamente os recursos de forma incorreta — o que é uma superfície de ataque real que a literatura de segurança MCP relacionada (arXiv:2601.17549) examina em detalhes.

A estruturação honesta é que se trata de uma proposta de design com um modelo formal de prova de conceito. O trabalho árduo de engenharia — construir o mecanismo de política, testar a cobertura de rótulos em diversas ferramentas, medir empiricamente o compromisso entre autonomia e segurança — é declarado como trabalho futuro.

Por que isso importa para a IA financeira

Agentes de gravação (write-back) do Beancount enfrentam exatamente o padrão de perigo para o qual este artigo foi projetado: a composição de ferramentas criando riscos emergentes. Um agente que lê um lançamento de conta sensível e depois publica um resumo em um razão (ledger) compartilhado pode estar fazendo algo perfeitamente razoável em cada etapa individual, ao mesmo tempo em que viola uma restrição de confidencialidade que só é visível no nível do sistema. A abordagem da STPA de começar pelas perdas das partes interessadas e invertê-las em requisitos mapeia-se perfeitamente para o domínio financeiro, onde as perdas são violações regulatórias, divulgações não autorizadas e mutações irreversíveis no razão.

A extensão MCP é diretamente relevante porque o ferramental do Beancount está sendo cada vez mais encapsulado como servidores MCP. Se essas ferramentas puderem declarar seu nível de recurso e classe de confidencialidade de forma estruturada e legível por máquina, torna-se possível aplicar políticas de fluxo de dados no limite do protocolo, em vez de esperar que o agente se autopolicie. As restrições de lógica temporal — exigindo que cada post_transaction seja precedido por um balance_check bem-sucedido — são exatamente o tipo de invariante que um agente financeiro precisa garantir antes de confirmar as gravações.

A peça que falta, por enquanto, é que nada disso foi construído e testado. Mas como um vocabulário de design para pensar sobre a segurança de agentes de razão, STPA + IFC é o framework mais fundamentado que vi nesta literatura.

O que ler a seguir

• "Securing AI Agents with Information-Flow Control" — arXiv:2505.23643, Microsoft Research; implementa um sistema IFC concreto (Fides) com rastreamento de manchas (taint tracking), avaliado no AgentDojo; o complemento empírico a este artigo.
• "Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents" — arXiv:2601.17549; analisa diretamente a superfície de ataque MCP que o framework deste artigo pretende defender.
• "Systematic Hazard Analysis for Frontier AI using STPA" — arXiv:2506.01782; uma aplicação mais recente da metodologia STPA a sistemas de IA de forma ampla, útil para entender como a técnica escala.