Resumo Técnico: FAVA (Autorização Formal para Agentes Verificados com Grafos de Permissão Baseados em Evidências)

Declaração do Problema

Agentes de Grandes Modelos de Linguagem (LLMs) operam cada vez mais em ambientes dinâmicos e críticos (ex: repositórios de código, armazenamento em nuvem, shells locais), intercalando o raciocínio semântico com operações complexas de sistema. O artigo argumenta que os mecanismos de autorização existentes são fundamentalmente insuficientes para esses cenários devido a três limitações primárias:

1. Descompasso Estático vs. Dinâmico: As defesas atuais dependem de listas de permissões (allowlists) estáticas de nível de ferramenta ou filtros de palavras-chave, que falham em considerar a natureza altamente dependente de contexto da execução de agentes. As políticas de agentes do mundo real frequentemente envolvem restrições temporais dependentes de sequência (90% dos projetos analisados) e lógica condicional aninhada (mais de 40%), que listas estáticas não conseguem capturar.
2. Ambiguidade Semântica: Políticas baseadas apenas em prompts (ex: pedir aos modelos para "serem seguros") carecem de capacidades de aplicação, enquanto sandboxes de nível de SO carecem da compreensão semântica necessária para governar lógica condicional de alto nível e fluxos de dados.
3. Falta de Garantias Formais: LLMs probabilísticos não podem garantir a correção formal em relação à exfiltração de dados, modificações de estado destrutivas ou violações de obrigações temporais.

Metodologia

O FAVA propõe um framework de autorização em tempo de execução que desacopla a compreensão semântica da aplicação lógica. O sistema opera através de um pipeline de quatro estágios:

1. Aquisição de Evidências e IR de Permissão

O FAVA utiliza um LLM estritamente como um extrator semântico, não como um tomador de decisão. Ele analisa tarefas em linguagem natural, contratos de execução e rastros de execução em uma Representação Intermediária (IR) de Permissão estruturada. Esta IR define explicitamente os limites de autorização usando cinco campos principais:

• Intenção, Ativos, Ações, Obrigações e Sinks (Destinos).
• Intervalos de Evidência (Evidence Spans): Links criptográficos ou textuais conectando cada campo à sua origem.
  Este passo preserva instruções semânticas complexas (ex: "requer revisão antes de testar") como restrições estruturais auditáveis, em vez de julgamentos opacos do modelo.

2. Redução de Grafo (Graph Lowering)

Uma passagem de redução determinística converte a IR de Permissão em um grafo de permissão baseado em evidências $G = (V, E)$.

• Nós: Carregam rótulos de segurança fundamentados em evidências (ex: segredo, pii, destrutivo).
• Arestas: Codificam relações de dependência, incluindo fluxos de dados, guardas de controle (restrições temporais) e ancestralidade de tempo de execução.
• Sanitização: Requer especificações de transformadores confiáveis explícitas (ex: redact(secret) -> safe_text); asserções vagas não são tratadas como sanitizadores.
  Este grafo serve como um substrato formalmente verificável, transformando dados semânticos em uma estrutura adequada para verificação matemática.

3. Autorização SMT

A decisão de segurança central é computada por um autorizador de Satisfatibilidade de Teorias Modulares (SMT) (implementado usando Z3). O solver avalia o grafo contra uma política fixa para determinar se uma atribuição de capacidade é satisfatória.

• Propagação de Taint (Mancha): Os rótulos propagam-se ao longo das arestas de dependência, a menos que sejam transformados por um sanitizador confiável.
• Resolução de Restrições: O sistema verifica fluxos proibidos (ex: segredo $\to$ net:*).
• Saída: O solver retorna um conjunto de capacidades autorizado ou um contraexemplo preciso identificando o caminho violador.
• Monotonicidade: O sistema suporta "reparo de grafo monotônico", onde eventos de tempo de execução adicionam novos fatos ao grafo, forçando a reautorização antes de qualquer ação efetiva.

4. Gateway de Tempo de Execução

Um gateway Just-In-Time (JIT) impõe o resultado do solver.

• Lógica de Decisão: Se um contraexemplo for encontrado, a ação é bloqueada. Se nenhuma violação for encontrada, mas o perfil de risco permanecer sensível ou ambíguo, o gateway falha fechado (fails closed) (bloqueia a ação) para priorizar a segurança sobre a utilidade.
• Escopo: O gateway media todos os efeitos de tempo de execução relevantes para a segurança, garantindo que a execução de backend permaneça dentro do conjunto de capacidades concedido.

Principais Contribuições

1. Conceito de Framework: Introdução do FAVA, um novo framework de autorização em tempo de execução que muda o gerenciamento de permissões de listas de permissões estáticas para autorização de grafo verificável.
2. Metodologia Formal: Um pipeline que aproveita LLMs para extração de IR estruturada, reduz deterministicamente isso para um grafo baseado em evidências e emprega um autorizador SMT para decisões de consistência de política. Este design permite o reparo de grafo monotônico e a reautorização Just-In-Time.
3. Avaliação Abrangente: Testes extensivos nos cenários OpenAgentSafety, OctoBench e ActPlane, demonstrando alta conformidade de decisão e interceptando traços violadores dinâmicos.

Resultados Experimentais

Os autores avaliaram o FAVA em um conjunto de dados de 801 tarefas em quatro benchmarks.

• Taxa de Conformidade de Decisão (DCR): O FAVA alcançou um DCR de 90,5% sobre o conjunto de dados agregado.
• Cenários Condicionados por Traço: O FAVA alcançou 100,0% de DCR nas divisões estruturadas e rotuladas de traço condicionado (ActPlane Public e ActPlane Traces), interceptando com sucesso todas as ações não autorizadas sem falsos negativos nestas divisões específicas.
• Comparação:
  • Vs. Guardas Estáticos/Regex: O FAVA superou significativamente o Regex Guard, que sofreu de bloqueios excessivos (0 Verdadeiros Negativos em OpenAgentSafety).
  • Vs. Prompt-Only/Heurística: O FAVA superou o GuardAgent e o AgentSpec, que exibiram Falsos Negativos massivos (sub-bloqueio) devido à falta de rastreamento explícito de fluxo de dados.
• Eficiência: O gateway ativo de tempo de execução adiciona um overhead negligenciável de 0,3% à execução do agente ao vivo. O tempo mediano de autorização Just-In-Time é de 0,845 ms, mesmo para grafos com até 10 nós.

Significância e Alegações

O artigo afirma que o FAVA estabelece uma fundação rigorosa e matematicamente fundamentada para assegurar agentes autônomos, ao separar explicitamente a compreensão do LLM da aplicação de segurança.

• Garantia Formal: O sistema fornece garantias formais em relação ao grafo de permissão gerado e à tradução da política. Ele afirma que qualquer atribuição de capacidade satisfatória satisfaz estritamente todas as regras de política codificadas.
• Mudança de Paradigma: Ele aborda a "lacuna de modalidade" entre instruções de linguagem natural e aplicação rigorosa, traduzindo tarefas ambíguas em um substrato determinístico.
• Segurança Conservadora: O framework adota intencionalmente uma postura conservadora, priorizando a segurança sobre a utilidade ao falhar fechado em ações ambíguas ou sensíveis. Essa troca resulta em uma alta taxa de interceptação de ataques (98,9%) ao custo de alguma utilidade benigna (69 bloqueios falsos na avaliação).

Os autores observam que a solidez do sistema depende da correção da extração do LLM de nível superior e da integridade do gateway. Embora a autorização matemática seja robusta, o sistema não pretende resolver a completude da extração de linguagem natural ou a descoberta de fluxos implícitos. Melhorias futuras são direcionadas para a extração semântica consciente de proveniência, em vez de alterar a lógica de decisão SMT.