Pierpaolo Degano, University of Pisa
From 11.30 until 13.00
At CNB/F/110 (Lunch) + CAB/F/100.9 (Seminar), ETH Zurich
Universitätstrasse 6, 8092 Zurich
Abstract:
Firewalls are a fundamental tool for managing and protecting computer networks.
They not only permit specifying which packets are allowed to enter a network, but also how these packets are modified by translating IP addresses and performing port redirection.
Configuring a firewall is notoriously hard.
Equally difficult are policy maintenance and refactoring, as well as porting a configuration from one firewall system to another.
One reason for that is that the configuration languages almost always have no clear meaning.
Based on that, we defined a pipeline, whose tools assists (assist) system administrators to check if:
(i) the intended security policy is actually implemented by a configuration;
(ii) two configurations are equivalent;
(iii) updates have the desired effect on the firewall behavior;
(iv) remove useless or redundant rules;
and additionally
(v) transcompile a configuration into an equivalent one in a different language.
The pipeline is based on IFCL, an intermediate firewall language that has a formal semantics.
More in detail, its first stage decompiles real firewall configurations from different systems into IFCL.
The second one transforms them as logical predicates and uses the Z3 solver to synthesize an abstract specification that succinctly represents the firewall behavior.
The system administrator can then analyze the firewall behavior by posing SQL-like queries, and he can update the configuration to meet the requrements.
Finally, the last stage compiles the abstract specification to the chosen language.
Tests on IPTABLES, IPFW and PF show that our tools are effective.