Sintesi Tecnica: Verifica Probabilistica Efficiente e Solida per Agenti AI

Definizione del Problema

L'impiego di agenti AI basati su Large Language Model (LLM) in ambienti digitali complessi introduce rischi di sicurezza critici, in particolare quando gli agenti possiedono l'accesso programmatico a interfacce di sistema come terminali e file system. Sebbene il monitoraggio runtime tramite monitor di riferimento offra una soluzione per l'applicazione di policy di sicurezza, gli approcci esistenti sono limitati a policy deterministiche. In scenari pratici, gli agenti spesso si affidano a componenti a monte (ad esempio, rilevatori di PII, strumenti di redazione o classificatori) che producono output probabilistici con tassi di errore intrinseci.

Gli attuali monitor deterministici gestiscono questa ambiguità applicando soglie locali per convertire gli output probabilistici in decisioni binarie. Questa discretizzazione crea un compromesso fragile tra sicurezza e utilità:

• Soglie elevate rischiano di non bloccare azioni dannose (falsi negativi).
• Soglie basse rischiano di bloccare azioni sicure (falsi positivi).
• Assunzioni di Indipendenza: Le tecniche di inferenza probabilistica standard (ad esempio, il Weighted Model Counting) spesso assumono che i fatti di base siano mutuamente indipendenti. Nelle impostazioni agentiche, questa assunzione è frequentemente invalida; ad esempio, il fallimento di uno strumento di redazione su un file può essere perfettamente correlato al suo fallimento su un altro a causa di contenuti condivisi o del comportamento dello strumento stesso. Fare affidamento sull'indipendenza può portare a una grave sottostima del rischio durante l'uso di catene di strumenti multi-step.

Il documento affronta la necessità di un framework di verifica che preservi il contesto probabilistico continuo, gestisca correlazioni arbitrarie tra i predicati senza assumere l'indipendenza e fornisca limiti superiori rigorosi e solidi sulle probabilità di violazione della policy in tempo reale.

Metodologia

Il framework proposto modella l'esecuzione dell'agente come un problema di ottimizzazione distribuito robustamente su una traiettoria di esecuzione. La metodologia consiste in quattro fasi principali:

1. Modellazione Datalog Probabilistica

La traccia di esecuzione dell'agente viene compilata in un programma Datalog dove:

• Fatti di Base ($F$): Rappresentano le osservazioni iniziali dell'ambiente (ad esempio, "il file A contiene PII") parametrizzati da limiti di probabilità marginale $[\ell_f, u_f]$ derivati dai tassi di errore empirici degli strumenti.
• Regole ($R$): Codificano la logica di transizione di stato (ad esempio, propagazione dei dati, fusione, declassificazione) come regole intensionali.
• Grafo di Derivazione: La traccia di esecuzione viene tradotta in un Grafo Aciclico Diretto (DAG) dove i nodi rappresentano i fatti e gli archi rappresentano le applicazioni delle regole. Gli autori dimostrano che ogni esecuzione di policy Datalog può essere riscritta in modo tale che ogni fatto derivato dipenda da al massimo due fatti genitore (arità $\le 2$), permettendo alla logica di essere espressa tramite polinomi multilineari.

2. Formulazione di Ottimizzazione Esatta (Limite Teorico)

Per calcolare la probabilità peggiore di una violazione della policy, gli autori formulano un programma lineare (LP) esatto sullo spazio delle misure di probabilità congiunta $\mu$.

• Obiettivo: Massimizzare la probabilità di raggiungere uno stato non sicuro (ad esempio, dati sensibili che raggiungono un destinatario esterno).
• Vincoli:
  • Coerenza Strutturale: La misura $\mu$ deve assegnare probabilità zero agli stati che violano la logica di transizione deterministica delle regole Datalog.
  • Limiti Marginali: La misura deve rispettare i limiti inferiori e superiori noti dei fatti di base iniziali.
  • Robustezza Distribuita: Fondamentalmente, la formulazione non effettua assunzioni sulla distribuzione congiunta (indipendenza, correlazione positiva/negativa) a meno che non sia esplicitamente specificato. Essa ricerca la "peggiore" distribuzione congiunta coerente con le marginali.
• Limitazione: Questo LP esatto è di dimensioni esponenziali ($2^{|V_F|}$) ed è computazionalmente intrattabile per il monitoraggio in tempo reale.

3. Relax con Programmazione Semidefinita (SDP)

Per ottenere l'efficienza a runtime, gli autori introducono una relax con Programmazione Semidefinita (SDP) di dimensione polinomiale.

• Tracciamento dei Momenti: Invece di ottimizzare sull'intera distribuzione congiunta, l'SDP traccia solo i momenti di primo e secondo ordine (aspettative e correlazioni a coppie) della distribuzione dello stato.
• Linearizzazione: I termini quadratici non convessi derivanti dai vincoli di covarianza vengono linearizzati utilizzando involucri di McCormick sugli intervalli marginali.
• Classi di Correlazione: Il framework supporta vincoli di correlazione espliciti (Correlati Positivamente, Correlati Negativamente, Indipendenti) tra specifici predicati, consentendo all'ottimizzazione di stringere i limiti quando la conoscenza del dominio è disponibile.
• Solidità: Gli autori dimostrano che la relax SDP fornisce un limite superiore solido ($R^*_{SDP} \ge R^*$) sul rischio di esecuzione reale. Ciò garantisce che il monitor non blocchi mai una violazione, preservando le garanzie di sicurezza anche se occasionalmente blocca azioni sicure (riducendo l'utilità).

4. Applicazione a Runtime

Il limite superiore calcolato viene confrontato con una soglia di sicurezza globale $\tau$. Se il rischio stimato supera $\tau$, il monitor di riferimento blocca la chiamata allo strumento proposta; altrimenti, permette l'esecuzione.

Contributi Chiave

1. Modello di Verifica Probabilistica: Identificazione dei rischi di sicurezza nei motori deterministici per ambienti ambigui e introduzione di un modello per la verifica probabilistica che evita la binarizzazione prematura.
2. Formalizzazione del Rischio Esatto: Modellazione delle traiettorie multi-step degli agenti tramite grafi di derivazione Datalog e formalizzazione del calcolo del rischio di violazione della policy nel caso peggiore come un problema di ottimizzazione esatta su misure congiunte.
3. Relax SDP Solida: Introduzione di una relax SDP di dimensione polinomiale che traccia i momenti di secondo ordine per approssimare efficientemente il rischio. Il documento dimostra formalmente che questa relax è un limite superiore stretto sul rischio di esecuzione, garantendo la solidità senza assunzioni di indipendenza.
4. Validazione Empirica: Valutazione attraverso benchmark di agenti terminali (Intercode-NL2Bash, ATBench) e task di vulnerabilità side-channel (Praline), dimostrando un miglioramento del trade-off sicurezza-utilità rispetto allo stato dell'arte.

Risultati

Il framework è stato valutato contro tre baseline: Praline (un motore di inferenza Datalog all'avanguardia con gestione della correlazione), campionamento Monte Carlo (che assume una stretta indipendenza) e un motore Deterministico con soglie locali.

• Trade-off Sicurezza-Utilità: L'approccio SDP ha superato costantemente le baseline in termini di Area Sotto la Curva (AUC) per il trade-off utilità-sicurezza.
  • vs Monte Carlo: Monte Carlo ha ottenuto un'alta utilità ma ha fallito sulla sicurezza (alti falsi negativi) perché le assunzioni di indipendenza hanno sottostimato il rischio nel caso peggiore, specialmente quando gli input erano positivamente correlati.
  • vs Praline: Sebbene Praline abbia ottenuto una sicurezza perfetta, ha sofferto di timeout del solver e di limiti ampi sulle task complesse, portando a un eccesso di falsi positivi (bassa utilità). L'approccio SDP ha mantenuto una sicurezza perfetta pur ottenendo un'utilità maggiore e una latenza inferiore nei benchmark terminali.
  • vs Deterministico: I motori deterministici hanno mostrato prestazioni scarse in entrambi i parametri, spesso fallendo nel bloccare azioni insicure o bloccando azioni sicure a causa della perdita di informazioni derivante dal thresholding.
• Latenza: La relax SDP ha dimostrato scalabilità polinomiale. Nei benchmark Intercode e ATBench, l'SDP è stata significativamente più veloce (ad esempio, ~221ms vs ~1015ms per Praline su Intercode). In task side-channel complesse con molti vincoli di correlazione, la latenza SDP è aumentata ma è rimasta prevedibile, evitando le latenze della coda esponenziale e i timeout associati al ragionamento SMT esatto.
• Sensibilità alla Correlazione: Gli esperimenti hanno mostrato che all'aumentare delle correlazioni di input, l'assunzione di indipendenza (Monte Carlo) ha portato a un calo netto dell'utilità (aumento dei falsi positivi) perché sovrastimava il rischio in contesti correlati dove il vero limite del caso peggiore era più stretto. Il framework SDP si è adattato efficacementamente a questi vincoli.

Significato e Rivendicazioni

Il documento sostiene di fornire un cambio di paradigma dalla verifica deterministica a quella probabilistica per gli agenti AI. Il suo significato primario risiede nel colmare il divario tra solidità (garanzie di sicurezza rigorose) e trattabilità (prestazioni in tempo reale) in presenza di ambiguità.

• Robustezza: Utilizzando l'ottimizzazione distribuita robustamente, il framework garantisce che le garanzie di sicurezza siano valide indipendentemente dalle correlazioni sconosciute tra i predicati, un requisito critico per le implementazioni di agenti nel mondo reale dove i fallimenti degli strumenti possono essere accoppiati.
• Praticità: La relax SDP consente l'applicazione di policy di sicurezza complesse e multi-step con input probabilistici continui senza l'intrattabilità computazionale dell'inferenza esatta o i rischi di sicurezza delle assunzioni di indipendenza.
• Fondamenta: Il lavoro stabilisce una base scalabile per la sicurezza degli agenti autonomi che operano in ambienti ambigui, andando oltre le difese euristiche verso l'applicazione formale e probabilistica.

Gli autori riconoscono alcune limitazioni, specificamente che i limiti di rischio possono degradare (convergere a 1.0) su orizzonti di esecuzione molto lunghi con alti gradi di fusione dei fatti, e che l'approccio dipende dalla semantica predefinita degli strumenti, il che può essere complesso per script arbitrari generati dagli agenti. Tuttavia, il framework è presentato come un passo significativo verso la sicurezza degli agenti scalabile e rigorosa.