Verifizierbar sichere Tool-Nutzung für LLM-Agenten: STPA trifft auf MCP

Ich lese schon seit einiger Zeit die Literatur zu Guardrails – GuardAgent, ShieldAgent, AGrail – und sie alle verbessern die Erkennungsraten, während sie im Stillen zugeben, dass sie eigentlich nichts garantieren können. Dieses ICSE NIER 2026 Paper von Doshi et al. von der CMU und der NC State verfolgt einen anderen Ansatz: Anstatt zu fragen, wie man schlechtes Agentenverhalten zuverlässiger erkennt, fragen sie, wie man unsicheres Verhalten formal unmöglich macht. Es ist ein Positionspapier, keine empirische Studie, aber der Rahmen ist scharf genug, um eine sorgfältige Lektüre wert zu sein.

Das Paper

"Towards Verifiably Safe Tool Use for LLM Agents" (arXiv:2601.08012) von Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos und Christian Kästner schlägt eine Methodik vor, um Sicherheitsspezifikationen über die Tool-Nutzung von LLM-Agenten abzuleiten und durchzusetzen. Die zentrale Beobachtung ist, dass Risiken in Agentensystemen primär durch Tool-Komposition entstehen – nicht durch das Versagen einzelner Tools – weshalb Schutzmaßnahmen auf Komponentenebene sie nicht erfassen können. Ein Agent, der einen Kalenderkonflikt löst, könnte korrekt einen privaten Gesundheitsdatensatz abfragen und korrekt eine E-Mail senden, während er dennoch etwas Katastrophales tut: den Inhalt dieses Datensatzes an die Kollegen eines Patienten durchsickern lassen.

Die vorgeschlagene Lösung besteht aus zwei Teilen. Erstens wenden die Autoren die System-Theoretic Process Analysis (STPA) an, eine sicherheitstechnische Methode aus der Luftfahrt und der Nukleartechnik, um Gefahren auf Agentenebene zu identifizieren, Sicherheitsanforderungen abzuleiten und diese als Spezifikationen für Datenflüsse und Tool-Sequenzen zu formalisieren. Zweitens führen sie ein fähigkeitserweitertes Model Context Protocol (MCP) Framework ein, in dem jedes Tool strukturierte Metadaten deklarieren muss: Capability-Stufe (nur lesen, nur schreiben, lesen-schreiben, ausführen), Vertraulichkeitsklassifizierung und Vertrauensniveau. Die Durchsetzung ist dann in vier Stufen gegliedert: eine automatische Blockliste für nachweislich unsichere Flüsse, eine Mustlist für erforderliche Sequenzen, eine Allowlist für vorab genehmigte Operationen und eine Eskalation zur Bestätigung für mehrdeutige Fälle.

Der formale Verifizierungsschritt verwendet Alloy, ein Werkzeug für relationale Logik erster Ordnung, um den Ausführungsraum zu modellieren und erschöpfend zu prüfen, dass unter den festgelegten Richtlinien keine Sicherheitsverletzungen auftreten können, während sichere Pfade erreichbar bleiben. Dies ist das primäre „Ergebnis“ des Papers – es gibt keine Zahlen zur Benchmark-Genauigkeit, was für ein NIER-Kurzpapier zu erwarten ist.

Kernideen

• STPA definiert Agentensicherheit als ein System-Engineering-Problem neu: Verluste identifizieren, gefährliche Interaktionen zurückverfolgen, Anforderungen ableiten – bevor jeglicher Code zur Durchsetzung geschrieben wird.
• Spezifikationen unterteilen sich in zwei Arten: Informationsfluss-Einschränkungen („Event-E-Mails dürfen keine privaten Daten enthalten, die nicht dem Empfänger gehören“) und temporale Logik-Einschränkungen („jedem update_event muss ein send_email an jeden Teilnehmer folgen“).
• Die vierstufige Durchsetzung (Blocklist / Mustlist / Allowlist / Bestätigung) ist darauf ausgelegt, Sicherheitsmüdigkeit zu reduzieren – die meisten sicheren Flüsse sind vorab genehmigt, sodass der Agent nicht ständig um Erlaubnis fragt.
• Alloys erschöpfende Trace-Analyse bestätigte das Fehlen unsicherer Flüsse in der Kalender-Fallstudie bei gleichzeitigem Erhalt der Aufgabenfunktionalität.
• Der gesamte Ansatz ist explizit auf aufgabenspezifische Agenten ausgerichtet, nicht auf Allzweck-Assistenten – die Autoren räumen ein, dass spezialisierte Agenten leichter zu sichern sind.

Was Bestand hat – und was nicht

Der intellektuelle Schachzug ist solide: Die Entlehnung von STPA aus der sicherheitskritischen Technik ist der richtige Instinkt. Im Gegensatz zu probabilistischen Guardrails wandelt dieser Ansatz Anforderungen in Prädikate über System-Traces um, die verifiziert statt geschätzt werden können. Die vierstufige Durchsetzungshierarchie ist durchdacht gestaltet – insbesondere die Unterscheidung zwischen Blockliste und Bestätigung ist wichtig, da permanente Bestätigungsaufforderungen das Vertrauen der Nutzer untergraben und ignoriert werden.

Dennoch sind die Einschränkungen des Papers erheblich und bleiben weitgehend ungelöst. Das Problem des Vertrauens in Metadaten wird zwar anerkannt, aber nicht gelöst: Das gesamte Framework hängt davon ab, dass Tool-Entwickler ihre Tools korrekt kennzeichnen. In einem offenen MCP-Marktplatz, auf dem Drittanbieter-Tools üblich sind, gibt es keinen Durchsetzungsmechanismus für die Korrektheit der Kennzeichnungen. Die formale Verifizierung wird zudem an einem handgefertigten Alloy-Spielzeugmodell durchgeführt – sie demonstriert die Machbarkeit des Ansatzes, nicht jedoch, dass der Ansatz auf reale Systeme in großem Maßstab angewendet werden kann.

Ich sehe auch kein überzeugendes Argument dafür, warum STPA die richtige Methode zur Gefahrenanalyse ist im Vergleich zu beispielsweise Threat Modeling oder HAZOP. Die Kalender-Fallstudie ist illustrativ, aber trivial klein. Und es gibt keine Diskussion über böswillige Tool-Anbieter, die Fähigkeiten absichtlich falsch kennzeichnen – was eine echte Angriffsfläche darstellt, die in der verwandten MCP-Sicherheitsliteratur (arXiv:2601.17549) detailliert untersucht wird.

Die ehrliche Einordnung ist, dass es sich hierbei um einen Designvorschlag mit einem formalen Proof-of-Concept-Modell handelt. Die harte technische Arbeit – der Aufbau der Policy-Engine, das Testen der Label-Abdeckung über diverse Tools hinweg, die empirische Messung des Kompromisses zwischen Autonomie und Sicherheit – wird als zukünftige Arbeit deklariert.

Warum dies für Finance-KI wichtig ist

Beancount-Write-Back-Agenten stehen genau vor dem Gefahrenmuster, für das dieses Paper konzipiert wurde: Tool-Komposition, die emergente Risiken erzeugt. Ein Agent, der einen sensiblen Kontoeintrag liest und dann eine Zusammenfassung in einem gemeinsamen Ledger postet, macht in jedem einzelnen Schritt vielleicht etwas vollkommen Vernünftiges, während er eine Vertraulichkeitsbeschränkung verletzt, die nur auf Systemebene sichtbar ist. Der Ansatz von STPA, bei den Verlusten der Stakeholder zu beginnen und diese in Anforderungen umzuwandeln, lässt sich sauber auf den Finanzbereich übertragen, wo die Verluste regulatorische Verstöße, unbefugte Offenlegungen und irreversible Ledger-Mutationen sind.

Die MCP-Erweiterung ist direkt relevant, da Beancount-Tools zunehmend als MCP-Server bereitgestellt werden. Wenn diese Tools ihre Capability-Stufe und Vertraulichkeitsklasse strukturiert und maschinenlesbar deklarieren können, wird es möglich, Informationsfluss-Richtlinien an der Protokollgrenze durchzusetzen, anstatt zu hoffen, dass der Agent sich selbst kontrolliert. Die temporalen Logik-Einschränkungen – etwa die Forderung, dass jedem post_transaction ein erfolgreicher balance_check vorausgehen muss – sind genau die Art von Invariante, die ein Finanzagent garantieren muss, bevor er Schreibvorgänge festschreibt.

Das fehlende Puzzleteil ist vorerst, dass nichts davon gebaut und getestet wurde. Aber als Design-Vokabular, um über die Sicherheit von Ledger-Agenten nachzudenken, ist STPA + IFC das fundierteste Framework, das ich bisher in dieser Literatur gesehen habe.

Was man als Nächstes lesen sollte

• "Securing AI Agents with Information-Flow Control" — arXiv:2505.23643, Microsoft Research; implementiert ein konkretes IFC-System (Fides) mit Taint-Tracking, evaluiert auf AgentDojo; die empirische Ergänzung zu diesem Paper.
• "Breaking the Protocol: Security Analysis of the Model Context Protocol Specification and Prompt Injection Vulnerabilities in Tool-Integrated LLM Agents" — arXiv:2601.17549; analysiert direkt die MCP-Angriffsfläche, die das Framework dieses Papers verteidigen soll.
• "Systematic Hazard Analysis for Frontier AI using STPA" — arXiv:2506.01782; eine aktuellere Anwendung der STPA-Methodik auf KI-Systeme im Allgemeinen, nützlich um zu verstehen, wie die Technik skaliert.