Language-Independent Synthesis of Firewall Policies
| Autor: | Chiara Bodei, Pierpaolo Degano, Letterio Galletta, Lorenzo Veronese, Riccardo Focardi, Mauro Tempesta |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Standards
Computer science Network address translation 02 engineering and technology Security policy computer.software_genre Tools Firewall (construction) Policy Synthesis Control flow 020204 information systems Firewall configuration Network Security 0202 electrical engineering electronic engineering information engineering Proposals Operating systems 020203 distributed computing Intermediate language Tools Firewalls (computing) Proposals Network address translation Standards Operating systems Settore INF/01 - Informatica Network packet Programming language Solver computer Firewalls (computing) |
| Zdroj: | EuroS&P |
| DOI: | 10.1109/eurosp.2018.00015 |
| Popis: | Configuring and maintaining a firewall configuration is notoriously hard. Policies are written in low-level, platform-specific languages where firewall rules are inspected and enforced along non trivial control flow paths. Further difficulties arise from Network Address Translation (NAT), since filters must be implemented with addresses translations in mind. In this work, we study the problem of decompiling a real firewall configuration into an abstract specification. This abstract version throws the low-level details away by exposing the meaning of the configuration, i.e., the allowed connections with possible address translations. The generated specification makes it easier for system administrators to check if: (i) the intended security policy is actually implemented; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior. The peculiarity of our approach is that is independent of the specific target firewall system and language. This independence is obtained through a generic intermediate language that provides the typical features of real configuration languages and that separates the specification of the rulesets, determining the destiny of packets, from the specification of the platform-dependent steps needed to elaborate packets. We present a tool that decompiles real firewall configurations from different systems into this intermediate language and uses the Z3 solver to synthesize the abstract specification that succinctly represents the firewall behavior and the NAT. Tests on real configurations show that the tool is effective: it synthesizes complex policies in a matter of minutes and, and it answers to specific queries in just a few seconds. The tool can also point out policy differences before and after configuration updates in a simple, tabular form. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|