Agentproof: Static Verification of Agent Workflow Graphs

Resumo Técnico: Agentproof

1. O Problema

Os frameworks de agentes de IA (como LangGraph, CrewAI, AutoGen e Google ADK) representam cada vez mais o comportamento dos agentes como grafos de fluxo de trabalho explícitos. No entanto, a segurança nesses sistemas é predominantemente tratada como uma preocupação em tempo de execução (runtime), utilizando guardrails que filtram conteúdo ou chamadas de ferramentas individualmente.

Essas abordagens reativas possuem três limitações fundamentais:

1. Sobrecarga de latência: Impõem custo por chamada.
2. Cobertura parcial: Detectam violações apenas quando o caminho de execução ofensivo é realmente exercitado.
3. Falha na detecção de defeitos topológicos: Não conseguem identificar erros estruturais no grafo (como nós sem saída, ciclos infinitos ou rotas que contornam aprovações humanas) a menos que esses caminhos específicos sejam testados.

Existe uma lacuna na verificação estática: técnicas de model checking clássicas (como SPIN ou NuSMV) poderiam detectar esses erros, mas exigem que os desenvolvedores traduzam manualmente o código do agente para linguagens de modelagem dedicadas (ex: Promela), o que é proibitivo para a iteração rápida de designs de agentes.

2. Metodologia

O Agentproof é um sistema projetado para a verificação estática pré-implantação de grafos de fluxo de trabalho de agentes. A abordagem baseia-se na extração automática do modelo de análise diretamente do código-fonte dos frameworks, eliminando a necessidade de modelagem manual.

O pipeline do sistema consiste em cinco etapas principais:

1. Extração de Grafos Abstratos:

   • O sistema possui extratores específicos para quatro frameworks principais (LangGraph, CrewAI, AutoGen, Google ADK).
   • Esses extratores normalizam representações heterogêneas em um modelo de grafo unificado (AgentGraph) com nós e arestas tipados (ex: entry, exit, tool, llm, router, human, subgraph).
   • Isso permite que as análises subsequentes sejam independentes do framework.

2. Verificações Estruturais (6 Checks):

   • O sistema executa verificações topológicas lineares ($O(|V| + |E|)$) sobre o grafo extraído:
     • Alcance de Saída: Todos os nós alcançáveis podem chegar a um nó de saída?
     • Ausência de "Dead-Ends": Existem nós que não são de saída e não têm arestas de saída?
     • Isolamento/Reversibilidade: Garante que não há nós presos em ciclos sem saída (livelock).
     • Forma do Roteador: Verifica se as arestas de nós de roteamento são condicionais.
     • Porta Humana (Human Gate): Garante que caminhos para ferramentas sensíveis passem por um nó de aprovação humana.
     • Declaração de Ferramentas: Verifica se nós de ferramenta têm nomes de ferramentas declarados.
   • Ao falhar, o sistema gera um rastro de testemunha (witness trace) que mostra o caminho exato do defeito.

3. Políticas Temporais (DSL e DFA):

   • O sistema utiliza uma DSL (Domain Specific Language) para especificar políticas de segurança baseadas no fragmento de segurança da Lógica Temporal Linear (LTL).
   • As políticas são compiladas em Autômatos Finitos Determinísticos (DFA).
   • Verificação Estática: Realiza uma construção de produto entre o Grafo do Agente e o DFA (Graph × DFA). Isso permite verificar se qualquer caminho no grafo viola a política, sem executar o agente.
   • Monitoramento em Tempo de Execução: Os mesmos DFAs podem monitorar fluxos de eventos em tempo real.

4. Modelo de Ameaças:

   • Foca em erros de desenvolvedor (T1) e injeção maliciosa de workflows (T2) via CI/CD.
   • Assume que o conteúdo gerado pelo LLM (semântica) é não determinístico e fora do escopo; o foco é a topologia e o fluxo de controle.

3. Contribuições Principais

• Pipeline de Extração Cross-Framework: A primeira ferramenta que extrai automaticamente modelos de verificação unificados de quatro frameworks de agentes distintos, eliminando a barreira de entrada de modelagem manual exigida por verificadores genéricos.
• Pipeline de Verificação Pré-Implantação: Combina 6 verificações estruturais com um verificador temporal baseado em DFA, capaz de detectar defeitos topológicos que ferramentas de tempo de execução ignoram.
• DSL de Segurança Específica para Agentes: Uma linguagem de política que cobre o fragmento de segurança da LTL, projetada para ser simples de usar e compilada em DFAs eficientes.
• Benchmarks e Avaliação Empírica: Criação de um corpus de 18 workflows curados (incluindo defeitos injetados) para avaliar a eficácia da ferramenta.

4. Resultados da Avaliação

O sistema foi avaliado em um conjunto de 18 workflows construídos pelos autores, cobrindo os quatro frameworks suportados.

• Detecção de Defeitos:
  • 27% dos workflows no benchmark continham defeitos estruturais (nós sem saída, saídas inacessíveis, violações de forma de roteador).
  • 55% violaram uma política de "porta humana" quando aplicada (falta de aprovação humana em tarefas sensíveis).
  • O sistema detectou 100% dos defeitos estruturais injetados.
• Desempenho:
  • A verificação é extremamente rápida. Para grafos de até 5.000 nós, a verificação completa ocorre em menos de um segundo (ex: ~105 ms para 5.000 nós).
  • A compilação de políticas e a avaliação de monitoramento são independentes do tamanho do grafo.
• Políticas Temporais:
  • 15 políticas de segurança reais (baseadas em GDPR, SOC 2, OWASP) foram definidas. Todas se encaixaram no fragmento de 7 formas da DSL e foram verificadas com sucesso.
• Precisão:
  • As verificações estruturais alcançaram precisão perfeita (P=1.0).
  • A detecção de nós "humanos" (baseada em heurísticas de nomenclatura) teve uma precisão de 0.75 devido a um falso positivo em um fluxo de baixo risco, indicando uma área para melhoria (ex: uso de anotações explícitas).

5. Significado e Impacto

O Agentproof preenche uma lacuna crítica na segurança de agentes de IA:

• Complementaridade: Ele não substitui os guardrails de tempo de execução (que protegem contra conteúdo tóxico ou injeção de prompt), mas complementa-os ao garantir que a topologia do workflow seja segura antes mesmo de o agente ser executado.
• Eficiência: Permite a detecção de defeitos que só ocorreriam em caminhos de execução raros ou não testados, economizando custos de computação e riscos de segurança.
• Adoção Prática: Ao eliminar a necessidade de modelagem manual, torna a verificação formal acessível para desenvolvedores de agentes que iteram rapidamente sobre designs complexos.
• Futuro: O trabalho estabelece uma base para a criação de benchmarks reprodutíveis e sugere a necessidade de verificação dinâmica de grafos mutáveis e a expansão da DSL para fragmentos temporais mais ricos.

Em resumo, o Agentproof transforma a segurança de agentes de uma prática reativa e baseada em amostragem para uma prática proativa e exaustiva baseada na estrutura do sistema.