Verifica di configurazioni di sistema

Il servizio permette di verificare la correttezza della configurazione di un sistema di rete rispetto alle politiche di sicurezza (Access Control List) definite per regolare gli accessi alle risorse del sistema stesso da parte dei suoi utenti. Il servizio di basa su tre input, ovvero tre modelli:

(i.) il modello del sistema, con i dettagli sugli ambienti fisici, sui dispositivi, sui servizi presenti e sulle loro interconnessioni logiche e fisiche; (ii.) il modello delle policy (ovvero le Access Control List) che specifica chi puo' accedere a quale risorsa; (iii.) il modello degli utenti nel sistema, ovvero il loro stato iniziale (collocazione fisica e bagaglio di conoscenze).

Il servizio esplora, in maniera esaustiva, tutti i possibili stati in cui gli utenti possono trovarsi (eseguendo sequenze di movimenti tra gli ambienti e di accessi alle risorse, fisiche e logiche). In pratica l'analisi scopre tutto quello che ogni utente può fare direttamente o indirettamente, sfruttando la particolare configurazione degli elementi del sistema. Il servizio quindi confronta questo risultato e verifica che sia corretto rispetto alla security policy. Come risultato, il servizio costruisce una tabella evidenziando le violazioni delle policy: utenti che possono accedere ad una operazione su una risorsa contrariamente a quanto affermato nella security policy, o il caso opposto, ovvero utenti che non riescono ad accedere ad un risorsa quando invece devono poterlo fare. Per ogni utente analizzato il servizio crea anche il corrispondente Labelled Transition System (LTS) che rappresenta tutte le possibili sequenze di azioni che l'utente puo' compiere.