Verifieerbaar Veilig Toolgebruik voor LLM-agenten: STPA ontmoet MCP

Ik lees al een tijdje de guardrail-literatuur — GuardAgent, ShieldAgent, AGrail — en ze verbeteren allemaal de detectiepercentages terwijl ze stilletjes toegeven dat ze eigenlijk niets kunnen garanderen. Dit ICSE NIER 2026-paper van Doshi et al. van CMU en NC State kiest een andere invalshoek: in plaats van te vragen hoe we slecht gedrag van agenten betrouwbaarder kunnen detecteren, vragen ze hoe we onveilig gedrag formeel onmogelijk kunnen maken. Het is een position paper, geen empirische studie, maar de inkadering is scherp genoeg om aandachtig te lezen.

Het paper

"Towards Verifiably Safe Tool Use for LLM Agents" (arXiv:2601.08012) door Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos en Christian Kästner stelt een methodologie voor om veiligheidsspecificaties af te leiden en af te dwingen voor het toolgebruik door LLM-agenten. De kernobservatie is dat risico's in agentsystemen primair voortkomen uit tool-compositie — niet uit het falen van individuele tools — waardoor beveiligingen op componentniveau ze niet kunnen opvangen. Een agent die een agendaconflict oplost, zou correct een privé medisch dossier kunnen opvragen en correct een e-mail kunnen verzenden, terwijl hij toch iets catastrofaals doet: de inhoud van dat dossier lekken naar de collega's van een patiënt.

De voorgestelde oplossing bestaat uit twee delen. Ten eerste passen de auteurs System-Theoretic Process Analysis (STPA) toe, een veiligheidstechnische methode uit de luchtvaart en nucleaire systemen, om gevaren op agent-niveau te identificeren, veiligheidseisen af te leiden en deze te formaliseren als specificaties voor datastromen en tool-sequenties. Ten tweede introduceren ze een voor capaciteiten uitgebreid Model Context Protocol (MCP) framework waarin elke tool gestructureerde metadata moet declareren: capaciteitsniveau (alleen-lezen, alleen-schrijven, lezen-schrijven, uitvoeren), vertrouwelijkheidsclassificatie en vertrouwensniveau. De handhaving is vervolgens gestructureerd in vier lagen: een automatische blocklist voor bewijsbaar onveilige stromen, een mustlist voor vereiste sequenties, een allowlist voor vooraf goedgekeurde operaties, en escalatie naar bevestiging voor ambigue gevallen.

De formele verificatiestap gebruikt Alloy, een relationele logica-tool van de eerste orde, om de executieruimte te modelleren en uitputtend te controleren of er onder het vastgestelde beleid geen veiligheidsschendingen kunnen optreden, terwijl veilige sporen bereikbaar blijven. Dit is het primaire "resultaat" van het paper — er zijn geen benchmark-accuratiecijfers, wat verwacht mag worden voor een kort NIER-paper.

Belangrijkste ideeën

• STPA herdefinieert de veiligheid van agenten als een systems engineering-probleem: identificeer verliezen, herleid ze via gevaarlijke interacties, leid vereisten af — nog voordat er handhavingscode wordt geschreven.
• Specificaties vallen uiteen in twee soorten: beperkingen op de informatiestroom ("e-mails over evenementen mogen geen privégegevens bevatten die niet van de ontvanger zijn") en temporele logica-beperkingen ("elke update_event moet worden gevolgd door send_email naar elke aanwezige").
• De handhaving in vier lagen (blocklist / mustlist / allowlist / bevestiging) is ontworpen om beveiligingsmoeheid te verminderen — de meeste veilige stromen zijn vooraf goedgekeurd, zodat de agent niet constant om toestemming vraagt.
• De uitputtende sporenanalyse van Alloy bevestigde de afwezigheid van onveilige stromen in de agenda-casestudy, terwijl de functionaliteit van de taken behouden bleef.
• De hele aanpak is expliciet gericht op taakspecifieke agenten, niet op assistenten voor algemeen gebruik — de auteurs erkennen dat gespecialiseerde agenten haalbaarder te beveiligen zijn.

Wat overeind blijft — en wat niet

De intellectuele zet is solide: het lenen van STPA uit de veiligheidskritische techniek is het juiste instinct. In tegenstelling tot probabilistische guardrails zet deze aanpak vereisten om in predicaten over systeemsporen, die geverifieerd kunnen worden in plaats van geschat. De hiërarchie van handhaving in vier lagen is doordacht ontworpen — vooral het onderscheid tussen de blocklist en bevestiging is belangrijk, omdat permanente bevestigingsvragen het vertrouwen van de gebruiker uithollen en worden genegeerd.

Dat gezegd hebbende, de beperkingen van het paper zijn aanzienlijk en blijven grotendeels onbesproken. Het probleem van vertrouwen in metadata wordt erkend maar niet opgelost: het hele framework is afhankelijk van tool-ontwikkelaars die hun tools nauwkeurig labelen. In een open MCP-marktplaats waar tools van derden gebruikelijk zijn, is er geen handhavingsmechanisme voor de juistheid van labels. De formele verificatie is ook uitgevoerd op een handmatig opgesteld Alloy-speelgoedmodel — het toont de haalbaarheid van de aanpak aan, niet dat de aanpak op schaal kan worden toegepast op echte systemen.

Ik zie ook geen overtuigend argument waarom STPA de juiste methode voor gevarenanalyse is vergeleken met bijvoorbeeld threat modeling of HAZOP. De agenda-casestudy is illustratief maar triviaal klein. En er is geen discussie over kwaadwillende tool-aanbieders die opzettelijk capaciteiten verkeerd labelen — wat een reëel aanvalsoppervlak is dat de gerelateerde MCP-beveiligingsliteratuur (arXiv:2601.17549) in detail onderzoekt.

De eerlijke inkadering is dat dit een ontwerpplan is met een proof-of-concept formeel model. Het zware engineeringwerk — het bouwen van de policy engine, het testen van de labeldekking over diverse tools, het empirisch meten van de afweging tussen autonomie en veiligheid — wordt aangemerkt als toekomstig werk.

Waarom dit belangrijk is voor finance AI

Beancount write-back agenten worden geconfronteerd met precies het gevarenpatroon waar dit paper voor ontworpen is: tool-compositie die opkomende risico's creëert. Een agent die een gevoelige rekeningboeking leest en vervolgens een samenvatting naar een gedeeld grootboek stuurt, kan bij elke individuele stap iets volkomen redelijks doen, terwijl hij een vertrouwelijkheidsbeperking schendt die alleen op systeemniveau zichtbaar is. De STPA-aanpak om te beginnen bij de verliezen van belanghebbenden en deze om te keren naar vereisten, sluit naadloos aan op het financiële domein, waar de verliezen bestaan uit overtredingen van regelgeving, ongeoorloofde openbaarmakingen en onomkeerbare grootboekmutaties.

De MCP-uitbreiding is direct relevant omdat Beancount-tooling steeds vaker wordt verpakt als MCP-servers. Als die tools hun capaciteitsniveau en vertrouwelijkheidsklasse op een gestructureerde, machineleesbare manier kunnen declareren, wordt het mogelijk om het informatiestroombeleid af te dwingen aan de protocolgrens, in plaats van te hopen dat de agent zichzelf controleert. De temporele logica-beperkingen — bijvoorbeeld de eis dat elke post_transaction moet worden voorafgegaan door een succesvolle balance_check — zijn precies het soort invarianten dat een financiële agent moet kunnen garanderen voordat hij schrijfacties uitvoert.

Het ontbrekende stuk is voorlopig dat niets hiervan nog gebouwd en getest is. Maar als ontwerptaal om na te denken over de veiligheid van grootboekagenten, is STPA + IFC het meest principiële framework dat ik in deze literatuur ben tegengekomen.

Wat nu te lezen

• "Securing AI Agents with Information-Flow Control" — arXiv:2505.23643, Microsoft Research; implementeert een concreet IFC-systeem (Fides) met taint-tracking, geëvalueerd op AgentDojo; de empirische aanvulling op dit paper.
• "Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents" — arXiv:2601.17549; analyseert direct het MCP-aanvalsoppervlak waartegen het framework in dit paper bedoeld is te verdedigen.
• "Systematic Hazard Analysis for Frontier AI using STPA" — arXiv:2506.01782; een recentere toepassing van de STPA-methodologie op AI-systemen in het algemeen, nuttig om te begrijpen hoe de techniek schaalt.