Perché alcune violazioni di finalità richiedono di confrontare le esecuzioni degli agenti

Un controllo di autorizzazione che verifica separatamente ogni chiamata a uno strumento può far rispettare una regola su ciò che un agente può divulgare per la finalità di un compito?

Il paper pone questa domanda perché una sequenza di azioni consentite può violare una regola globale e perché, per valutare la finalità, potrebbe essere necessario confrontare più di un’esecuzione.

Il paper formalizza un punto cieco nei controlli sulle chiamate agli strumenti e introduce AL-Synth per generare esempi in cui le regole valide per l’intero compito sfuggono ai controlli azione per azione.

Un controllo che esamina una chiamata a uno strumento alla volta può far rispettare una regola sulla finalità? Gli autori formalizzano una violazione come due esecuzioni con lo stesso compito e lo stesso contesto autorizzato rispetto alla finalità, ma con divulgazioni diverse.

Dimostrano che ciascuna esecuzione è conforme se considerata da sola: un monitor che ne vede una sola e vuole evitare falsi allarmi deve quindi non rilevare la coppia.

AL-Synth genera esempi di questo tipo a partire da modelli simbolici di agenti. Nei test con giudici, otto modelli su nove non hanno mai bloccato il witness quando valutavano le azioni una alla volta, mentre otto lo hanno identificato in tutte le 30 ripetizioni quando hanno visto entrambe le esecuzioni.

Questo sostiene la conclusione formale: rilevare questo tipo di violazione richiede di confrontare le esecuzioni oppure di accettare falsi allarmi.

Il limite formale si applica quando la finalità è davvero relazionale rispetto a esecuzioni autorizzate localmente. Il sintetizzatore è convalidato su piccoli modelli simbolici, non attraverso uno studio di scalabilità, e i compiti sono sintetici.

Separatamente, la campagna con i giudici valuta modelli nel ruolo di giudici, gli studi con agenti attivi riguardano due famiglie di modelli e la copertura delle protezioni è dedotta dai design pubblicati.