“Transcompilation, synthesis and generation of firewall configuration languages“
The tool FireWall Synthesizer implements a transcompilation pipeline to (i) decompile real configurations into abstract specifications representing the set of the permitted connections; (ii) perform policy refactoring by removing redundant rules thus obtaining minimal and clean configurations; (iii) automatically port a configuration written for a system into the language of another system. The transcompiling pipeline is made of the following stages:
- decompile a policy from the source language to an intermediate language;
- extract the meaning of the policy as a table describing how the accepted packets are translated;
- compile the semantic table into the target language.
The core of the stage 1 is the intermediate language IFCL equipped with a formal semantics and with all the typical features of firewall languages. The intermediate language enables the algorithmic manipulation of stage 2. In this stage a SAT-based procedure is used to derive a declarative configuration in a tabular form that is minimal and captures all accepted packets and their transformations, with neither overlapping nor shadowing rules.
Bibliograpy
- L. Ceragioli, L. Galletta, M. Tempesta, From Firewalls to Functions and Back, in Proc. of the Third Italian Conference on Cyber Security (ITASEC 2019), Pisa, Italy, February 13-15, 2019
- L. Ceragioli, L. Galletta, M. Tempesta, Are All Firewall Systems Equally Powerful?, in Proc. of the 14th Workshop on Programming Languages and Analysis for Security (PLAS 2019), London, UK, November 15, 2019