• sicurezza
• approcci formali
• transcompilazione
• firewall
• configurazione

Il porting delle configurazioni da un sistema di firewall a un altro è un procedimento difficile e costoso.
Le configurazioni consistono in centinaia di regole scritte in linguaggi di basso livello, specifici della
piattaforma ed in cui l’ordine delle regole influenza la semantica della configurazione. Senza una
procedura automatica per il porting, un amministratore è tenuto a conoscere i dettagli delle politiche
di sicurezza implementate e a progettare da capo la configurazione per il nuovo sistema. Nel caso
in cui le politiche di sicurezza non siano state documentate accuratamente è necessario analizzare la
configurazione iniziale e tentare di creare una configurazione equivalente per il sistema target: questo
è un procedimento rischioso perché è possibile tralasciare dettagli significativi e produrre un firewall
non equivalente a quello di partenza. È possibile in questo modo compromettere la sicurezza della
rete in quanto si implementa senza accorgersene una politica diversa da quella originale e gli asset
potrebbero non essere protetti in modo corretto. In un lavoro recente è stata proposta una pipeline di
transcompilazione fra linguaggi di configurazione di firewall, composta da tre fasi: (i ) decompilazione
della configurazione dal linguaggio di origine ad un linguaggio intermedio; (ii ) estrazione del significato
della configurazione come insieme minimale di regole dichiarative che descrivono i pacchetti accettati
e le traduzioni in termini logici; (iii ) compilazione delle regole dichiarative nel linguaggio target. Lo
strumento firewall synthesizer rappresenta l’implementazione delle prime due fasi in quanto permette,
facendo uso di un SAT solver, di derivare una rappresentazione ad alto livello della semantica di un
firewall. Per la fase (iii ) è stato proposto un algoritmo che tuttavia non ha garanzie di conservare la
traduzione degli indirizzi (Network Address Translation o NAT) e che si basa sull’operazione di marking
dei pacchetti, la quale è soggetta a restrizioni differenti nei vari sistemi firewall.
In questa tesi presentiamo un nuovo algoritmo per la sintesi della semantica nella fase (ii ) che
non necessita di un SAT solver e analizziamo formalmente la generazione della configurazione target
nella fase (iii ), tenendo in considerazione il problema di NAT. A questo scopo studiamo la differente
espressività dei sistemi firewall riguardo la traduzione degli indirizzi dei pacchetti. Nel linguaggio
intermedio, che è dotato di una semantica formale, ogni sistema firewall è modellato tramite un
diagramma di controllo e ogni configurazione come un assegnamento di ruleset ai nodi del diagramma.
Per ogni linguaggio di configurazione individuiamo dei vincoli che caratterizzano quali assegnamenti
di ruleset ai nodi del diagramma di controllo possono essere espressi e sfruttiamo questi vincoli sia per
studiare l’espressività dei linguaggi di configurazione, sia per definire un algoritmo per la generazione
della configurazione finale.