Ús d'eines verificablement segur per a agents de LLM: STPA es troba amb MCP

He estat llegint la literatura sobre barreres de seguretat (guardrails) des de fa temps — GuardAgent, ShieldAgent, AGrail — i tots milloren les taxes de detecció mentre admeten en silenci que en realitat no poden garantir res. Aquest article de l'ICSE NIER 2026 de Doshi et al. de la CMU i la NC State adopta una perspectiva diferent: en comptes de preguntar com detectar comportaments dolents dels agents de manera més fiable, es pregunten com fer que el comportament insegur sigui formalment impossible. És un document de posició, no un estudi empíric, però el plantejament és prou agut com perquè valgui la pena llegir-lo amb atenció.

L'article

«Towards Verifiably Safe Tool Use for LLM Agents» (arXiv:2601.08012) d'Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos i Christian Kästner proposa una metodologia per derivar i fer complir especificacions de seguretat sobre l'ús d'eines d'agents de LLM. L'observació central és que els riscos en els sistemes d'agents sorgeixen principalment de la composició d'eines — no de fallades d'eines individuals —, de manera que les salvaguardes a nivell de component no poden detectar-los. Un agent que resol un conflicte de calendari podria consultar correctament un registre de salut privat i enviar correctament un correu electrònic, però tot i així fer una cosa catastròfica: filtrar el contingut d'aquest registre als col·legues d'un pacient.

La solució proposada consta de dues parts. Primer, els autors apliquen l'Anàlisi de Processos Teòric del Sistema (STPA), un mètode d'enginyeria de seguretat de sistemes aviàtics i nuclears, per identificar perills a nivell d'agent, derivar requisits de seguretat i formalitzar-los com a especificacions sobre els fluxos de dades i les seqüències d'eines. Segon, introdueixen un marc del Model Context Protocol (MCP) millorat amb capacitats on cada eina ha de declarar metadades estructurades: nivell de capacitat (només lectura, només escriptura, lectura-escriptura, execució), classificació de confidencialitat i nivell de confiança. L'execució s'estructura llavors en quatre nivells: llista de bloqueig automàtica per a fluxos demostrablement insegurs, llista de deures per a seqüències obligatòries, llista permesa per a operacions preaprovades i escalada de confirmació per a casos ambigus.

El pas de verificació formal utilitza Alloy, una eina de lògica relacional de primer ordre, per modelar l'espai d'execució i comprovar exhaustivament que, sota les polítiques establertes, no es poden produir violacions de seguretat mentre les traces segures romanen accessibles. Aquest és el «resultat» principal de l'article; no hi ha xifres de precisió de referència, cosa que és d'esperar per a un article curt de NIER.

Idees clau

• L'STPA replanteja la seguretat de l'agent com un problema d' enginyeria de sistemes: identificar pèrdues, rastrejar-les a través d'interaccions perilloses, derivar requisits — abans d'escriure cap codi d'execució.
• Les especificacions es divideixen en dos tipus: restriccions de flux d'informació («els correus electrònics d'esdeveniments no han d'incloure dades privades que no pertanyin al destinatari») i restriccions de lògica temporal («cada update_event ha d'anar seguit de send_email a cada assistent»).
• L'aplicació de quatre nivells (llista de bloqueig / llista de deures / llista permesa / confirmació) està dissenyada per reduir la fatiga de seguretat: la majoria dels fluxos segurs estan preaprovats, de manera que l'agent no demana permís constantment.
• L'anàlisi exhaustiva de traces d'Alloy va confirmar l'absència de fluxos insegurs en l'estudi de cas del calendari mantenint la funcionalitat de la tasca.
• Tot l'enfocament està explícitament orientat a agents específics de tasques, no a assistents d'ús general; els autors reconeixen que els agents especialitzats són més factibles d'assegurar.

Què se sosté — i què no

El moviment intel·lectual és encertat: manllevar l'STPA de l'enginyeria de seguretat crítica és l'instint correcte. A diferència de les barreres de seguretat probabilístiques, aquest enfocament converteix els requisits en predicats sobre traces del sistema, que es poden verificar en lloc d'estimar-se. La jerarquia d'aplicació de quatre nivells està dissenyada amb cura; la distinció entre llista de bloqueig i confirmació és especialment important, perquè les sol·licituds de confirmació permanents erosionen la confiança de l'usuari i s'acaben ignorant.

Dit això, les limitacions de l'article són significatives i la majoria queden sense abordar. El problema de la confiança en les metadades es reconeix però no es resol: tot el marc depèn de si els desenvolupadors d'eines etiqueten les seves eines correctament. En un mercat obert d'MCP on les eines de tercers són habituals, no hi ha cap mecanisme per fer complir la correcció de les etiquetes. La verificació formal també es realitza sobre un model de joguina d'Alloy fet a mà; demostra la viabilitat de l'enfocament, no que l'enfocament es pugui aplicar a sistemes reals a escala.

Tampoc veig un argument convincent de per què l'STPA és el mètode d'anàlisi de perills adequat en comparació amb, per exemple, el modelatge d'amenaces o l'HAZOP. L'estudi de cas del calendari és il·lustratiu però trivialment petit. I no hi ha cap discussió sobre proveïdors d'eines adversaris que etiquetin malament les capacitats deliberadament, la qual cosa és una superfície d'atac real que la literatura de seguretat MCP relacionada (arXiv:2601.17549) examina detalladament.

El plantejament honest és que es tracta d'una proposta de disseny amb un model formal de prova de concepte. El treball dur d'enginyeria — construir el motor de polítiques, provar la cobertura d'etiquetes en diverses eines, mesurar empíricament el compromís entre autonomia i seguretat — es declara com a treball futur.

Per què això és important per a la IA financera

Els agents d'escriptura de Beancount s'enfronten exactament al patró de perill per al qual està dissenyat aquest article: la composició d'eines que crea riscos emergents. Un agent que llegeix una entrada de compte sensible i després publica un resum en un llibre major compartit podria estar fent una cosa perfectament raonable en cada pas individual mentre viola una restricció de confidencialitat que només és visible a nivell de sistema. L'enfocament de l'STPA de partir de les pèrdues de les parts interessades i invertir-les en requisits s'adapta perfectament al domini de les finances, on les pèrdues són violacions regulatòries, revelacions no autoritzades i mutacions irreversibles del llibre major.

L'extensió de l'MCP és directament rellevant perquè les eines de Beancount s'estan embolicant cada vegada més com a servidors MCP. Si aquestes eines poden declarar el seu nivell de capacitat i classe de confidencialitat de manera estructurada i llegible per màquina, es fa possible fer complir les polítiques de flux de dades al límit del protocol en lloc d'esperar que l'agent s'autocontrolli. Les restriccions de lògica temporal — requerir que cada post_transaction vagi precedida d'una balance_check exitosa — són exactament el tipus d'invariant que un agent de finances ha de garantir abans d'executar escriptures.

La peça que falta, per ara, és que res d'això s'ha construït ni provat. Però com a vocabulari de disseny per pensar en la seguretat dels agents del llibre major, STPA + IFC és el marc més basat en principis que he vist en aquesta literatura.

Què llegir a continuació

• «Securing AI Agents with Information-Flow Control» — arXiv:2505.23643, Microsoft Research; implementa un sistema IFC concret (Fides) amb seguiment de taques (taint tracking), avaluat a AgentDojo; el complement empíric d'aquest article.
• «Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents» — arXiv:2601.17549; analitza directament la superfície d'atac MCP que el marc d'aquest article pretén defensar.
• «Systematic Hazard Analysis for Frontier AI using STPA» — arXiv:2506.01782; una aplicació més recent de la metodologia STPA als sistemes d'IA en general, útil per entendre com escala la tècnica.