CaMeLoT verifica formalmente o plano de um agente de IA antes de executar qualquer ferramenta
CaMeLoT estende a defesa CaMeL contra injeção de prompt adicionando uma camada de verificação estática: o plano gerado por um agente LLM é traduzido em um sistema de transição de estados finitos, rotulado com informação de proveniência e taint, e checado contra políticas temporais expressas em lógica CTL usando o model checker nuXmv antes de qualquer ferramenta ser de fato chamada. Planos reprovados geram um contraexemplo que serve de retroalimentação para o agente corrigir o plano, sem gastar chamadas de LLM ou de ferramenta nem precisar desfazer efeitos colaterais.
O ponto de partida do CaMeLoT é uma observação sobre a natureza da segurança em agentes que executam planos de múltiplas etapas: o risco não está isolado em um único passo, mas na trajetória inteira que o plano gera — quais ferramentas são chamadas, em que ordem, e como dados fluem entre elas. O CaMeL, sistema do qual este trabalho é uma extensão, já ataca injeção de prompt rastreando taint e proveniência durante a execução; o CaMeLoT complementa isso adicionando uma etapa de verificação antes da execução, quando ainda é barato reprovar um plano ruim.
Tecnicamente, o plano gerado pelo agente é traduzido em um sistema de transição de estados finito, rotulado com as chamadas de ferramenta previstas, informação de proveniência (de onde veio cada dado) e informação de taint (quais dados são potencialmente controlados por um atacante). Esse sistema é então checado contra políticas de segurança expressas em lógica temporal computacional (CTL) — um formalismo que permite expressar propriedades sobre toda a execução futura possível, como "um dado marcado como não confiável nunca deve alcançar uma chamada de rede sem passar por sanitização" — usando o model checker nuXmv, uma ferramenta madura e amplamente usada em verificação formal de sistemas.
A vantagem prática dessa abordagem é dupla: primeiro, planos inseguros são rejeitados antes de qualquer chamada real de LLM ou de ferramenta, economizando tokens e evitando o custo operacional de reverter efeitos colaterais já produzidos ou de desmontar sandboxes temporários criados para a execução. Segundo, quando a verificação falha, o model checker devolve um contraexemplo concreto — uma trajetória específica que viola a política —, que pode ser usado como retroalimentação estruturada para o próprio agente tentar reparar o plano, em vez de simplesmente recusar a tarefa sem explicação.
Os autores avaliam o CaMeLoT contra políticas derivadas do benchmark AgentDojo (referência comum para medir robustez de agentes contra injeção de prompt), fluxos de trabalho de centro de operações de segurança (SOC) e experimentos de extração de prompt, mostrando que o sistema consegue verificar uma classe ampla de propriedades temporais antes da execução, preservando a cobertura de checagem em tempo de execução que o CaMeL original já oferecia. Para quem está avaliando arquiteturas de defesa para agentes que operam com autonomia sobre ferramentas sensíveis, o trabalho reforça a tendência de combinar verificação estática (antes de agir) com monitoramento dinâmico (durante a ação) como camadas complementares, em vez de depender de apenas uma das duas.