Sintesi Tecnica: Linguaggio di Descrizione delle Policy per l'Autorizzazione mediante Programmazione Basata sulla Logica

Problema

I moderni sistemi informativi sono sempre più ampi e complessi, rendendo impossibile eradicare tutte le vulnerabilità. Di conseguenza, viene adottata la strategia della Difesa in Profondità (Defense-in-Depth), che si basa su una rigorosa partizione multi-livello dei sistemi per ritardare gli attacchi e localizzare i danni. L'efficacia di questa strategia dipende dal controllo degli accessi obbligatorio (MAC) a grana fine. Tuttavia, l'implementazione del MAC a grana fine presenta una sfida significativa: il volume di regole di controllo degli accessi richieste diventa enorme.

Le implementazioni esistenti, come SELinux, descrivono le policy elencando direttamente le singole regole di controllo degli accessi. All'aumentare della granularità, la descrizione della policy cresce enormemente, rendendo difficile comprendere il comportamento complessivo della policy senza strumenti di verifica dedicati. Inoltre, i linguaggi di descrizione delle policy convenzionali (ad esempio, SDSI, SPKI, PolicyMaker) spesso mancano della flessibilità necessaria per definire predicati specifici dell'applicazione o per gestire la complessità strutturale richiesta per una gestione efficiente delle policy in scenari di difesa multi-livello. Il problema centrale è la mancanza di un linguaggio di descrizione delle policy in grado di descrivere concisamente enormi policy mantenendo la correttezza logica e supportando l'astrazione strutturale.

Metodologia

Gli autori propongono un Linguaggio di Descrizione delle Policy basato sulla programmazione basata sulla logica, specificamente implementato utilizzando Datalog (un sottoinsieme di Prolog). La metodologia prevede tre componenti principali:

1. Design del Linguaggio

Il linguaggio definisce una policy come un insieme di Dichiarazioni Dichiarative (DS) e consente Query di Autorizzazione (Q).

• Sintassi: Il linguaggio utilizza una sintassi simile all'inglese, basata sulla logica dei predicati. I predicati chiave includono:
  • is permitted to / is forbidden to: Definisce i diritti di accesso tra un soggetto e un oggetto.
  • moves to: Definisce le transizioni di stato di un soggetto innescate da un'operazione.
  • inherits: Permette agli attributi di ereditare i permessi da altri attributi.
• Semantica Formale: Il linguaggio definisce regole di inferenza formali per derivare i fatti:
  • Regola di Inferenza (a): Deriva automaticamente fatti specifici dalle dichiarazioni condizionali quando i termini variabili vengono sostituiti con costanti.
  • Regola di Inferenza (b): Deriva automaticamente i permessi per un attributo che eredita da un altro attributo, consentendo la propagazione gerarchica dei permessi.
• Implementazione: Il linguaggio viene tradotto in programmi Datalog, le dichiarazioni dichiarative diventano clausole Datalog e le query di autorizzazione vengono valutate rispetto a queste clausole utilizzando il sistema Datalog XSB, che supporta la semantica ben fondata e i predicati tabulati per prevenire loop infiniti.

2. Metodi di Descrizione Strutturale

Per affrontare la complessità della descrizione delle policy, gli autori propongono due tecniche strutturali:

• Gerarchizzazione degli Elementi: Similmente al Controllo degli Accessi Basato sui Ruoli (RBAC), questo raggruppa le regole di controllo degli accessi sotto attributi astratti (es. ruoli). Le regole sono definite per variabili (es. x tagged MANAGER) ed espandibili quando soggetti specifici vengono assegnati a tali attributi.
• Strutturazione delle Procedure di Autorizzazione: Similmente al Controllo degli Accessi Basato sulle Mansioni (TBAC), questo subroutinizza le procedure di autorizzazione. Il predicato moves to permette al linguaggio di astrarre le transizioni di stato (es. il passaggio da PREPARE_PHASE a COMMIT_PHASE), permettendo di descrivere concisamente flussi di transazione complessi.

3. Strategia di Valutazione

Gli autori hanno costruito un sistema sperimentale per valutare il linguaggio:

• Validità: Hanno tradotto l'esistente policy di SELinux nel linguaggio proposto. Hanno confrontato le decisioni di autorizzazione (Vettori di Accesso) generate dal meccanismo del kernel originale di SELinux rispetto a quelle generate dall'implementazione Datalog attraverso 15.100.162 combinazioni di query.
• Espressività: Hanno confrontato il numero di righe di codice sorgente e il numero di pagine di elenco della policy originale di SELinux rispetto alle implementazioni in stile C-List e stile ACL del linguaggio proposto.

Contributi Chiave

1. Un Linguaggio di Policy Basato sulla Logica: La proposta di un linguaggio che esprime le regole di controllo degli accessi come programmi logici, consentendo l'ereditarietà degli attributi e la strutturazione di tipo subroutine delle procedure di autorizzazione.
2. Semantica Formale e Regole di Inferenza: La definizione di semantica formale e regole di inferenza che permettono la derivazione automatica dei permessi basata su gerarchie di attributi e transizioni condizionali.
3. Implementazione Datalog: Un'implementazione concreta utilizzando XSB che traduce il linguaggio di policy in un sistema basato su regole capace di gestire lo scambio di dati su larga scala.
4. Astrazione Strutturale per il MAC: Un metodo per descrivere i modelli di controllo degli accessi (come RBAC e TBAC) in modo strutturale, riducendo la necessità di elencare esplicitamente ogni singola regola.

Risultati

• Validità: Nel confronto con SELinux, il linguaggio proposto ha prodotto risposte di autorizzazione identiche (Vettori di Accesso) per il 99,95% delle 15.100.162 query testate. Il restante ~0,05% di discrepanze è stato attribuito a query che coinvolgevano contesti generati dinamicamente durante l'operazione del sistema, che dipendono da meccanismi di passaggio di argomenti esterni alla logica centrale di autorizzazione. Gli autori concludono che il linguaggio opera in modo logicamente corretto.
• Espressività (Riduzione della Descrizione):
  • La policy originale di SELinux conteneva 6.524 righe e 133 pagine.
  • Il linguaggio proposto (stile C-List) ha ridotto questo a 335 righe e 95 pagine.
  • Il linguaggio proposto (stile ACL) ha ridotto questo a 356 righe e 96 pagine.
  • Ciò rappresenta una riduzione di circa il 95% nelle righe di codice sorgente e del 28% nelle pagine di elenco.

Significato e Rivendicazioni

L'articolo sostiene che il linguaggio proposto affronta con successo la complessità della descrizione delle policy nelle strategie di difesa multi-livello. Elevando il livello di astrazione attraverso la programmazione logica, il linguaggio consente:

• Descrizione Concisa della Policy: Riducendo drasticamente il volume di codice richiesto per descrivere policy complesse, rendendole più gestibili.
• Correttezza Logica: Garantendo che le decisioni di autorizzazione siano derivate matematicamente e logicamente, facilitando la verifica.
• Flessibilità: Consentendo la descrizione di condizioni dinamiche (es. "essere fermato" o "essere contaminato") e transizioni di stato complesse che sono difficili da esprimere in linguaggi a elenco di regole piatte.

Gli autori osservano che, sebbene il linguaggio migliori la panoramica della policy nel suo insieme, la leggibilità delle singole regole può essere inferiore rispetto alla designazione diretta degli elementi (come in SELinux). Pertanto, il linguaggio è particolarmente adatto a scenari che coinvolgono un gran numero di procedure di accesso condivise o un numero enorme di regole che richiedono una strutturazione flessibile, piuttosto che per la definizione rigorosa di un piccolo numero di regole non correlate.

Il lavoro futuro, come delineato dagli autori, include la realizzazione di applicazioni quali la verifica della policy come condizione per il controllo degli accessi, la gestione dei cambiamenti delle regole tramite meta-regole e l'integrazione del sistema di elaborazione Datalog direttamente nel kernel del sistema operativo per migliorare le prestazioni e la sicurezza.