Transcompilazione fra linguaggi di firewall: sintesi e generazione di configurazioni
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.