Uso Sicuro e Verificabile degli Strumenti per Agenti LLM: STPA incontra MCP

Da tempo leggo la letteratura sulle barriere di sicurezza — GuardAgent, ShieldAgent, AGrail — e tutte migliorano i tassi di rilevamento ammettendo silenziosamente di non poter garantire nulla. Questo articolo ICSE NIER 2026 di Doshi et al. di CMU e NC State adotta un approccio diverso: invece di chiedersi come rilevare in modo più affidabile il comportamento scorretto di un agente, si chiede come rendere il comportamento non sicuro formalmente impossibile. È un position paper, non uno studio empirico, ma la sua impostazione è sufficientemente nitida da meritare una lettura attenta.

L'articolo​

"Towards Verifiably Safe Tool Use for LLM Agents" (arXiv:2601.08012) di Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos e Christian Kästner propone una metodologia per derivare e far rispettare specifiche di sicurezza sull'uso di strumenti da parte di agenti LLM. L'osservazione centrale è che i rischi nei sistemi agente derivano principalmente dalla composizione di strumenti — non da guasti di singoli strumenti — quindi le salvaguardie a livello di componente non possono intercettarli. Un agente che risolve un conflitto di calendario potrebbe interrogare correttamente una cartella clinica privata e inviare correttamente un'email, mentre compie comunque un'azione catastrofica: divulgare il contenuto di quella cartella ai colleghi di un paziente.

La soluzione proposta ha due parti. In primo luogo, gli autori applicano l'Analisi Sistemico-Teoretica dei Processi (STPA), un metodo di ingegneria della sicurezza proveniente dai settori aeronautico e nucleare, per identificare i pericoli a livello di agente, derivare requisiti di sicurezza e formalizzarli come specifiche sui flussi di dati e le sequenze di strumenti. In secondo luogo, introducono un framework Model Context Protocol (MCP) potenziato con capacità in cui ogni strumento deve dichiarare metadati strutturati: livello di capacità (sola lettura, sola scrittura, lettura-scrittura, esecuzione), classificazione di riservatezza e livello di fiducia. L'applicazione è quindi strutturata su quattro livelli: lista nera automatica per flussi dimostrabilmente non sicuri, lista obbligatoria per sequenze richieste, lista bianca per operazioni pre-approvate ed escalation di conferma per casi ambigui.

Il passo di verifica formale utilizza Alloy, uno strumento di logica relazionale del primo ordine, per modellare lo spazio di esecuzione e verificare esaustivamente che, secondo le policy dichiarate, le violazioni della sicurezza non possano verificarsi mentre le tracce sicure rimangono raggiungibili. Questo è il principale "risultato" dell'articolo — non ci sono valori numerici di accuratezza su benchmark, il che è previsto per un articolo breve NIER.

Idee chiave​

• STPA ridescrive la sicurezza degli agenti come un problema di ingegneria dei sistemi: identificare le perdite, risalire alle interazioni pericolose, derivare i requisiti — prima di scrivere qualsiasi codice di enforcement
• Le specifiche si dividono in due tipi: vincoli sul flusso informativo ("le email di eventi non devono includere dati privati non appartenenti al destinatario") e vincoli di logica temporale ("ogni update_event deve essere seguito da send_email a ciascun partecipante")
• L'applicazione su quattro livelli (lista nera / lista obbligatoria / lista bianca / conferma) è progettata per ridurre l'affaticamento da sicurezza — la maggior parte dei flussi sicuri sono pre-approvati, quindi l'agente non chiede continuamente il permesso
• L'analisi esaustiva delle tracce di Alloy ha confermato l'assenza di flussi non sicuri nel caso studio del calendario, preservando al contempo la funzionalità del compito
• L'intero approccio è esplicitamente limitato ad agenti specifici per un compito, non ad assistenti generici — gli autori riconoscono che gli agenti specializzati sono più facilmente securizzabili

Cosa funziona — e cosa no​

La mossa intellettuale è solida: prendere in prestito STPA dall'ingegneria della sicurezza critica è l'istinto giusto. A differenza delle barriere probabilistiche, questo approccio converte i requisiti in predicati sulle tracce del sistema, che possono essere verificati anziché stimati. La gerarchia di enforcement a quattro livelli è ben progettata — la distinzione tra lista nera e conferma è particolarmente importante, perché i prompt di conferma permanenti erodono la fiducia dell'utente e vengono ignorati.

Detto ciò, le limitazioni dell'articolo sono significative e per lo più non affrontate. Il problema della fiducia nei metadati viene riconosciuto ma non risolto: l'intero framework dipende dal fatto che gli sviluppatori degli strumenti etichettino accuratamente i propri strumenti. In un mercato MCP aperto dove gli strumenti di terze parti sono comuni, non esiste un meccanismo di enforcement per la correttezza delle etichette. Inoltre, la verifica formale viene eseguita su un giocattolo modello Alloy costruito a mano — dimostra la fattibilità dell'approccio, non che l'approccio possa essere applicato a sistemi reali su larga scala.

Inoltre, non vedo un argomento convincente sul perché STPA sia il metodo di analisi dei pericoli giusto rispetto, ad esempio, alla modellazione delle minacce o a HAZOP. Il caso studio del calendario è illustrativo ma banalmente piccolo. E non c'è discussione sui fornitori di strumenti malevoli che etichettano deliberatamente in modo errato le capacità — che è una superficie d'attacco reale esaminata in dettaglio nella letteratura correlata sulla sicurezza MCP (arXiv:2601.17549).

L'impostazione onesta è che questa è una proposta di progettazione con un modello formale proof-of-concept. Il duro lavoro ingegneristico — costruire il motore delle policy, testare la copertura delle etichette su strumenti diversi, misurare empiricamente il compromesso autonomia-sicurezza — viene dichiarato come lavoro futuro.

Perché questo è rilevante per l'AI finanziaria​

Gli agenti di scrittura su Beancount affrontano esattamente il modello di pericolo per cui questo articolo è progettato: la composizione di strumenti che crea rischi emergenti. Un agente che legge una voce contabile sensibile e poi pubblica un riepilogo in un registro condiviso potrebbe fare qualcosa di perfettamente ragionevole in ogni singolo passo, violando al contempo un vincolo di riservatezza visibile solo a livello di sistema. L'approccio STPA di partire dalle perdite degli stakeholder e invertirle in requisiti si mappa chiaramente sul dominio finanziario, dove le perdite sono violazioni normative, divulgazioni non autorizzate e mutazioni irreversibili della contabilità.

L'estensione MCP è direttamente rilevante perché gli strumenti Beancount sono sempre più spesso incapsulati come server MCP. Se questi strumenti possono dichiarare il loro livello di capacità e la classe di riservatezza in modo strutturato e leggibile dalla macchina, diventa possibile applicare policy sul flusso di dati al confine del protocollo, invece di sperare che l'agente si autoregolamenti. I vincoli di logica temporale — richiedere che ogni post_transaction sia preceduto da un balance_check riuscito — sono esattamente il tipo di invariante che un agente finanziario deve garantire prima di impegnare scritture.

L'elemento mancante, per ora, è che nulla di tutto ciò è stato costruito e testato. Ma come vocabolario progettuale per pensare alla sicurezza degli agenti contabili, STPA + IFC è il framework più rigoroso che abbia visto in questa letteratura.

Cosa leggere dopo​

• "Securing AI Agents with Information-Flow Control" — arXiv:2505.23643, Microsoft Research; implementa un sistema IFC concreto (Fides) con tracciamento delle macchie, valutato su AgentDojo; il complemento empirico di questo articolo
• "Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents" — arXiv:2601.17549; analizza direttamente la superficie d'attacco MCP che il framework di questo articolo mira a difendere
• "Systematic Hazard Analysis for Frontier AI using STPA" — arXiv:2506.01782; un'applicazione più recente della metodologia STPA ai sistemi AI in generale, utile per comprendere come la tecnica si adatti a scala più ampia