Extending the Formalism and Theoretical Foundations of Cryptography to AI

Resumo Técnico: Estendendo o Formalismo e as Fundações Teóricas da Criptografia para IA

Autores: Federico Villa, F. Betül Durak, Tadayoshi Kohno, Tapdig Maharramli, Franziska Roesner.
Instituições: ETH Zurich, Microsoft Research, Georgetown University, University of Washington.

1. O Problema

O avanço recente em Modelos de Linguagem (LMs) permitiu o surgimento de agentes autônomos capazes de executar tarefas complexas com supervisão mínima. À medida que esses agentes ganham autonomia e autoridade em sistemas críticos, a comunidade de segurança identifica riscos significativos.
O problema central abordado é a falta de uma base formal comum para avaliar e comparar propostas de controle de acesso e permissão para agentes de IA. Atualmente, as soluções existentes (como Progent, Conseca, FIDES) são frequentemente baseadas em heurísticas ou argumentos intuitivos, dificultando a comparação rigorosa de suas garantias de segurança. Não há um modelo unificado que defina formalmente o que significa um sistema de IA ser "seguro", "completo" (funcional) e "robusto" contra adversários.

2. Metodologia

Os autores adotam uma perspectiva interdisciplinar, aplicando o rigor da criptografia moderna (definições formais, modelos de adversários e provas de segurança redutíveis) ao domínio da IA. A metodologia segue os seguintes passos:

• Abstração AIOracle: Definem um modelo unificado chamado AIOracle, que engloba LMs, chatbots, classificadores e agentes. O modelo opera em duas fases principais:
  • LEARN: Envolve a geração de dados (GENERATE_DATA), fine-tuning e aprendizado por reforço.
  • INFER: O processo de inferência onde o modelo recebe um prompt e um contexto para gerar um resultado.
• Taxonomia de Ataques: Desenvolvem uma taxonomia multidimensional para classificar ataques contra LMs, baseada em:
  • Vetor de Ataque: Baseado em dados (corrupção no treinamento) ou baseado em prompts (injeção na inferência).
  • Fase de Ataque: Aprendizado (pre-training/fine-tuning) ou Inferência.
  • Conhecimento do Adversário: White-box (acesso total ao modelo) ou Black-box (apenas API).
  • Persistência: Ataques transitórios (sessão única) ou persistentes (alteração permanente do modelo).
• Jogos de Segurança (Security Games): Introduzem um framework baseado em jogos para definir formalmente a segurança.
  • Completude (Completeness): Garante que o sistema funcione corretamente na ausência de um adversário (atende aos objetivos de "ajudabilidade" e "inocuidade").
  • Segurança (Robustness): Garante que o sistema resista a manipulações de um adversário com capacidades computacionais limitadas, mantendo a confidencialidade, integridade e disponibilidade (CIA).
• Decomposição Modular: Propõem uma abordagem de "construção dual" para separar objetivos conflitantes (como ajudar o usuário vs. não causar danos), utilizando oráculos criativos e oráculos de filtragem (boring).

3. Principais Contribuições

1. Fundação Formal para Agentes de IA: Estabelecem o primeiro framework formal que unifica a segurança de agentes autônomos, definindo o AIOracle e seus algoritmos de aprendizado e inferência.
2. Taxonomia Unificada de Ataques: Criaram uma classificação sistemática de ataques (ex: envenenamento de dados, jailbreak, injeção de prompts, inferência de associação) que permite analisar vulnerabilidades em diferentes fases do ciclo de vida do modelo.
3. Jogo de Segurança Unificado: Desenvolvem um jogo de segurança que captura simultaneamente Confidencialidade, Integridade e Disponibilidade.
   • Demonstram formalmente que proteger a confidencialidade dos dados de treinamento (impedir que o modelo revele informações privadas) entra em conflito fundamental com a completude (utilidade do modelo). Se um modelo é perfeitamente privado (diferencialmente privado), ele perde a capacidade de aprender padrões úteis, tornando-se inútil para certas tarefas.
4. Decomposição Modular de Objetivos: Formalizam a separação entre "ajudabilidade" (helpfulness) e "inocuidade" (harmlessness) em predicados distintos ($\phi_1$ e $\phi_2$).
   • Provaram a correção (soundness) de uma construção dual onde um modelo "criativo" gera respostas e um modelo "burocrático" (filtro) verifica se elas atendem aos critérios de segurança antes de serem entregues.
5. Análise de Mecanismos Existentes: Aplicaram seu formalismo para analisar e explicar as limitações de sistemas atuais como FIDES, Progent e Conseca, identificando, por exemplo, o risco de atualizações de política baseadas em prompts não verificadas.

4. Resultados Chave

• Conflito Inerente entre Privacidade e Utilidade: O trabalho prova que, sob o modelo formal proposto, é impossível ter um sistema que seja simultaneamente perfeitamente seguro contra vazamento de dados de treinamento (confidencialidade estrita) e completamente útil (completude). A proteção total de dados de treinamento impede o aprendizado de padrões necessários para a funcionalidade.
• Validação da Abordagem Modular: A prova teórica da "construção dual" demonstra que é possível garantir a segurança de um sistema complexo decompondo-o em módulos menores (gerador e verificador), desde que cada módulo satisfaça seus próprios requisitos de completude e segurança.
• Identificação de Vulnerabilidades em Projetos Atuais: A análise formal revelou que mecanismos que dependem de um único LM para gerar e verificar políticas (como em algumas implementações de Conseca e Progent) criam um paradoxo de segurança, onde o mecanismo de defesa é tão vulnerável a ataques de injeção de prompts quanto o próprio agente que ele protege.

5. Significância e Impacto

Este trabalho é fundamental por trazer o rigor da criptografia para a segurança de IA.

• Mudança de Paradigma: Move o campo de discussões baseadas em heurísticas e testes empíricos para um terreno de definições formais e provas de segurança.
• Guia para Projetistas: Oferece aos engenheiros de segurança e pesquisadores um modelo para projetar sistemas de agentes que sejam "provavelmente seguros" (provably secure), sugerindo que a decomposição modular é a via mais promissora para resolver conflitos entre segurança e funcionalidade.
• Base para Regulamentação: Fornece uma linguagem técnica precisa para avaliar a segurança de sistemas de IA, o que é crucial para o desenvolvimento de padrões e regulamentações futuras.
• Prevenção de Riscos: Ao formalizar as capacidades do adversário e as condições de vitória, o trabalho ajuda a identificar falhas estruturais antes que sistemas inseguros sejam implantados em ambientes críticos.

Em suma, o artigo argumenta que, para projetar sistemas de IA seguros com métricas mensuráveis, é necessário abandonar abordagens monolíticas e adotar uma arquitetura modular baseada em fundamentos formais, permitindo reduções de segurança e garantias teóricas sólidas.