Technische Samenvatting: Efficiënte en Betrouwbare Probabilistische Verificatie voor AI-agenten

Probleemstelling

De inzet van op Large Language Models (LLM) gebaseerde AI-agenten in complexe digitale omgevingen introduceert kritieke beveiligingsrisico's, met name wanneer agenten programmeerbare toegang hebben tot systeeminterfaces zoals terminals en bestandssystemen. Hoewel runtime-monitoring via reference monitors een oplossing biedt voor het afdwingen van beveiligingsbeleid, zijn bestaande benaderingen beperkt tot deterministische beleidsregels. In praktische scenario's vertrouwen agenten vaak op upstream-componenten (bijv. PII-detectoren, redactietools of classificatietools) die probabilistische outputs produceren met inherente foutpercentages.

Huidige deterministische monitors gaan met deze ambiguïteit om door lokale drempelwaarden toe te passen om probabilistische outputs om te zetten in binaire beslissingen. Deze discretisering creëert een kwetsbare afweging tussen beveiliging en bruikbaarheid:

• Hoge drempelwaarden riskeren het niet blokkeren van schadelijke acties (false negatives).
• Lage drempelwaarden riskeren het onterecht blokkeren van veilige acties (false positives).
• Onafhankelijkheidsaannames: Standaard probabilistische inferentietechnieken (bijv. Weighted Model Counting) gaan er vaak vanuit dat basisfeiten wederzijds onafhankelijk zijn. In agentische settings is deze aanname vaak ongeldig; bijvoorbeeld kan het falen van een redactietool op één bestand perfect gecorreleerd zijn met het falen op een ander bestand vanwege gedeelde inhoud of toolgedrag. Het vertrouwen op onafhankelijkheid kan leiden tot een ernstige onderschatting van het risico tijdens meerstaps tool-ketens (tool chaining).

Het artikel adresseert de behoefte aan een verificatiekader dat continue probabilistische context behoudt, willekeurige correlaties tussen predicaten afhandelt zonder onafhankelijkheid te veronderstellen, en rigoureuze, betrouwbare bovengrenzen biedt voor de waarschijnlijkheid van beleidsschendingen in real-time.

Methodologie

Het voorgestelde kader modelleert de executie van de agent als een distributionally robust optimization problem over een executietraject. De methodologie bestaat uit vier hoofdfasen:

1. Probabilistische Datalog-modellering

Het executietraject van de agent wordt gecompileerd naar een Datalog-programma waarbij:

• Basisfeiten ($F$): De initiële omgevingsobservaties vertegenwoordigen (bijv. "bestand A bevat PII"), geparametriseerd door marginale waarschijnlijkheidsgrenzen $[\ell_f, u_f]$ afgeleid van empirische tool-foutpercentages.
• Regels ($R$): De logica van de toestandsveranderingen coderen (bijv. datapropagatie, samenvoeging, declassificatie) als intentionele regels.
• Derivatiegrafiek: Het executietraject wordt vertaald naar een Directed Acyclic Graph (DAG) waarbij knopen feiten vertegenwoordigen en randen regeltoepassingen vertegenwoordigen. De auteurs bewijzen dat elke Datalog-beleidsexecutie zodanig herschreven kan worden dat elk afgeleid feit afhankelijk is van maximaal twee ouderfeiten (arity $\le 2$), waardoor de logica via multilineaire polynomen uitgedrukt kan worden.

2. Exacte Optimalisatieformulering (Theoretische Grens)

Om de slechtst denkbare waarschijnlijkheid van een beleidsschending te berekenen, formuleren de auteurs een exact lineair programma (LP) over de ruimte van gezamenlijke waarschijnlijkheidsmaten $\mu$.

• Doelstelling: Maximaliseer de waarschijnlijkheid van het bereiken van een onveilige toestand (bijv. gevoelige gegevens die een externe ontvanger bereiken).
• Constraints:
  • Structurele Consistentie: De maat $\mu$ moet een kans van nul toekennen aan toestanden die de deterministische transitielogica van de Datalog-regels schenden.
  • Marginale Grenzen: De maat moet voldoen aan de bekende lagere en hogere grenzen van de initiële basisfeiten.
  • Distributional Robustness: Cruciaal is dat de formulering geen aannames doet over de gezamenlijke distributie (onafhankelijkheid, positieve/negatieve correlatie), tenzij expliciet gespecificeerd. Het zoekt naar de "worst-case" gezamenlijke distributie die consistent is met de marginalen.
• Beperking: Dit exacte LP is exponentieel groot ($2^{|V_F|}$) en computationeel onhandelbaar voor real-time monitoring.

3. Semidefinite Programming (SDP) Relaxatie

Om runtime-efficiëntie te bereiken, introduceren de auteurs een polynomiaal omvangrijke Semidefinite Programming (SDP) relaxatie.

• Moment Tracking: In plaats van te optimaliseren over de volledige gezamenlijke distributie, houdt de SDP alleen de eerste- en tweede-orde momenten (verwachtingen en paar-correlaties) van de toestandsdistributie bij.
• Linearisatie: Niet-convexe kwadratische termen die voortkomen uit covariantie-constraints worden lineair gemaakt met behulp van McCormick envelopes over de marginale intervallen.
• Correlatieklassen: Het kader ondersteunt expliciete correlatie-constraints (positief gecorreleerd, negatief gecorreleerd, onafhankelijk) tussen specifieke predicaten, waardoor de optimalisatie de grenzen kan aanscherpen wanneer domeinkennis beschikbaar is.
• Soundness (Betrouwbaarheid): De auteurs bewijzen dat de SDP-relaxatie een sound upper bound ($R^*_{SDP} \ge R^*$) levert op de ware executierisico. Dit zorgt ervoor dat de monitor een schending nooit onderblokkeert, wat de beveiligingsgaranties behoudt, zelfs als het incidenteel te veel blokkeert (wat de bruikbaarheid vermindert).

4. Runtime Handhaving

De berekende bovengrens wordt vergeleken met een globale veiligheidsdrempel $\tau$. Als het geschatte risico $\tau$ overschrijdt, blokkeert de reference monitor de voorgestelde tool-call; anders wordt de executie toegestaan.

Belangrijkste Bijdragen

1. Probabilistisch Verificatiemodel: Identificatie van beveiligingsrisico's in deterministische engines voor ambigue omgevingen en de introductie van een model voor probabilistische verificatie dat voortijdige binarisatie vermijdt.
2. Exacte Risicoformalisering: Het modelleren van meerstaps agent-trajecten via Datalog-derivatiegrafieken en het formaliseren van de berekening van het worst-case beleidsschendingsrisico als een exact optimalisatieprobleem over gezamenlijke maten.
3. Sound SDP Relaxatie: Introductie van een polynomiaal omvangrijke SDP-relaxatie die tweede-orde momenten bijhoudt om risico efficiënt te benaderen. Het artikel bewijst formeel dat deze relaxatie een strikte bovengrens is op het executierisico, wat beveiliging garandeert zonder onafhankelijkheidsaannames.
4. Empirische Validatie: Evaluatie via terminal-agent benchmarks (Intercode-NL2Bash, ATBench) en side-channel kwetsbaarheids-taken (Praline), waarbij een verbeterde security-utility trade-off wordt aangetoond vergeleken met de huidige stand van de techniek.

Resultaten

Het framework werd geëvalueerd tegen drie baselines: Praline (een state-of-the-art Datalog inference engine met correlatieverwerking), Monte Carlo sampling (uitgaande van strikte onafhankelijkheid) en een Deterministische engine met lokale drempelwaarden.

• Security-Utility Trade-off: De SDP-benadering presteerde consequent beter dan de baselines wat betreft de Area Under the Curve (AUC) voor de utility-security trade-off.
  • vs. Monte Carlo: Monte Carlo behaalde een hoge utility maar faalde op beveiliging (hoge false negatives) omdat onafhankelijkheidsaannames het worst-case risico onderschatten, vooral wanneer inputs positief gecorreleerd waren.
  • vs. Praline: Hoewel Praline perfecte beveiliging bereikte, leed het onder solver-timeouts en losse grenzen op complexe taken, wat leidde tot excessieve false positives (lage utility). De SDP-benadering behield perfecte beveiliging terwijl het een hogere utility en lagere latentie bereikte op terminal benchmarks.
  • vs. Deterministisch: Deterministische engines vertoonden slechte prestaties in beide metrieken, waarbij ze vaak ofwel onveilige acties niet blokkeerden, of veilige acties blokkeerden door informatieverlies door thresholding.
• Latentie: De SDP-relaxatie demonstreerde polynomiale schaalbaarheid. Op Intercode en ATBench benchmarks was SDP aanzienlijk sneller (bijv. ~221ms vs ~1015ms voor Praline op Intercode). Op complexe side-channel taken met veel correlatie-constraints nam de SDP-latentie toe, maar bleef voorspelbaar, waardoor de exponentiële tail-latencies en timeouts van exact SMT-gebaseerd redeneren werden vermeden.
• Correlatiegevoeligheid: Experimenten toonden aan dat naarmate de input-correlaties toenamen, de onafhankelijkheidsaanname (Monte Carlo) leidde tot een scherpe daling in utility (toename van false positives) omdat het het risico overschatte in gecorreleerde settings waar de ware worst-case grens nauwer was. Het SDP-framework paste zich effectief aan deze constraints aan.

Betekenis en Claims

Het artikel claimt een paradigmaverschuiving te bieden van deterministische naar probabilistische verificatie voor AI-agenten. De primaire betekenis ligt in het overbruggen van de kloof tussen soundness (rigoureuze beveiligingsgaranties) en tractability (real-time prestaties) in de aanwezigheid van ambiguïteit.

• Robuustheid: Door gebruik te maken van distributionally robust optimization, zorgt het framework ervoor dat de beveiligingsgaranties standhouden ongeacht onbekende correlaties tussen predicaten, een cruciale vereiste voor real-world agent-deployments waar tool-failures gekoppeld kunnen zijn.
• Praktische toepasbaarheid: De SDP-relaxatie maakt de handhaving van complexe, meerstaps beveiligingspolicies met continue probabilistische inputs mogelijk zonder de computationele onhandelbaarheid van exacte inferentie of de veiligheidsrisico's van onafhankelijkheidsaannames.
• Fundament: Het werk legt een schaalbare basis voor het beveiligen van autonome agenten die opereren in ambigue omgevingen, waarbij men verder gaat dan heuristische defensies naar formele, probabilistische handhaving.

De auteurs erkennen beperkingen, specifelijk dat risicogrenzen kunnen verslechteren (convergeren naar 1.0) over zeer lange executiehorizonten met een hoge graad van fact-merging, en dat de aanpak afhankelijk is van vooraf gedefinieerde tool-semantiek, wat uitdagend kan zijn voor willekeurige scripts gegenereerd door agenten. Desalniettemin wordt het framework gepresenteerd als een significante stap naar rigoureuze, schaalbare agent-beveiliging.