Verification of Robust Properties for Access Control Policies

1. Il Problema: Verifica di Politiche Incomplete e Iterative

Il lavoro affronta una limitazione fondamentale nei metodi esistenti di verifica delle politiche di controllo degli accessi (es. XACML).

• Assunzione di Completezza: Gli approcci tradizionali (basati su modelli teorici come SMT, BDD o logica dei modelli stabili) richiedono che la politica sia completa e fully determined (completamente specificata) prima di poter verificare una proprietà di sicurezza.
• Realtà dello Sviluppo: In pratica, le politiche di sicurezza sono sviluppate in modo iterativo, composte da componenti mantenuti da parti diverse e estese man mano che le strutture organizzative evolvono. Spesso è necessario imporre vincoli di sicurezza prima che le assegnazioni di ruoli o le decisioni di delega siano finalizzate.
• Il Gap: Gli strumenti attuali non possono ragionare su ciò che la struttura inferenziale di una politica garantisce indipendentemente da come verranno risolte le decisioni pendenti. Se una decisione pendente viene risolta o la politica viene estesa, la verifica deve essere rifatta da zero, rendendo il processo non composizionale e intrattabile per politiche in rapida evoluzione.

2. Metodologia: Semantica di Estensione della Base (Base-Extension Semantics)

L'autore introduce un nuovo quadro semantico basato sulla semantica di estensione della base (proof-theoretic semantics), spostando il focus dalla verità in un modello statico al comportamento inferenziale attraverso le estensioni della politica.

Il Giudizio di Supporto (Support Judgment)

Il concetto centrale è il giudizio di supporto: $\Vdash_P \phi$.
Questo afferma che la politica $P$ possiede la proprietà robusta $\phi$, indipendentemente da come le decisioni pendenti verranno risolte o da come la politica verrà estesa in futuro.

La semantica è definita attraverso quattro connettivi logici che catturano diversi aspetti del ragionamento robusto:

1. Implicazione Robusta ($\Rightarrow$): $\Vdash_P \phi \Rightarrow \psi$ significa che ogni estensione della politica che supporta $\phi$ supporta anche $\psi$. È un condizionale inferenziale, non materiale.
2. Disgiunzione Robusta ($\oplus$): $\Vdash_P \phi \oplus \psi$ non richiede che una delle due alternative sia attualmente derivabile. Afferma che, in ogni estensione futura, se una delle alternative fosse risolta, le stesse conseguenze di sicurezza seguirebbero. Questo permette di verificare vincoli (es. separazione dei compiti) anche quando l'assegnazione del ruolo (es. chi sarà il chair) è ancora pendente.
3. Congiunzione Robusta ($\otimes$): $\Vdash_P \phi \otimes \psi$ richiede che le conseguenze derivate dalla presenza simultanea di $\phi$ e $\psi$ siano garantite. Questo è cruciale per rilevare fallimenti che emergono solo quando più vincoli interagiscono, che la verifica isolata potrebbe non cogliere.
4. Negazione Robusta ($\neg$): Definita come incompatibilità strutturale. $\Vdash_P \neg \phi$ (o $\phi \Rightarrow 0$) significa che l'esistenza di $\phi$ in qualsiasi estensione coerente corromperebbe la politica (portando a un stato $0$ in cui ogni atomo è derivabile, rendendo il sistema di controllo incoerente). Non è semplice "non derivabilità", ma una garanzia che $\phi$ non possa mai sorgere senza distruggere il sistema.

Proprietà Chiave: Monotonicità

Un risultato strutturale fondamentale è il Teorema di Monotonicità (Proposizione 6): se una proprietà robusta è verificata per una politica $P$, essa rimane verificata per qualsiasi estensione $Q \supseteq P$.

• Implicazione: La verifica è composizionale. Non è necessario rieseguire la verifica completa quando la politica viene aggiornata; basta verificare le nuove regole o le proprietà direttamente influenzate.

3. Risultati Tecnici e Riduzione Computazionale

La sfida principale era che la definizione di supporto quantifica universalmente su tutte le possibili estensioni della politica (un insieme infinito). L'autore dimostra che questo problema è risolvibile computazionalmente.

• Riduzione alla Ricerca di Prova: Il giudizio semantico $\Vdash_P \phi$ viene ridotto a una ricerca di prova (proof-search) in un linguaggio di programmazione logica del secondo ordine.
• Codifica degli Obiettivi: Vengono definiti mappature $\lceil \cdot \rceil$ che traducono le formule di proprietà robuste in obiettivi (goals) per un interprete logico:
  • La disgiunzione robusta e la congiunzione robusta vengono codificate usando quantificatori di secondo ordine su atomi atomici ($\forall X$).
  • L'uso di variabili eigen (fresche) nel meccanismo di prova uniforme realizza operativamente la quantificazione universale su tutte le estensioni possibili.
• Teorema di Correttezza e Completezza (Teorema 12):
  $$\Vdash_P \phi \iff P \vdash_O \lceil \phi \rceil$$
  Questo teorema stabilisce che la verifica della proprietà robusta è equivalente all'esecuzione di un obiettivo in un programma logico finito. Il processo è quindi finitario, decidibile ed eseguibile.

4. Contributi Principali

1. Identificazione del Problema: Formalizzazione della "verifica di proprietà robuste" come problema di semantica dimostrativa per le politiche di controllo degli accessi.
2. Quadro Semantico: Definizione del giudizio di supporto $\Vdash_P \phi$ con connettivi specifici (implicazione, disgiunzione, congiunzione, negazione) che soddisfano i requisiti di inferenzialità, composizionalità e finitezza.
3. Riduzione Computazionale: Dimostrazione che la verifica robusta, nonostante la sua definizione semantica infinita, si riduce alla ricerca di prova in un linguaggio di programmazione logica del secondo ordine, fornendo una procedura di verifica pratica.
4. Teorema di Monotonicità: Prova che le proprietà verificate persistono sotto estensione, abilitando la verifica composizionale.

5. Significato e Impatto

• Cambiamento di Paradigma: Il lavoro sposta la verifica dalla fase di "policy deployment" (politica completa) alla fase di "policy development" (politica in evoluzione). Permette di garantire la sicurezza prima che le decisioni siano finalizzate.
• Efficienza Operativa: Grazie alla proprietà di monotonicità, i costi di verifica non crescono con la dimensione totale della politica, ma solo con le modifiche apportate. Questo risolve il problema della ridondanza nei cicli di sviluppo iterativo.
• Complementarità: Questo approccio non sostituisce strumenti esistenti come Zelkova o Margrave (che verificano istanze complete), ma li integra. Permette di "certificare" quali proprietà possono essere portate avanti senza riesecuzione quando la politica viene estesa, riducendo il carico sui solver SMT o BDD.
• Fondamenti Teorici: Collega la sicurezza informatica alla semantica dimostrativa e alla teoria delle categorie (modelli di presheaf), offrendo una base teorica solida per il ragionamento su sistemi dinamici e distribuiti.

In sintesi, il paper propone un metodo formale per garantire che le politiche di sicurezza siano strutturalmente robuste, permettendo agli amministratori di verificare vincoli critici in presenza di incertezza e di mantenere tali garanzie man mano che il sistema evolve, senza dover ricominciare da capo ad ogni modifica.