Alignment Contracts for Agentic Security Systems

1. Probleemstelling

De opkomst van Agentic Security Systems—autonome agenten aangedreven door Large Language Models (LLM's) die beveiligingstests kunnen plannen, uitvoeren en valideren (bijvoorbeeld penetration testing)—creëert een kritiek asymmetrisch controleprobleem.

• Het Dilemma: Deze agenten moeten sterke offensieve capaciteiten behouden (bijvoorbeeld het exploiteren van kwetsbaarheden, het onderzoeken van systemen) binnen een geautoriseerd bereik, terwijl ze diezelfde capaciteiten strikt moeten ontzeggen buiten dat bereik (bijvoorbeeld het aanvallen van niet-geautoriseerde doelen, het exfiltreren van data naar tegenstanders).
• Het Falen van Bestaande Veiligheidsmaatregelen: Huidige veiligheidsmechanismen (zoals prompt-filtering, intentie-classificatie of alomvattende weigering) zijn ontoereikend omdat:
  1. Ze vaak vertrouwen op het afleiden van de intentie van de agent, wat onbetrouwbaar is tegenover adversarial prompt injection of model backdoors.
  2. Ze ontberen een formele, eersteklas definitie van de "grens" tussen geautoriseerde en niet-geautoriseerde acties gebaseerd op waarneembare effecten.
  3. Ze niet kunnen garanderen dat een agent, zelfs als deze is gecompromitteerd of gemanipuleerd, geen schadelijke acties zal uitvoeren als de actie zelf technisch "toegestaan" is door een los beleid.

De kernuitdaging is het afdwingen van een verantwoordelijkheidsgrens waarbij het systeem garandeert dat alle gerealiseerde effecten (netwerkverzoeken, bestandstoegang, procesuitvoering) binnen door de operator gedefinieerde beperkingen blijven, ongeacht de interne staat van de LLM of adversarial manipulatie.

2. Methodologie: Alignment Contracts

De auteurs stellen Alignment Contracts voor, een formeel raamwerk voor het specificeren en afdwingen van gedragsbeperkingen over waarneembare effectsporen.

A. Kernconcepten

• Effectalfabet ($\Sigma$): Een eindige verzameling van waarneembare effectklassen (bijvoorbeeld NET voor netwerk, FS voor bestandssysteem, EXEC voor procesuitvoering).
• Gebeurtenis: Een tuple $e = \langle \sigma, p, t, i \rangle$ die een effectklasse, parameters (bijvoorbeeld bestemmings-IP, methode), tijdstempel en agent-ID voorstelt.
• Spoor: Een eindige reeks gebeurtenissen.
• Het Contract ($C$): Een tuple die definieert:
  • Bereik ($S$): Welke doelen zijn geautoriseerd.
  • Toegestane/Verboden Effecten ($E_{allow}, E_{forbid}$): Specifieke actieklassen die zijn toegestaan of verbannen.
  • Budgetten ($B$): Beperkingen op middelen (bijvoorbeeld maximaal 10.000 verzoeken).
  • Openbaarmakingsbeleid ($D$): Waar gevoelige data (kwetsbaarheden, referenties) naartoe kan stromen.
  • Kosten en Stromen: Boekhoudkundige functies voor middelen en data-extractie.

B. Het Afdwingingsmechanisme

Het systeem vertrouwt op een Referentiemonitor die werkt onder de Aanneming van Effectwaarneembaarheid (EOA):

1. Mediatie: Alle externe effecten moeten voordat ze worden uitgevoerd, door een mediatie-laag (bijvoorbeeld een getypeerde tool-wrapper, HTTP-proxy of kernel-hook) passeren.
2. Toelaatbaarheidscontrole: Voor elke voorgestelde gebeurtenis $e$ en huidig spoorprefix $\tau$, controleert de monitor of $Adm(e, \tau, C)$ geldt. Dit omvat het verifiëren van:
   • Het doel bevindt zich binnen het bereik.
   • Het effect is toegestaan en niet verboden.
   • Budgetten zijn niet overschreden.
   • Openbaarmakingsstromen zijn geautoriseerd.
3. Actie: Als het toelaatbaar is, wordt de gebeurtenis toegelaten; anders wordt deze geweigerd. De monitor werkt puur op waarneembare data en negeert de interne redenering van de LLM.

C. Formele Grondslagen

• Veiligheidseigenschap: Contractvoldoening wordt gedefinieerd als een veiligheidseigenschap over eindige sporen. Als een contract wordt geschonden, bestaat er een eindig "slecht prefix" dat de schending aantoont.
• Mechanisatie: De kerntheorema's zijn geverifieerd met Lean 4, een formeel bewijshulpmiddel, waarmee de logische geldigheid van het raamwerk wordt gewaarborgd.

3. Belangrijkste Bijdragen

1. Formeel Model: Definitie van Alignment Contracts als tuples over een eindig effectalfabet met spoorgebaseerde semantiek. Het paper bewijst de Eindig-Slecht-Prefix-Witness Eigenschap, waarmee wordt gegarandeerd dat schendingen in eindige tijd detecteerbaar zijn.
2. Geluidheid van Afdwinging: Onder de EOA bewijzen de auteurs dat elke agent (zelfs adversarial, met prompt injection of backdoored) alleen contract-voldoende sporen produceert als zijn effecten volledig gemedieerd zijn. Dit verplaatst het vertrouwen van de niet-vertrouwde LLM naar de kleine, controleerbare afdwingingsbarrière.
3. Contractalgebra:
   • Verfijning ($C' \sqsubseteq C$): Een mechanisme om strengere contracten te creëren (smaller bereik, strakkere budgetten) die de geluidheid behouden.
   • Eenrichtingscompositie: Regels voor het combineren van contracten (bijvoorbeeld het samenvoegen van organisatorisch beleid met engagement-bereik) met bewezen geluidheidsgaranties.
   • Beslisbaarheid: Het paper stelt vast dat toelaatbaarheidscontrole beslisbaar en computationeel efficiënt is ($O(|Res|)$ online met caching).
4. Aanpassingsschema: Een raamwerk voor het afhandelen van dynamische systeemwijzigingen (bijvoorbeeld het opstarten van sub-agenten, het wisselen van tools) door "contract-bewarende" aanpassingsregels te definiëren.
5. Onmogelijkheidsresultaten: Het paper schetst formeel de grenzen van de aanpak:
   • Onbeslisbaarheid: Statische pre-toelatingsanalyse van of een tool ooit een verboden effect probeert, is onbeslisbaar voor Turing-volledige talen.
   • Omzeilingslimieten: Als een tool de mediatie-laag omzeilt (bijvoorbeeld via kernel-modules of zijkanalen), stort de geluidheidsgarantie in.
   • Waarneembaarheidsgrenzen: Verborgen kanalen (payload-steganografie, timing-kanalen) en niet-gemodelleerde effecten vallen buiten het bestek van het theorema.

4. Resultaten en Evaluatie

• Theoretische Garanties: Het Lean 4-artifact verifieert dat als de Referentiemonitor correct is geïmplementeerd en de EOA geldt, het systeem geluid is. Het gedrag van de LLM is irrelevant voor de garantie; alleen het gerealiseerde effect telt.
• Casestudy (Web Pentesting): Het raamwerk is geïmplementeerd voor een scenario van web-penetration testing. Het modelleerde succesvol beperkingen zoals:
  • "Alleen HTTP GET/HEAD op *.example.com."
  • "Geen bestandssysteemoperaties."
  • "Maximaal 10.000 verzoeken."
  • "Rapporten alleen naar het dashboard."
  • De monitor blokkeerde correct pogingen om data te exfiltreren naar evil.com of niet-geautoriseerde domeinen te benaderen, zelfs wanneer de agent "prompt-injected" was om dit te doen.
• Complexiteit: De kern toelaatbaarheidscontrole blijkt in praktische implementaties constant-tijd per gebeurtenis te zijn (onder de aanname van kleine, vaste middelenverzamelingen), wat het levensvatbaar maakt voor afdwinging tijdens runtime.

5. Betekenis

Dit paper vertegenwoordigt een paradigmaverschuiving in het beveiligen van AI-agenten:

• Van Intentie naar Effect: Het schuift weg van het proberen om de interne intentie van de LLM te "alignen" (wat moeilijk en broos is) naar het afdwingen van beperkingen op waarneembare effecten (wat verifieerbaar is).
• Formeel Vertrouwen: Door het gebruik van gemecaniseerde bewijzen, biedt het een wiskundig rigoureuze garantie dat een agent zijn contract niet kan schenden als de mediatie-laag veilig is. Dit reduceert de Trusted Computing Base (TCB) tot de monitor en de mediatiegrens, de LLM daarin uitgesloten.
• Praktische Toepasbaarheid: Het raamwerk is ontworpen voor real-world offensieve beveiligingsworkflows en biedt een manier om krachtige autonome agenten veilig in te zetten zonder angst voor collaterale schade of datalekken.
• Duidelijke Grenzen: Door expliciet te stellen wat het systeem niet kan garanderen (bijvoorbeeld inspectie van payload-inhoud, timing-kanalen), voorkomt het over-reliance op de technologie en leidt het toekomstige engineering-inspanningen naar het sluiten van die specifieke gaten.

Kortom, Alignment Contracts bieden het eerste formele, beslisbare en mechanisch geverifieerde raamwerk om te garanderen dat agentic security systemen strikt binnen geautoriseerde grenzen opereren, waardoor de "black box" van LLM-redenering wordt omgezet in een "white box" van afdwingbare effectbeperkingen.