Technisch Overzicht: Stop Betekent Stop: Het Meten en Herstellen van de Handhavingskloof in Agent-Framework Control Primitives

1. Probleemstelling

Large Language Model (LLM) agents voeren in toenemende mate onomkeerbare acties uit op externe systemen (bijv. e-mails verzenden, betalingen autoriseren, code implementeren). Om risico's te beperken, leveren belangrijke agent-frameworks control primitives: Human-in-the-Loop (HITL) goedkeuringspoorten, run-annulering en executie-timeouts.

Praktijkrichtlijnen en documentatie van leveranciers impliceren een barrière-contract: wanneer een run wordt gepauzeerd voor goedkeuring, geannuleerd of een timeout optreedt, mag er geen gated side-effect worden uitgevoerd totdat een beslissing is genomen. Als een operator een verzoek afwijst, mag de actie niet hebben plaatsgevonden.

Het onderzoek identificeert een kritieke handhavingskloof: dit barrière-contract wordt in de praktijk niet nageleefd. De auteurs demonstreren dat in veelgebruikte frameworks de "stop"-semantiek wordt geschonden door concurrency en het ontwerp van het executiemodel. Specifiek:

• Sibling Leak: Wanneer een goedkeuringspoort een tak van een parallelle executiestap pauzeert, blijven sibling-takken doorgaan met uitvoeren. Als een sibling tijdens de pauze een side-effect uitvoert, is een daaropvolgende menselijke afwijzing niet langer in staat dit te voorkomen.
• Replay Double-Execution: Bij het hervatten van een gepauzeerde run voeren sommige frameworks stappen vanaf het begin opnieuw uit, waardoor effecten die vóór de pauze zijn uitgevoerd, een tweede keer worden uitgevoerd.
• Cancellation Orphans: Wanneer een run wordt geannuleerd, kunnen asynchrone worker-threads doorgaan tot voltooiing, waardoor effecten landen nadat het annulering signaal is waargenomen.
• Timeout Zombies: Effecten kunnen voltooien en landen nadat een timeout aan de caller is gerapporteerd.

Deze fouten zijn geen geïsoleerde bugs, maar terugkerende patronen over vier verschillende executiemodellen (Pregel/BSP, event buses, message-passing fan-out en parallel tool calls) en twee taal-runtimes (Python en Node.js).

2. Methodologie

Meting (Model-vrije Probes)

De auteurs ontwikkelden model-vrije differentiële probes om het framework-gedrag te isoleren van LLM-nondeterminisme.

• Mechanisme: Minimale workflows werden geconstrueerd waarbij de control primitive (pauze, annulering, timeout) de enige variabele was. Side-effects werden geïnstrumenteerd als appends aan een in-process event log.
• Scope: Zes open-source frameworks werden geëvalueerd (LangGraph, LlamaIndex Workflows, Microsoft Agent Framework, OpenAI Agents SDK, CrewAI, en LangGraph.js).
• Verificatie: Probes werden uitgevoerd over meerdere onafhankelijke omgevingen en framework-versies om reproduceerbaarheid te waarborgen. Een gerandomiseerde structurele sweep van 1.000 workflows op LangGraph bevestigde dat de leak rate deterministisch is op basis van de executie-topologie.

Expositie en Corroboratie

• Model Emissie: De studie mat hoe vaak frontier-modellen (GPT-4o, Claude, Gemini, DeepSeek, Llama) de specifieke "leak-triggerende" planvorm emitteren (een consequente tool call die een turn deelt met benign siblings). De ratio's varieerden per model en taak, waarbij GPT-4o de vorm in tot 14% van de runs emitteerde.
• End-to-End Executie: Live modellen werden door echte frameworks gedreven om de onvoorwaardelijke waarschijnlijkheid van een leak ($P(\text{leak})$) te meten. Resultaten toonden aan dat zodra de planvorm is geëmitteerd, het framework de effect met een waarschijnlijkheid van 1.00-leakt ($P(\text{leak} | \text{emitted}) = 1.00$).
• Publieke Corpus: Een corpus van 13 publieke incidenten uit issue trackers werd samengesteld, wat kwalitatieve corroboratie biedt dat deze fouten in de praktijk voorkomen.

Reparatie en Verificatie

De auteurs stelden SOUNDGATE voor, een environment-external effect gate.

• Ontwerp: Een kleine, taal-onafhankelijke arbiter (geïmplementeerd in Rust) die buiten de control flow van het framework staat. Elk side-effect moet worden ingediend bij SOUNDGATE voor toelating voordat uitvoering plaatsvindt.
• Contract: De reparatie steunt op een complete-mediation contract: elke side-effect pad moet zich onderwerpen aan de gate. Dit wordt afgedwongen via wrapper-discipline, statische linting en structurele kernel-level routes (network namespaces en eBPF hooks) die ongemedieerde netwerk egress weigeren.
• Formele Verificatie: De admission core werd mechanisch geverifieerd met behulp van:
  • Verus: Het bewijzen van safety properties over een sequentieel model.
  • TLA+/TLC: Uitputtende model checking van concurrente interleavings (tot $7.5 \times 10^7$ staten).
  • TLAPS: Inductieve bewijzen voor onbegrensde runs.
  • Loom: Bounded model checking van de gedeployde concurrente Rust-code.
  • Differentiele Conformance: $1.2 \times 10^7$ operaties die de gedeployde code vergeleken met het formele model met nul divergenties.

3. Belangrijkste Bijdragen

1. Meting (C1): Een karakterisering van een cross-framework handhavingskloof in geleverde control primitives. Het paper isoleert een "sibling leak" en bevestigt replay, annulering en timeout schendingen over vijf frameworks (vier onafhankelijke ontwerpen plus een cross-language port) en twee runtimes.
2. Kwalitatieve Corroboratie (C2): Bewijs dat het gevaar in de praktijk bereikbaar is. Realistische modellen emitteren de triggerende planvorm met een niet-verwaarloosbare frequentie, en live end-to-end metingen bevestigen dat $P(\text{leak} | \text{emitted}) = 1.00$. Een publieke corpus van 13 incidenten ondersteunt het bestaan van deze fouten in productie.
3. Extern Reparatiemechanisme (C3): SOUNDGATE, een environment-external gate waarvan de admission core model-geverifieerd en differentieel getest is. Het dwingt vier eigenschappen af:
   • Hold-until-decided: Voorkomt sibling leaks.
   • Reject-cancels: Zorgt ervoor dat afgewezen effecten nooit worden uitgevoerd.
   • Dedup-on-replay: Voorkomt dubbele executie bij hervatting.
   • Fence-on-cancel: Voorkomt zombie effecten na annulering.
     De reparatie werd end-to-end gedemonstreerd op alle zes de frameworks, waarbij alle vier de executiemodellen en beide runtimes werden gedekt.
4. Evaluatie (C4): Demonstratie dat de gate schendingen onderdrukt onder benign en adversariële input (inclusief prompt injection) terwijl een lage overhead (1 ms per write) en hoge throughput (12k admissions/sec in durable mode) behouden blijven.

4. Resultaten

• Schendingsratio's: In de geëvalueerde frameworks reproduceerden de sibling leak en de reject-after-effect schendingen zich in elk framework dat in staat was de configuratie uit te drukken.
• Live Leak Rates: In end-to-end experimenten met live modellen:
  • GPT-4o: 44% van de runs lekte een effect tijdens de pauze zonder de gate.
  • Claude: 9% van de runs lekte.
  • Llama 3.3: 19% van de runs lekte.
  • DeepSeek: 0% (vanwege sequentiële dispositie).
  • Gemedieerde Rate: Met SOUNDGATE daalde de leak rate naar 0% over alle modellen en runs.
• Prestaties:
  • Latency: De mediane admission cost was ~1.1 ms per write (de mediane episode latency was statistisch onveranderd).
  • Throughput: Een enkele node hield ~12.000 admissions per seconde vol in durable (WAL) mode met group commit.
  • Correctheid: Op de $\tau$-bench retail benchmark voltooide de gated agent episodes met nul false refusals van legitieme writes.

5. Betekenis en Claims

Het paper claimt dat de "stop betekent stop" assumptie, waar praktici op vertrouwen voor veiligheid, een contract mismatch is in plaats van een formele garantie in huidige agent-frameworks. De betekenis ligt in drie gebieden:

1. Empirische Karakterisering: Het paper biedt de eerste systematische, cross-framework meting van deze control-plane fouten, en bewijst dat dit geen geïsoleerde implementatiefouten zijn, maar structurele problemen voortvloeiend uit de spanning tussen parallellisme en barrière-semantiek.
2. Haalbaarheid van Externe Handhaving: Het demonstreert dat een robuuste barrière kan worden afgedwongen buiten de control flow van het framework. Door het handhavingspunt bij de tool-boundary te plaatsen (via een externe gate), kan het systeem veiligheidseigenschappen garanderen, ongeacht het onderliggende scheduler- of concurrency-model van het framework.
3. Verificatie en Adoptie: De reparatie (SOUNDGATE) is niet slechts een theoretisch voorstel; het is een geverifieerde, inzetbare component. De admission core is mechanisch geverifieerd, en de integratiekosten zijn minimaal (een ~20-regelige wrapper per framework).

Bescheidenheid van Claims:

• Het paper stelt expliciet dat het niet claimt prompt injection te fixen of te verdedigen tegen gecompromitteerde tools; het gaat uit van het "complete-mediation contract" (dat alle effecten via de gate worden gerouteerd).
• Het erkent dat op naturalistische taken huidige frontier-modellen vaak writes serialiseren, waardoor de kloof "latent" is in plaats van alomtegenwoordig. Echter, het argumenteert dat de barrière noodzakelijk is voor scenario's met adversariële input, multi-effect taken, of expliciete parallelle configuraties.
• De reparatie is voorwaardelijk op het complete-mediation contract; als een tool de gate omzeilt (bijv. via een ongewrapped pad), vervalt de garantie. Het paper adresseert dit via structurele kernel routes (eBPF/namespaces) die netwerk egress door de gate dwingen, waardoor potentiële stille leaks worden omgezet in luidruchtige beschikbaarheidsfouten.

Concluderend stelt het paper dat voor agent-systemen met onomkeerbare tool-toegang, environment-external effect gating een robuuste standaard is om te garanderen dat menselijke beslissingen (goedkeuring, afwijzing, annulering) mechanisch worden gerespecteerd, waarmee een kritieke veiligheidskloof wordt gesloten die huidige frameworks niet adresseren.