Formal Security Analysis of Agent Protocol Composition

Sintesi Tecnica: Analisi di Sicurezza Formale della Composizione di Protocolli per Agenti

Definizione del Problema
I protocolli per agenti AI (es. MCP, A2A, ANP) si stanno evolvendo in infrastrutture software critiche che mediano l'accesso agli strumenti, la delega e il contesto condiviso attraverso flussi di lavoro autonomi. Sebbene le vulnerabilità dei singoli protocolli (es. command injection in un singolo server) siano documentate, esiste un significativo divario di garanzia relativo alla composizione dei protocolli. Quando più agenti o server interagiscono, emergono comportamenti insicuri derivanti dall'interazione tra payload semantici, autorità delegata e contesto condiviso, piuttosto che da errori isolati nel formato dei messaggi.

Gli approcci attuali non riescono ad affrontare questo aspetto in modo olistico: la verifica classica dei protocolli si concentra sulla forma dei messaggi e l'integrità dei canali ma manca di ragionamento semantico; la ricerca sulla sicurezza degli agenti mira spesso a specifici attacchi o benchmark piuttosto che alle specifiche dei protocolli e ai comportamenti degli SDK; e i metodi formali per i sistemi agentici verificano tipicamente piani o artefatti di coordinamento piuttosto che i protocolli di comunicazione pubblica stessi. La sfida centrale è mantenere una catena di evidenza dalle specifiche in linguaggio naturale ai controlli formali e ai test di implementazione, tenendo conto del fatto che le responsabilità di sicurezza sono spesso distribuite tra specifiche, SDK, host e bridge di runtime, lasciando "vuoti di responsabilità" dove nessun componente possiede il controllo.

Metodologia: Framework AgentThread
Gli autori presentano AgentThread, un framework collegato alla sorgente progettato per eseguire l'analisi della garanzia di sicurezza sui protocolli degli agenti, dalla specifica testuale agli SDK in esecuzione. Il flusso di lavoro è strutturato in tre fasi:

1. Estrazione Collegata alla Sorgente e Rappresentazione Intermedia (IR):

   • Il sistema raccoglie gli artefatti autorevoli del protocollo (prosa, schemi, SDK, implementazioni di riferimento).
   • Estrae le Clausole Normative (es. "MUST", "SHOULD") e le mappa in una IR di Protocollo Tipizzata. Questa IR preserva la provenienza della sorgente, i legami tra gli attori e la modalità.
   • Fondamentalmente, genera anche una IR di Responsabilità, che traccia chi possiede un determinato controllo (specifica, SDK, bridge) e se tale controllo è applicato.

2. Modellazione Formale (TLA+):

   • La IR viene compilata in modelli TLA+ utilizzando il model checker TLC.
   • Il framework definisce uno scopo di sicurezza a livelli:
     • Livello RPC (L1-L3): Integrità del messaggio, ciclo di vita della sessione, legame identità/capability.
     • Livello Agente (L4-L5): Controllo delle operazioni semantiche (es. prompt injection), audit/accountability e sicurezza della composizione.
   • Verifica a due fasi:
     • Fase 1 (Livello Specifica): TLC genera tracce di controesempio per gli invarianti violati. I risultati vengono classificati come Spec-Fail, Model-Fail o Ambiguity-Fail.
     • Fase 2 (Livello Implementazione): I controesempi eseguibili vengono abbassati attraverso Adapter di Protocollo in test di riproduzione contro SDK reali e server di riferimento. Se una traccia non può essere riprodotta, viene registrata l'evidenza a livello di sorgente/tipo.

3. Analisi della Composizione:

   • Il framework costruisce modelli TLA+ composti combinando le transizioni IR di due protocolli e aggiungendo Azioni di Bridge che modellano il trasferimento di stato attraverso i confini.
   • Le azioni di bridge sono vincolate da contratti di capacità finiti per verificare se le proprietà di sicurezza (es. monotonicità dell'autorità, continuità dell'audit) persistono attraverso il bridge.

Contributi Chiave

1. Analisi Formale Sistematica: Il documento definisce uno scopo di sicurezza a livelli per i protocolli degli agenti e deriva invarianti TLA+ verificabili che coprono il flusso del contenuto semantico, l'autorità delegata e la sicurezza della composizione.
2. Flusso di Lavoro Collegato alla Sorgente: AgentThread stabilisce una pipeline dal testo del protocollo ai modelli formali e ai test di implementazione, preservando i riferimenti alla sorgente per distinguere tra non conformità della specifica, lacune nelle raccomandazioni e responsabilità non assegnate.
3. Studio Empirico: Gli autori valutano cinque protocolli (MCP, A2A, ANP, ACP, ACP-Client), i loro SDK di produzione e otto modelli composti.

Risultati
Lo studio ha prodotto le seguenti scoperte attraverso i cinque protocolli e gli otto modelli composti:

• Risultati a Livello di Specifica: Sono stati identificati 35 problemi a livello di specifica. Questi includevano 12 confermati dai test di implementazione e 23 problemi presenti solo nella specifica.
• Fallimenti di Implementazione: Sono stati eseguiti 80 test di implementazione contro SDK di produzione e server di riferimento.
  • MCP: Ha mostrato una diretta non conformità agli standard (es. mancata sanitizzazione degli output degli strumenti nonostante i requisiti "MUST").
  • A2A e Altri: Spesso hanno esibito "lacune di hardening del framework" dove le specifiche mancavano di controlli obbligatori per l'ambito di delega o le tracce di audit.
• Fallimenti di Composizione: Sono stati scoperti 30 fallimenti aggiuntivi che emergevano solo sotto composizione di protocolli.
  • Questi fallimenti includevano escalation di autorità, bypass del consenso e interruzioni della traccia di audit dove un componente bridge (es. un runtime di un agente che connette MCP e A2A) permetteva a contenuti non attendibili di influenzare l'autorità delegata.
  • Nessun singolo protocollo possedeva il controllo per questi comportamenti cross-protocollo; erano "orfani di composizione".
• Lacune di Responsabilità: Solo un protocollo (ANP) applicava un controllo rilevante per la sicurezza (identità basata su DID) nella pratica. Nessun protocollo assegnava la responsabilità di enforcement per il comportamento cross-protocollo.

Significatività e Rivendicazioni
Il documento sostiene che l'insicurezza nei protocolli degli agenti non è semplicemente un bug della specifica o dell'implementazione, ma un vuoto di responsabilità attraverso lo stack software.

• L'Hardening Locale è Insufficiente: Proteggere i singoli server o SDK non impedisce i fallimenti derivanti dalla composizione di più componenti (es. un attaccante che controlla una pagina web recuperata da un server per iniettare istruzioni che attivano una lettura di file da parte di un altro).
• Il Problema del "Proprietario": I controlli di sicurezza critici per i sistemi composti spesso cadono al di fuori dello scopo normativo di un singolo protocollo, rimanendo non posseduti da specifiche, SDK o deployment.
• Spostamento Metodologico: Gli autori sostengono che la sicurezza della composizione debba essere trattata come una proprietà del protocollo di prima classe che richiede contratti di composizione espliciti e responsabilità di enforcement, piuttosto che come un'aggiunta successiva a livello applicativo. AgentThread fornisce il meccanismo per rendere esplicite queste obbligazioni suddivise sin dalle prime fasi del processo di progettazione.