Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach

Diese Arbeit stellt die erste Prozesskalkül-Formalisierung der Agenten-Protokolle SGD und MCP bereit, beweist deren strukturelle Bisimilarität unter einer spezifischen Abbildung, identifiziert jedoch durch die Analyse der umgekehrten Abbildung kritische Ausdruckslücken in MCP, die durch die Einführung des Typsystems MCP+ geschlossen werden, um eine vollständige behaviorale Äquivalenz und formale Verifizierbarkeit zu gewährleisten.

Das Wesentliche

Stell dir vor, du hast einen extrem klugen, aber manchmal etwas chaotischen Assistenten (den KI-Agenten). Dieser Assistent kann Dinge tun, die er nicht selbst kann, indem er auf Werkzeuge zugreift – wie einen Zug buchen, Geld überweisen oder eine E-Mail senden. Damit er diese Werkzeuge sicher und korrekt benutzt, braucht er eine Art „Bauanleitung" oder „Speisekarte", die ihm genau sagt, was er tun darf und wie.

In der Welt der KI gibt es aktuell zwei große Ansätze, wie diese Bauanleitungen erstellt werden:

1. SGD (Schema-Guided Dialogue): Ein akademischer Ansatz, der sehr detailliert ist und genau festlegt, wann eine Aktion sicher ist (z. B. „Du darfst Geld nur abheben, wenn du vorher den Kontostand geprüft hast").
2. MCP (Model Context Protocol): Ein industrieller Standard, der schnell und flexibel ist, um viele verschiedene Werkzeuge zu verbinden, aber manchmal wichtige Sicherheitsdetails vergisst.

Der Autor dieses Papers, Andreas Schlapbach, stellt sich die Frage: Sind diese beiden Ansätze eigentlich dasselbe? Und wenn ja, warum funktioniert der eine manchmal sicherer als der andere?

Hier ist die einfache Erklärung der Forschung, verpackt in eine Geschichte:

1. Die Sprache der Werkzeuge (Die formale Semantik)

Stell dir vor, SGD und MCP sind zwei verschiedene Sprachen, in denen Architekten (die Entwickler) dem Bauarbeiter (der KI) sagen, wie er bauen soll.

• Der Autor hat eine neue, universelle Grammatik (eine Art „Mathematik für Prozesse") entwickelt, um beide Sprachen zu übersetzen.
• Er hat bewiesen, dass man die Bauanleitung von SGD fast perfekt in die Sprache von MCP übersetzen kann. Das ist wie das Übersetzen eines detaillierten Kochrezepts in eine einfache Einkaufsliste.

2. Das Problem: Der Informationsverlust (Die Lücke)

Hier kommt das Wichtigste: Wenn man von SGD (dem detaillierten Rezept) zu MCP (der Einkaufsliste) wechselt, geht Information verloren.

Die Analogie:
Stell dir vor, SGD sagt: „Nimm den Hammer, aber nur, wenn du einen Schutzhelm auf hast und der Boden trocken ist."
MCP sagt nur: „Nimm den Hammer."

Der MCP-Standard vergisst drei kritische Dinge, die in SGD enthalten sind:

1. Der „Gefahren-Status": Ist diese Aktion gefährlich? (MCP weiß nicht immer, ob eine Handlung Geld kostet oder Daten löscht).
2. Der „Notfallplan": Was passiert, wenn etwas schiefgeht? (SGD hat genaue Pläne für Fehler, MCP oft nicht).
3. Die „Abhängigkeiten": Muss ich zuerst A machen, bevor ich B tue? (SGD sagt es explizit, MCP lässt es oft offen).

Ohne diese Details kann der KI-Assistent vielleicht versehentlich Geld abheben, ohne vorher zu prüfen, ob genug drauf ist, oder er weiß nicht, was er tun soll, wenn ein Server abstürzt.

3. Die Lösung: MCP+ (Das Upgrade)

Der Autor schlägt vor, MCP nicht zu verwerfen, sondern zu upgraden. Er nennt das neue System MCP+.

Er fügt fünf einfache Regeln hinzu, die MCP wieder so sicher machen wie SGD:

1. Semantische Vollständigkeit: Beschreibungen müssen nicht nur sagen was ein Werkzeug ist, sondern warum es existiert und was es bedeutet (wie ein detailliertes Etikett auf einer Medizin).
2. Klare Grenzen: Jedes Werkzeug muss ein rotes oder grünes Licht haben: „Darf ich das einfach tun (grün)" oder „Darf ich das nur mit Erlaubnis tun (rot, z. B. bei Löschaktionen)".
3. Fehler-Protokolle: Jedes Werkzeug muss eine Anleitung dabei haben: „Wenn ich scheitere, versuche es noch 3 Mal" oder „Wenn ich scheitere, rufe den Menschen an".
4. Schrittweise Enthüllung: Um Platz zu sparen, darf das Werkzeug erst eine kurze Zusammenfassung zeigen und erst auf Nachfrage die langen Details. (Wie ein Menü: Erst die Überschrift, dann die Zutatenliste).
5. Beziehungen: Es muss klar sein, welche Werkzeuge voneinander abhängen (z. B. „Ich kann nur zahlen, wenn vorher bestellt wurde").

4. Das Ergebnis: Sicherheit durch Mathematik

Mit diesen fünf Regeln (MCP+) wird MCP mathematisch gleichwertig zu SGD.
Das bedeutet:

• Man kann beweisen, dass der Assistent niemals einen gefährlichen Befehl ausführt, ohne vorher zu prüfen.
• Man kann beweisen, dass der Assistent niemals in einer Endlosschleife stecken bleibt.
• Man kann beweisen, dass der Assistent niemals versehentlich Daten stiehlt (durch „Tool Poisoning", also manipulierte Beschreibungen).

Warum ist das wichtig?

Bisher verließen wir uns darauf, dass die KI „gute Absichten" hat oder dass wir sie viel testen. Aber Tests finden nicht alle Fehler.
Dieser Ansatz macht Sicherheit zu einer mathematischen Eigenschaft. Es ist wie ein Sicherheitsgurt im Auto: Man muss nicht hoffen, dass er funktioniert, man kann beweisen, dass er es tut, solange die Regeln eingehalten werden.

Zusammenfassend:
Der Autor hat bewiesen, dass die beiden großen KI-Standards eigentlich dasselbe Ziel haben, aber einer (MCP) ohne die richtigen Sicherheitsregeln zu riskant ist. Durch das Hinzufügen von fünf klaren Regeln (MCP+) schaffen wir ein System, in dem KI-Agenten nicht nur clever, sondern auch nachweisbar sicher sind. Das ist der Grundstein für eine Zukunft, in der KI sicher unsere Gelder verwaltet, Krankenhäuser steuert oder Züge lenkt.

Technische Zusammenfassung

1. Problemstellung

Der rasante Einsatz von Large Language Model (LLM) Agents, die externe Tools aufrufen können, hat eine kritische Lücke in der Sicherheitsverifikation aufgedeckt. Während diese Agents komplexe Workflows orchestrieren, fehlen formale Methoden, um ihre Korrektheit, Sicherheit und Verhaltensweisen zu beweisen.

Zwei dominante Paradigmen für die Integration von Agents und Tools existieren derzeit:

1. Schema-Guided Dialogue (SGD): Ein Forschungsframework, das es Modellen ermöglicht, neue APIs ohne Nachtraining (Zero-Shot) basierend auf natürlichen Sprachbeschreibungen von Schemata zu nutzen.
2. Model Context Protocol (MCP): Ein Industriestandard (von Anthropic), der eine N-zu-M-Integration durch standardisierte Primitive (Tools, Resources, Prompts) ermöglicht.

Obwohl beide Paradigmen auf maschinenlesbaren Schemata basieren, ist ihre formale Beziehung unbekannt. Es ist unklar, ob sie äquivalent sind, welche Eigenschaften bei Transformationen erhalten bleiben und wo spezifische Lücken in der Ausdruckskraft (Expressivität) eines der beiden Frameworks liegen.

2. Methodik

Die Arbeit verwendet den $\pi$-Kalkül (eine Prozessalgebra für nebenläufige, kommunizierende Systeme) als formale Grundlage, um SGD und MCP zu modellieren.

• Formalisierung: Beide Protokolle werden als Prozesse mit definierter Syntax, operationeller Semantik und markierten Übergangssystemen (LTS) dargestellt.
• Bisimulation: Die Äquivalenz wird durch den Nachweis einer starken Bisimulation ($\sim$) zwischen den Zustandsräumen der beiden Systeme geprüft.
• Mapping-Funktionen:
  • $\Phi$: Eine Abbildung von SGD-Prozessen auf MCP-Prozesse.
  • $\Phi^{-1}$: Eine inverse Abbildung von MCP zurück zu SGD.
• Typsystem-Erweiterungen: Um die gefundenen Lücken zu schließen, werden fünf Design-Prinzipien als Typsystem-Erweiterungen formalisiert, was zu einem neuen Kalkül namens MCP+ führt.

3. Wichtige Beiträge und Ergebnisse

A. Formale Semantik und Äquivalenzbeweis

Das Paper liefert die erste formale Semantik für SGD und MCP. Es wird bewiesen, dass SGD und MCP unter der Abbildung $\Phi$ strukturell bisimilar sind ($SGD \sim MCP$). Das bedeutet, dass ein SGD-Intent und das entsprechende MCP-Tool das gleiche beobachtbare Verhalten zeigen, solange die Abbildung angewendet wird.

B. Analyse der Umkehrabbildung und Identifikation von Lücken

Die Analyse der inversen Abbildung $\Phi^{-1}$ zeigt, dass diese partiell und verlustbehaftet ist. MCP kann nicht vollständig in SGD übersetzt werden, da folgende kritische Informationen in MCP fehlen oder nicht maschinenlesbar kodiert sind:

1. Transaktionsflag: Ob ein Tool eine Transaktion ist (z. B. erfordert Bestätigung), geht verloren.
2. Passive Kontexte: Das MCP-Primitive Resource (schreibgeschützte Daten) hat kein Äquivalent in SGD.
3. Dynamische Entdeckung: Die Fähigkeit zur Laufzeit-Verhandlung von Fähigkeiten (Capability Negotiation) fehlt in SGD.
4. Fehlerbehandlung: Strukturierte Fehler-Wiederherstrategien sind in SGD nicht explizit kodiert.

C. Die fünf Prinzipien und MCP+

Um eine vollständige Äquivalenz ($SGD \cong MCP+$) zu erreichen, werden fünf Prinzipien als Typsystem-Erweiterungen für MCP definiert:

1. Semantische Vollständigkeit (Semantic Completeness): Beschreibungen müssen nicht nur Typen, sondern auch den Zweck und Beispiele enthalten (gemessen an der semantischen Dichte).
2. Explizite Aktionsgrenzen (Explicit Action Boundaries): Tools müssen explizit kennzeichnen, ob sie Nebenwirkungen (Schreiben/Löschen) haben und eine Genehmigung erfordern.
3. Dokumentation von Fehlermodi (Failure Mode Documentation): Erwartete Fehlerzustände und Wiederherstellungsstrategien müssen deklariert sein.
4. Kompatibilität für progressive Offenlegung (Progressive Disclosure): Unterstützung von kurzen Zusammenfassungen für die Auswahl und detaillierten Beschreibungen für die Ausführung (zur Token-Optimierung).
5. Deklaration von Tool-Beziehungen (Inter-Tool Relationship Declaration): Explizite Angabe von Abhängigkeiten zwischen Tools (z. B. "Tool A erfordert Tool B").

Mit diesen Erweiterungen wird MCP+ definiert. Es wird bewiesen, dass $MCP+ \cong SGD$ gilt, d. h., es existiert eine Bijektion zwischen den beiden Systemen, die alle semantischen Eigenschaften erhält.

D. Sicherheitsgarantien

Die Arbeit leitet Sicherheitsinvarianten aus dem Prozesskalkül ab:

• Fähigkeitseinschränkung (Capability Confinement): Durch Kanalbeschränkung ($\nu$) im $\pi$-Kalkül wird verhindert, dass Tools unbefugten Zugriff auf Ressourcen erlangen.
• Verhinderung von Tool-Vergiftung: Ein Typsystem unterscheidet zwischen Daten (Strings) und Code, wodurch verhindert wird, dass schädliche Anweisungen in Tool-Beschreibungen injiziert werden.
• Ordnung von Genehmigungen und Abhängigkeiten: Es wird formal bewiesen, dass bei Tools mit Nebenwirkungen eine Genehmigung vor der Ausführung erfolgen muss und abhängige Tools in der korrekten Reihenfolge ausgeführt werden.

4. Bedeutung und Fazit

Dieses Paper stellt den ersten formalen Grundstein für verifizierte Agentensysteme dar. Es transformiert Agenten-Protokolle von ad-hoc Konventionen in mathematisch verifizierbare Systeme.

• Theoretischer Wert: Es klärt die konzeptionelle Konvergenz von SGD und MCP und zeigt auf, dass MCP ohne Erweiterungen weniger ausdrucksstark ist als SGD.
• Praktische Relevanz: Für kritische Anwendungen (Finanzen, Gesundheitswesen, Infrastruktur) bietet das Framework die Möglichkeit, Sicherheitsgarantien (z. B. "Keine Überweisung ohne Kontostand-Check") formal zu beweisen, anstatt sich auf Tests oder Prompt-Engineering zu verlassen.
• Zukunftsausblick: Die Arbeit ebnet den Weg für mechanisierte Beweise (z. B. in Isabelle/HOL), probabilistische Analysen von LLM-Entscheidungen und die Verifikation von Multi-Agenten-Choreografien.

Zusammenfassend etabliert die Arbeit Schema-Qualität als eine beweisbare Sicherheitseigenschaft und liefert die mathematische Basis für die nächste Generation autonomer, sicherer Software-Systeme ("Software 3.0").