Configurazione automatica di Web Firewall = Automatic configuration of Web Firewalls

La Virtualizzazione delle Funzioni di Rete (in inglese Network Functions Virtualization, NFV) rappresenta una tecnologia avanzata che permette di separare le funzioni di rete dall'hardware specializzato. Questo disaccoppiamento consente l'eliminazione dei dispositivi hardware dedicati per ciascuna funzione di rete, favorendo invece l'esecuzione di tali funzioni tramite processi software su server generici. Uno dei risultati che si possono ottenere attraverso la NFV è la creazione di un Grafo di Servizio (in inglese, Service Graph), cioè una rappresentazione di come le varie funzioni di rete sono disposte ed interconnesse tra loro. Tuttavia, sorge un problema: la creazione del Service Graph è solitamente compito di un amministratore di rete, che si occupa manualmente dell'allocazione e della configurazione delle Network Security Functions (NSF). Queste NSF includono, ad esempio, web-application firewall, essenziali per proteggere la rete da minacce di sicurezza informatica. Purtroppo, le operazioni manuali eseguite dall'amministratore rendono il processo suscettibile ad errori umani. L'obiettivo di questo lavoro di tesi è quello di presentare una possibile soluzione al problema precedentemente descritto. Questa tesi ha difatti contribuito allo sviluppo di VEREFOO (VErified REFinement and Optimized Orchestration), un framework che si propone di fornire un approccio automatizzato per garantire la sicurezza di rete e risolvere il problema sopra menzionato. Il principale contributo fornito dal presente lavoro di tesi è rivolto ai WAFs (Web Application Firewalls) ed alla loro applicabilità nell'ambito di VEREFOO. Lo scopo principale di VEREFOO è quello di automatizzare ed ottimizzare l'allocazione e la configurazione delle NSF necessarie per soddisfare i requisiti di sicurezza della rete. Questi requisiti possono essere espressi dall'amministratore di rete utilizzando un linguaggio di alto livello, rendendo l'intero processo più intuitivo. L'ottimizzazione compiuta da VEREFOO si basa sulla formulazione di un problema MaxSMT (Satisfiability Modulo Theories) e la sua successiva risoluzione. L'obiettivo è soddisfare un insieme di clausole definite "hard" che devono essere sempre rispettate e di massimizzare la somma dei pesi attribuiti alle clausole "soft", che invece non è necessario che siano soddisfatte. VEREFOO utilizza la combinazione di clausole hard e soft per stabilire dove, all'interno del Service Graph, è necessario assegnare determinate NSF, minimizzando il numero di istanze generate ed il numero di regole calate all'interno di ogni istanza. Nello specifico, in questo documento, ci si sofferma sulle istanze di tipo Web Application Firewall.